mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.add : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B₁ B₂ : Set β}
  {f₁ f₂ : α → β} {n : ℕ},
  IsAddFreimanHom n A B₁ f₁ → IsAddFreimanHom n A B₂ f₂ → IsAddFreimanHom n A (B₁ + B₂) (f₁ + f₂)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
MeasurableEquiv.IicProdIoi.eq_1 : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : DecidableLE ι] {X : ι → Type u_2} [inst_2 : LocallyFiniteOrderBot ι]
  [inst_3 : (i : ι) → MeasurableSpace (X i)] (a : ι),
  MeasurableEquiv.IicProdIoi a =
    { toFun := fun x i => if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩,
      invFun := fun x => (fun i => x ↑i, fun i => x ↑i), left_inv := ⋯, right_inv := ⋯, measurable_toFun := ⋯,
      measurable_invFun := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.c_without_negPivot_of_performRatCheck_success : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.AssignmentsInvariant →
    ∀ (negPivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHint : ℕ × Array ℕ),
      (f.performRatCheck negPivot ratHint).2 = true →
        ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
          f.clauses[ratHint.1]! = some c →
            Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f
              (c.delete negPivot)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_empty_type : ∀ {ι : Type u} {A : Type v} {x : ι → A} [inst : CommRing A] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra K A]
  [IsEmpty ι] [Nontrivial A], AlgebraicIndependent K x
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.insert_isBasis_insert_of_notMem_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} {I : Set α},
  M.IsBasis I X →
    e ∉ M.closure I →
      autoParam (e ∈ M.E) Matroid.IsBasis.insert_isBasis_insert_of_notMem_closure._auto_1 →
        M.IsBasis (insert e I) (insert e X)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.costructuredArrow_iso_iff : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {T : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} T] (P : CategoryTheory.MorphismProperty T) [P.RespectsIso]
  {L : CategoryTheory.Functor A T} {X : T} {f g : CategoryTheory.CostructuredArrow L X} (e : f ≅ g), P f.hom ↔ P g.hom
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix : Bool → Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.RingTheory.FreeCommRing
instCommRingFreeCommRing : (α : Type u_1) → CommRing (FreeCommRing α)
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.prodComonad_δ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (x : C),
  (CategoryTheory.prodComonad X).δ.app x =
    CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ x))
-- Mathlib.Topology.Homeomorph.Defs
/-- An equivalence between topological spaces respecting openness is a homeomorphism.  -/
Equiv.toHomeomorph : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → (e : X ≃ Y) → (∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) → X ≃ₜ Y
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.isUnit_iff_ordFrac_one_of_isDiscreteValuationRing : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {x : R},
  IsUnit x ↔ (Ring.ordFrac R) ((algebraMap R K) x) = 1
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Functor.toProfunctor_obj_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C) (X_1 : Dᵒᵖ), (F.toProfunctor.obj X).obj X_1 = (Opposite.unop X_1 ⟶ F.obj X)
-- Mathlib.Algebra.Group.TypeTags.Finite
instFiniteAdditive : ∀ {α : Type u} [Finite α], Finite (Additive α)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_zpow_iff_right_of_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {m n : ℤ}, 0 < a → a < 1 → (a ^ m < a ^ n ↔ n < m)
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reps.eq_1 : ∀ (m : ℤ), FixedDetMatrices.reps m = {A | ↑A 1 0 = 0 ∧ 0 < ↑A 0 0 ∧ 0 ≤ ↑A 0 1 ∧ |↑A 0 1| < |↑A 1 1|}
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.instMul : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → Mul ↑(Set.Ico 0 1)
-- Lean.CoreM
/-- Name of the file being compiled.  -/
Lean.Core.Context.fileName : Lean.Core.Context → String
-- Mathlib.CategoryTheory.Abelian.Exact
/-- If `(f, g)` is exact, then `Abelian.coimage.π g` is a cokernel of `f`.  -/
CategoryTheory.ShortComplex.Exact.isColimitCoimage : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Exact →
          CategoryTheory.Limits.IsColimit
            (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Abelian.coimage.π S.g) ⋯)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.trans.congr_simp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂}
  [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_7 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [inst_8 : RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [inst_9 : RingHomInvPair σ₃₁ σ₁₃] (e₁₂ e₁₂_1 : M₁ ≃ₛₗ[σ₁₂] M₂),
  e₁₂ = e₁₂_1 → ∀ (e₂₃ e₂₃_1 : M₂ ≃ₛₗ[σ₂₃] M₃), e₂₃ = e₂₃_1 → e₁₂.trans e₂₃ = e₁₂_1.trans e₂₃_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelp.toJson : Lean.Lsp.SignatureHelp → Lean.Json
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.colimitConstInitial_inv : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasInitial C],
  CategoryTheory.Limits.colimitConstInitial.inv =
    CategoryTheory.Limits.initial.to (CategoryTheory.Limits.colimit ((CategoryTheory.Functor.const J).obj (⊥_ C)))
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.Augmented.δ₀Iter_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (Y : CategoryTheory.SimplicialObject.Augmented C)
  {n m : ℕ} (i : ℕ) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.Augmented.δ₀Iter_hom_app._auto_1)
  {Z : C} (h : Y.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.left.δ₀Iter i hi)
      (CategoryTheory.CategoryStruct.comp (Y.hom.app (Opposite.op { len := n })) h) =
    CategoryTheory.CategoryStruct.comp (Y.hom.app (Opposite.op { len := m })) h
-- Init.System.IO
EIO.adaptExcept : {ε ε' α : Type} → (ε → ε') → EIO ε α → EIO ε' α
-- Mathlib.CategoryTheory.Sites.Abelian
CategoryTheory.sheafIsAbelian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} D] →
        [CategoryTheory.Abelian D] →
          {J : CategoryTheory.GrothendieckTopology C} →
            [CategoryTheory.HasSheafify J D] → CategoryTheory.Abelian (CategoryTheory.Sheaf J D)
-- Mathlib.RingTheory.Ideal.NatInt
/-- The natural numbers form a local semiring.  -/
instIsLocalRingNat : IsLocalRing ℕ
-- Lean.Declaration
/-- Inductive type this constructor is a member of  -/
Lean.ConstructorVal.induct : Lean.ConstructorVal → Lean.Name
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.arg.flag : Lean.Parser.ParserFn
-- Mathlib.Algebra.Homology.Augment
ChainComplex.augment_d_succ_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i j : ℕ),
  (C.augment f w).d (i + 1) (j + 1) = C.d i j
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y},
  (∀ {Z W : C} {f' : Z ⟶ W} {g' : Y ⟶ W} {g : X ⟶ Z}, CategoryTheory.IsPushout f g g' f' → P g → P g') →
    P.IsStableUnderCobaseChangeAlong f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
/-- The sheafification of presheaves of modules commutes with the functor which
forgets the module structures.  -/
PresheafOfModules.sheafificationCompForgetCompToPresheaf : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] →
                  [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
                    (PresheafOfModules.sheafification α).comp
                        ((SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.obj)) ≅
                      (PresheafOfModules.toPresheaf R₀).comp
                        ((CategoryTheory.presheafToSheaf J AddCommGrpCat).comp
                          (CategoryTheory.sheafToPresheaf J AddCommGrpCat))
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_zero_nat : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (k : ℕ), (f.genEigenspace 0) ↑k = LinearMap.ker (f ^ k)
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.projl_inl_apply : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {x : K},
  (LieAlgebra.SemiDirectSum.projl ψ) ((LieAlgebra.SemiDirectSum.inl ψ) x) = x
-- Mathlib.CategoryTheory.Filtered.Small
/-- Every functor from a small category to a cofiltered category factors fully faithfully through a
small cofiltered category. This is that category.  -/
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofilteredOrEmpty C] →
      {D : Type u₁} → [inst_2 : CategoryTheory.Category.{v₁, u₁} D] → CategoryTheory.Functor D C → Type (max u₁ v)
-- Mathlib.NumberTheory.FLT.Basic
FermatLastTheoremWith'.fermatLastTheoremWith : ∀ {R : Type u_2} [inst : CommSemiring R] [IsDomain R] {n : ℕ},
  FermatLastTheoremWith' R n →
    (∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n) → FermatLastTheoremWith R n
-- Init.Data.List.Perm
/-- Two lists without duplicates are permutations of each other if and only if
they have the same elements.  -/
List.perm_ext_iff_of_nodup : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Nodup → l₂.Nodup → (l₁.Perm l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.merge.eq_3 : ∀ {α : Type u_1} (le : α → α → Bool) (x : α) (xs_2 : List α) (y : α) (ys_2 : List α),
  (x :: xs_2).merge (y :: ys_2) le =
    if le x y = true then x :: xs_2.merge (y :: ys_2) le else y :: (x :: xs_2).merge ys_2 le
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.rank_add_le : ∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V'] [inst_4 : Module K V'] (f g : V →ₗ[K] V'), (f + g).rank ≤ f.rank + g.rank
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.isUniformOfEmpty : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  {P : Finpartition A} {G : SimpleGraph α} [inst_3 : DecidableRel G.Adj] {ε : 𝕜}, P.parts = ∅ → P.IsUniform G ε
-- Mathlib.Order.Filter.Bases.Basic
Filter.Tendsto.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β),
  Filter.Tendsto f l₁ l₂ = (Filter.map f l₁ ≤ l₂)
-- Init.Data.String.TakeDrop
/-- Removes leading whitespace from a string by returning a slice whose start position is the first
non-whitespace character, or the end position if there is no non-whitespace character.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.

Examples:

* `"abc".trimAsciiStart == "abc".toSlice`

* `"   abc".trimAsciiStart == "abc".toSlice`

* `"abc \t  ".trimAsciiStart == "abc \t  ".toSlice`

* `"  abc   ".trimAsciiStart == "abc   ".toSlice`

* `"abc\ndef\n".trimAsciiStart == "abc\ndef\n".toSlice`
 -/
String.trimAsciiStart : String → String.Slice
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Associate to a `PartialEquiv` an `Equiv` between the source and the target.  -/
PartialEquiv.toEquiv : {α : Type u_1} → {β : Type u_2} → (e : PartialEquiv α β) → ↑e.source ≃ ↑e.target
-- Mathlib.Tactic.ProdAssoc
/-- Elaborator for `prod_assoc%`.  -/
Lean.Expr.elabProdAssoc : Lean.Elab.Term.TermElab
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- A semiring `R` satisfies the strong rank condition, iff we cannot embed `R^(ℕ)` in some `Rⁿ`.  -/
strongRankCondition_iff_forall_not_injective : ∀ (R : Type u) [inst : Semiring R],
  StrongRankCondition R ↔ ∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Function.Injective ⇑f
-- Mathlib.RingTheory.FiniteLength
IsSemisimpleModule.finite_tfae : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M],
  [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instInhabitedCustomEliminators : Inhabited Lean.Meta.CustomEliminators
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.HasProjectiveResolution.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C},
  Nonempty (CategoryTheory.ProjectiveResolution Z) → CategoryTheory.HasProjectiveResolution Z
-- Std.Http.Data.Status
Std.Http.Status.preconditionRequired.sizeOf_spec : sizeOf Std.Http.Status.preconditionRequired = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.keys_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (t.get x ⋯))
        t.keys.attach).unattach
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourier_sum : ∀ {ι : Type u_1} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F]
  [inst_2 : FourierTransform E F] [FourierAdd E F] (f : ι → E) (s : Finset ι),
  FourierTransform.fourier (∑ i ∈ s, f i) = ∑ i ∈ s, FourierTransform.fourier (f i)
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Pull back a `MonoidWithZero` along an injective function.
See note [reducible non-instances].  -/
Function.Injective.monoidWithZero : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : Zero M₀'] →
      [inst_1 : Mul M₀'] →
        [inst_2 : One M₀'] →
          [inst_3 : Pow M₀' ℕ] →
            [inst_4 : MonoidWithZero M₀] →
              (f : M₀' → M₀) →
                Function.Injective f →
                  f 0 = 0 →
                    f 1 = 1 →
                      (∀ (x y : M₀'), f (x * y) = f x * f y) →
                        (∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n) → MonoidWithZero M₀'
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.right₀.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ), T.right₀ = Turing.ListBlank.cons T.head T.right
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.getElem_ofFn_go : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α} {acc : Array α} {i k : ℕ} (h : i ≤ n) (w₁ : k < acc.size + i),
  (Array.ofFn.go✝ f acc i h)[k] = if w₂ : k < acc.size then acc[k] else f ⟨n - i + k - acc.size, ⋯⟩
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.diff_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ m₄ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → ∀ (h₃ : m₃.WF), m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁.diff m₂ ⋯).Equiv (m₃.diff m₄ ⋯)
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- `OrderDual` as a functor.  -/
NonemptyFinLinOrd.dual : CategoryTheory.Functor NonemptyFinLinOrd NonemptyFinLinOrd
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_eq_one : ∀ {M : Type u_5} [inst : CommMonoid M] {s : Multiset M}, (∀ x ∈ s, x = 1) → s.prod = 1
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.iterFromIdxM_equiv_iterM_drop_toList : ∀ {n : ℕ} {α : Type w} {xs : Vector α n} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] {pos : ℕ},
  (xs.iterFromIdxM m pos).Equiv ((List.drop pos xs.toList).iterM m)
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_neg_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F) (α : A₁ ⟶ A₂),
  (-α).f = -α.f
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.liftQL.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Ring R] [inst_1 : Ring R₂] {σ : R →+* R₂} {M : Type u_3} {M₂ : Type u_4}
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] [inst_7 : Module R₂ M₂] (S : Submodule R M) (f f_1 : M →SL[σ] M₂) (e_f : f = f_1)
  (h : S ≤ (↑f).ker), S.liftQL f h = S.liftQL f_1 ⋯
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Disjoint unions of `X`-generated spaces are `X`-generated.  -/
Sigma.isGeneratedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {κ : Type u_1} {Y : κ → Type u_2}
  [inst_1 : (k : κ) → TopologicalSpace (Y k)] [∀ (k : κ), Topology.IsGeneratedBy X (Y k)],
  Topology.IsGeneratedBy X ((k : κ) × Y k)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.get?_ofSeq : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), (↑s).get? n = Computation.pure (s.get? n)
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.inv_nonneg : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 ≤ p⁻¹
-- Mathlib.Topology.Constructions.SumProd
mem_nhdsWithin_prod_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {y : Y} {s : Set (X × Y)}
  {tx : Set X} {ty : Set Y}, s ∈ nhdsWithin (x, y) (tx ×ˢ ty) ↔ ∃ u ∈ nhdsWithin x tx, ∃ v ∈ nhdsWithin y ty, u ×ˢ v ⊆ s
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- The Bochner integral in L1 space as a continuous linear map over ℝ.  -/
MeasureTheory.L1.integralCLM : {α : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      {m : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : NormedSpace ℝ E] → [CompleteSpace E] → ↥(MeasureTheory.Lp E 1 μ) →L[ℝ] E
-- Lean.Language.Basic
/-- Monad transformer holding all relevant data for processing.  -/
Lean.Language.ProcessingT : (Type → Type u_1) → Type → Type u_1
-- Mathlib.Order.Filter.Basic
Filter.eventuallyLE_iff_all_subsets : ∀ {α : Type u} {β : Type v} [inst : LE β] {f g : α → β} {l : Filter α},
  f ≤ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x ≤ g x
-- Mathlib.Topology.Algebra.Group.Basic
topologicalAddGroup_iInf : ∀ {G : Type w} {ι : Sort u_1} [inst : AddGroup G] {ts' : ι → TopologicalSpace G},
  (∀ (i : ι), IsTopologicalAddGroup G) → IsTopologicalAddGroup G
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.imageMonoIsoSource_hom_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).hom f =
    CategoryTheory.Limits.image.ι f
-- Init.Data.Fin.Basic
/-- Coarsens a bound by one.
 -/
Fin.castSucc : {n : ℕ} → Fin n → Fin (n + 1)
-- Lean.Server.Completion.CompletionUtils
_private.Lean.Server.Completion.CompletionUtils.0.Lean.Server.Completion.getDotIdCompletionTypeNames.visit : Lean.Expr → StateRefT' IO.RealWorld (Array Lean.Name) Lean.MetaM Unit
-- Init.Data.Nat.Basic
Nat.sub_le_sub_iff_right : ∀ {k m n : ℕ}, k ≤ m → (n - k ≤ m - k ↔ n ≤ m)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The obvious splitting of a short complex when `S.X₁` is zero and `S.g` is an isomorphism.  -/
CategoryTheory.ShortComplex.Splitting.ofIsZeroOfIsIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex C) → CategoryTheory.Limits.IsZero S.X₁ → CategoryTheory.IsIso S.g → S.Splitting
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The comparison morphism for the pullback of `f,g`.
This is an isomorphism iff `G` preserves the pullback of `f,g`; see
`Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean`
 -/
CategoryTheory.Limits.pullbackComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (G : CategoryTheory.Functor C D) →
            (f : X ⟶ Z) →
              (g : Y ⟶ Z) →
                [inst_2 : CategoryTheory.Limits.HasPullback f g] →
                  [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] →
                    G.obj (CategoryTheory.Limits.pullback f g) ⟶ CategoryTheory.Limits.pullback (G.map f) (G.map g)
-- Init.Data.String.Basic
String.isUTF8FirstByte_getUTF8Byte_zero : ∀ {b : String} {h : 0 < b.rawEndPos}, (b.getUTF8Byte 0 h).IsUTF8FirstByte
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂],
  (HomologicalComplex₂.total.mapIso e c₁₂).inv = HomologicalComplex₂.total.map e.inv c₁₂
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `Kᗮ` can be characterized as the intersection of the kernels of the operations of
inner product with each of the elements of `K`.  -/
Submodule.orthogonal_eq_inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), Kᗮ = ⨅ v, (↑((innerSL 𝕜) ↑v)).ker
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The contrapositive of `disjoint_openCell_of_ne`.  -/
Topology.RelCWComplex.eq_of_not_disjoint_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] {n : ℕ}
  {j : Topology.RelCWComplex.cell C n} {m : ℕ} {i : Topology.RelCWComplex.cell C m},
  ¬Disjoint (Topology.RelCWComplex.openCell n j) (Topology.RelCWComplex.openCell m i) → ⟨n, j⟩ = ⟨m, i⟩