mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.instPseudoMetricSpaceOfBoundedSpace : {α : Type u_1} → {β : Type u_2} → [inst : PseudoMetricSpace β] → [BoundedSpace β] → PseudoMetricSpace (UniformFun α β)
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.disjoint_map_compl : ∀ {α : Type u_1} [inst : BooleanAlgebra α] {s : Finset α},
  (↑s).Intersecting → Disjoint s (Finset.map { toFun := compl, inj' := ⋯ } s)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.toJordanDecomposition_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α}
  {j : MeasureTheory.JordanDecomposition α}, s = j.toSignedMeasure → s.toJordanDecomposition = j
-- Init.Data.AC
Lean.Data.AC.Expr.op.sizeOf_spec : ∀ (lhs rhs : Lean.Data.AC.Expr), sizeOf (lhs.op rhs) = 1 + sizeOf lhs + sizeOf rhs
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.compMono_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [inst_1 : CategoryTheory.Mono g],
  (F.compMono g).I = F.I
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instCompleteSpace : ∀ {R : Type u_3} {M : Type u_4} [inst : UniformSpace R] [inst_1 : UniformSpace M] [CompleteSpace R] [CompleteSpace M],
  CompleteSpace (TrivSqZeroExt R M)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.package : Lean.Lsp.SymbolKind
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_biInter : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_3} {p : ι → Prop} {s : (i : ι) → p i → Set α},
  (∀ (i : ι) (hi : p i), (s i hi).OrdConnected) → (⋂ i, ⋂ (hi : p i), s i hi).OrdConnected
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_expandIfNecessary : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑m.expandIfNecessary
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.higherOrders : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State → Array Bool
-- Mathlib.Algebra.BigOperators.Ring.List
List.sum_map_mul_right : ∀ {ι : Type u_1} {R : Type u_5} [inst : NonUnitalNonAssocSemiring R] (l : List ι) (f : ι → R) (r : R),
  (List.map (fun b => f b * r) l).sum = (List.map f l).sum * r
-- Mathlib.CategoryTheory.Generator.Sheaf
CategoryTheory.Sheaf.isSeparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasCoproducts A]
  [inst_3 : CategoryTheory.HasWeakSheafify J A] {ι : Type w} {S : ι → A},
  (CategoryTheory.ObjectProperty.ofObj S).IsSeparating →
    ∀
      [inst_4 :
        CategoryTheory.Limits.HasCoproduct fun x =>
          match x with
          | (X, i) => CategoryTheory.Sheaf.freeYoneda J X (S i)]
      [CategoryTheory.Preadditive A],
      CategoryTheory.IsSeparator
        (∐ fun x =>
          match x with
          | (X, i) => CategoryTheory.Sheaf.freeYoneda J X (S i))
-- Std.Time.Format.Basic
/-- Locale configuration for formatting and parsing, including locale-specific symbols and the first
day of the week used for week-of-year and week-of-month calculations.
Default is `DateFormat.enUS` (English, US).
 -/
Std.Time.FormatConfig.dateformat : Std.Time.FormatConfig → Std.Time.DateFormat
-- Lean.Meta.Basic
/-- Like `letTelescope`, but limits the number of `let`/`have`s consumed to `maxFVars?`.
If `maxFVars?` is none, then this is the same as `letTelescope`.
 -/
Lean.Meta.letBoundedTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        Lean.Expr →
          Option ℕ →
            (Array Lean.Expr → Lean.Expr → n α) → optParam Bool false → optParam Bool true → optParam Bool false → n α
-- Init.Data.Vector.Lemmas
Vector.flatten_flatten : ∀ {α : Type u_1} {n m k : ℕ} {xss : Vector (Vector (Vector α n) m) k},
  xss.flatten.flatten = Vector.cast ⋯ (Vector.map Vector.flatten xss).flatten
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsStrictRestriction.isRestriction : ∀ {α : Type u_1} {M N : Matroid α}, N.IsStrictRestriction M → N.IsRestriction M
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        (P₁ : CategoryTheory.Limits.IndObjectPresentation A) →
          (P₂ : CategoryTheory.Limits.IndObjectPresentation B) →
            CategoryTheory.Limits.IsColimit
              { pt := B, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ f g P₁ P₂ }
-- Mathlib.Algebra.Group.Defs
isDedekindFiniteAddMonoid_iff : ∀ (M : Type u_2) [inst : AddZero M], IsDedekindFiniteAddMonoid M ↔ ∀ {a b : M}, a + b = 0 → b + a = 0
-- Mathlib.Algebra.Group.Defs
/-- If all additions cancel on the right then every element is add-right-regular.  -/
IsAddRightRegular.all : ∀ {R : Type u_2} [inst : Add R] [IsRightCancelAdd R] (g : R), IsAddRightRegular g
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovEDist_self : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ : MeasureTheory.Measure Ω),
  MeasureTheory.levyProkhorovEDist μ μ = 0
-- Init.Data.String.Termination
String.Pos.remainingBytes_inj : ∀ {s : String} {p q : s.Pos}, p.remainingBytes = q.remainingBytes ↔ p = q
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posDef_sum : ∀ {m : Type u_1} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {ι : Type u_5}
  [AddLeftMono R] {A : ι → Matrix m m R} {s : Finset ι}, s.Nonempty → (∀ i ∈ s, (A i).PosDef) → (∑ i ∈ s, A i).PosDef
-- Lean.Meta.Basic
Lean.Meta.synthPending : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.continuousAt_iteratedFDeriv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {n : WithTop ℕ∞} {k : ℕ}, ContDiffAt 𝕜 n f x → ↑k ≤ n → ContinuousAt (iteratedFDeriv 𝕜 k f) x
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.formatErrorMessage.prettyCoeffs : Array String → Lean.Omega.Coeffs → String
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.category_comp_hom : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {X Y Z : CategoryTheory.Limits.Bicone F}
  (f : CategoryTheory.Limits.BiconeMorphism X Y) (g : CategoryTheory.Limits.BiconeMorphism Y Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Std.Sync.CancellationContext
Std.CancellationContext.State.mk.inj : ∀ {tokens : Std.TreeMap UInt64 (Std.CancellationToken × Array UInt64) compare} {id : UInt64}
  {tokens_1 : Std.TreeMap UInt64 (Std.CancellationToken × Array UInt64) compare} {id_1 : UInt64},
  { tokens := tokens, id := id } = { tokens := tokens_1, id := id_1 } → tokens = tokens_1 ∧ id = id_1
-- Mathlib.Topology.UniformSpace.Defs
/-- Construct a `UniformSpace` from a `UniformSpace.Core`.  -/
UniformSpace.ofCore : {α : Type u} → UniformSpace.Core α → UniformSpace α
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_forIn : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] {α : Type uu} (as : Array α) (init : β)
  (f : γ → α → β → m (ForInStep β)), Lean.Order.monotone f → Lean.Order.monotone fun x => forIn as init (f x)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_smul`. -/
ModularForm.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_preimage_singleton : ∀ {α : Type u_2} {β : Type u_3} (f : α → β) (s : Finset β), ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' ↑s
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Function.Injective ⇑(Monoid.Coprod.swap M N)
-- Lean.Linter.Init
/-- The `LinterOptions` structure is used to determine whether given linters are enabled.

This structure contains all the data required to do so, the `Options` set on the command line
or by the `set_option` command, and the `LinterSets` that have been declared.

A single structure holding this data is useful since we want `getLinterValue` to be a pure
function: determining the `LinterSets` would otherwise require a `MonadEnv` instance.
 -/
Lean.Linter.LinterOptions : Type
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of costructured arrows `F.obj c ⟶ d` to the category of structured arrows
`op d ⟶ F.op.obj c`.
 -/
CategoryTheory.CostructuredArrow.toStructuredArrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (d : D) →
            CategoryTheory.Functor (CategoryTheory.CostructuredArrow F d)ᵒᵖ
              (CategoryTheory.StructuredArrow (Opposite.op d) F.op)
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- An invariant linear map from coweight space to weight space.  -/
RootPairing.CoPolarization : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → [Fintype ι] → N →ₗ[R] M
-- Mathlib.Topology.Algebra.MulAction
/-- The scalar multiplication `(•)` is continuous.  -/
ContinuousSMul.continuous_smul : ∀ {M : Type u_1} {X : Type u_2} {inst : SMul M X} {inst_1 : TopologicalSpace M} {inst_2 : TopologicalSpace X}
  [self : ContinuousSMul M X], Continuous fun p => p.1 • p.2
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.girth_le_length : ∀ {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a}, w.IsCycle → G.girth ≤ w.length
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.inv_hom_id_eval : ∀ {C : Type u_1} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.GradedObject J C}
  (e : X ≅ Y) (j : J), CategoryTheory.CategoryStruct.comp (e.inv j) (e.hom j) = CategoryTheory.CategoryStruct.id (Y j)
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instBEqOfTransCmp : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → BEq (Std.ExtTreeSet α cmp)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool}
  {k fallback : α}, (Std.ExtTreeSet.filter f t).getD k fallback = (Option.filter f (t.get? k)).getD fallback
-- Lean.Compiler.InlineAttrs
Lean.Compiler.hasNoInlineAttribute : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- Composition of module object morphisms.  -/
CategoryTheory.Mod.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] → {M N O : CategoryTheory.Mod D A} → M.Hom N → N.Hom O → M.Hom O
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (Y.presheaf.obj (Opposite.op ⊤)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Y.toSpecΓ h) =
    CategoryTheory.CategoryStruct.comp X.toSpecΓ
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) h)
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.Accuracy.exact.sizeOf_spec : sizeOf Float.Model.UnpackedFloat.Accuracy.exact = 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, i < r.toList.length → (Std.PRange.succMany? (i + 1) r.lower).isSome = true
-- Mathlib.Algebra.Quaternion
Quaternion.imK_im : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a.im.imK = a.imK
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.one_le_convexBodyLT'Factor : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], 1 ≤ NumberField.mixedEmbedding.convexBodyLT'Factor K
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.bilinearRestrictScalars_apply_apply : ∀ (𝕜 : Type u_1) {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : SeminormedAddCommGroup E]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E]
  [inst_7 : SeminormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F]
  [inst_10 : IsScalarTower 𝕜 𝕜' F] [inst_11 : SeminormedAddCommGroup G] [inst_12 : NormedSpace 𝕜 G]
  [inst_13 : NormedSpace 𝕜' G] [inst_14 : IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G) (x : E) (y : F),
  ((ContinuousLinearMap.bilinearRestrictScalars 𝕜 B) x) y = (B x) y
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extend_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {X : C} (f : c.pt ⟶ X),
  (c.extend f).ι = CategoryTheory.CategoryStruct.comp c.ι ((CategoryTheory.Functor.const J).map f)
-- Mathlib.Algebra.Group.Submonoid.Defs
MonoidHom.mem_eqLocusM : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {f g : M →* N} {x : M},
  x ∈ f.eqLocusM g ↔ f x = g x
-- Mathlib.RingTheory.Unramified.LocalStructure
/-- Let `S` be an finite `R`-algebra that is unramified at some prime `Q`. Then there exists some
`x : S` such that `Q` is the unique prime lying over `P := Q ∩ R⟨x⟩` and `κ(P) = κ(Q)`.  -/
Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
  [inst_3 : Q.IsPrime] [Module.Finite R S] [Algebra.IsUnramifiedAt R Q],
  ∃ x,
    (Ideal.under (↥R[x]) Q).primesOver S = {Q} ∧
      Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.associator_inv_hom : ∀ {B : Type u} [inst : Quiver B] {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c) (h : CategoryTheory.FreeBicategory.Hom c d),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h).vcomp
      (CategoryTheory.FreeBicategory.Hom₂.associator f g h))
    (CategoryTheory.FreeBicategory.Hom₂.id (f.comp (g.comp h)))
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.leadingCoeff_T : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [NeZero 2] (n : ℤ),
  (Polynomial.Chebyshev.T R n).leadingCoeff = 2 ^ (n.natAbs - 1)
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.EStateM.instWP.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.error e s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_2 e s'
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.ext_of_ring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A] {f g : R →ₐc[R] A}, f 1 = g 1 → f = g
-- Init.Data.List.Lemmas
List.foldl_map : ∀ {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {f : β₁ → β₂} {g : α → β₂ → α} {l : List β₁} {init : α},
  List.foldl g init (List.map f l) = List.foldl (fun x y => g x (f y)) init l
-- Init.Data.List.BasicAux
List.getElem_append_left : ∀ {α : Type u_1} {i : ℕ} {as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length}, (as ++ bs)[i] = as[i]
-- Lean.Widget.Diff
/-- Computes a diff between `before` and `after` expressions.

This works by recursively comparing function arguments.

TODO(ed): experiment with a 'greatest common subexpression' design where
  given `e₀`, `e₁`, find the greatest common subexpressions `Xs : Array Expr` and a congruence `F` such that
  `e₀ = F[A₀[..Xs]]` and `e₀ = F[A₁[..Xs]]`. Then, we can have fancy diff highlighting where common subexpressions are not highlighted.

## Diffing binders

Two binding domains are identified if they have the same user name and the same type.
The most common tactic that modifies binders is after an `intros`.
To deal with this case, if `before = (a : α) → β` and `after`, is not a matching binder (ie: not `(a : α) → _`)
then we instantiate the `before` variable in a new context and continue diffing `β` against `after`.

  -/
_private.Lean.Widget.Diff.0.Lean.Widget.exprDiffCore : Lean.SubExpr → Lean.SubExpr → Lean.MetaM Lean.Widget.ExprDiff✝
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerToKer'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {n : ℕ}
  {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n)
  (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc hcc_1 : CategoryTheory.Limits.IsColimit cc),
  hcc = hcc_1 →
    ∀ (hkf hkf_1 : CategoryTheory.Limits.IsLimit kf),
      hkf = hkf_1 → hS.cokerToKer' k hk cc kf hcc hkf = hS.cokerToKer' k hk cc kf hcc_1 hkf_1
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.single_apply_self : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a : E i), ↑(lp.single p i a) i = a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierTensorRight : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (F : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))),
  CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u_1, max u u_1, max (max (u + 1) u_1) v_1,
      max (max (u + 1) u_1) v_1}
    (CategoryTheory.MonoidalCategory.tensorRight F)
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxoHasSize : Std.Rxo.HasSize ISize
-- Lean.AddDecl
_private.Lean.AddDecl.0.Lean.registerNamePrefixes : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
/-- See also `Complex.pow_cpow_ofNat_inv` for a version that also works for `x * I`, `0 ≤ x`.  -/
Complex.sq_cpow_two_inv : ∀ {x : ℂ}, 0 < x.re → (x ^ 2) ^ 2⁻¹ = x
-- Init.Data.String.Modify
String.Internal.capitalizeImpl : String → String
-- Mathlib.Analysis.Complex.Circle
/-- The additive character from `ℝ` onto the circle, given by `fun x ↦ exp (2 * π * x * I)`.
Denoted as `𝐞` within the `Real.FourierTransform` namespace. This uses the analyst convention that
there is a `2 * π` in the exponent.  -/
Real.fourierChar : AddChar ℝ Circle
-- Mathlib.Order.Bounds.Image
StrictAnti.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {a : α} {s : Set α},
  StrictAnti f → (IsGreatest (f '' s) (f a) ↔ IsLeast s a)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (hx : AlgebraicIndependent R x), hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X none) = Polynomial.X
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair_map_reflexion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A)
  {sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B}
  {sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B},
  (CategoryTheory.Limits.reflexivePair f g s sl sr).map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion = s
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- An open neighborhood of the identity in the Cartesian product of two nonarchimedean groups
contains the Cartesian product of an open neighborhood in each group.  -/
NonarchimedeanGroup.prod_subset : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [NonarchimedeanGroup G] {K : Type u_3}
  [inst_3 : Group K] [inst_4 : TopologicalSpace K] [NonarchimedeanGroup K] {U : Set (G × K)},
  U ∈ nhds 1 → ∃ V W, ↑V ×ˢ ↑W ⊆ U
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.mk.inj : ∀ {X : Type u_1} {inst : PseudoMetricSpace X} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {setsAt : X → Set (Set X)} {measurableSet : ∀ (x : X), ∀ s ∈ setsAt x, MeasurableSet s}
  {nonempty_interior : ∀ (x : X), ∀ s ∈ setsAt x, (interior s).Nonempty}
  {nontrivial : ∀ (x : X), ∀ ε > 0, ∃ s ∈ setsAt x, s ⊆ Metric.closedBall x ε}
  {covering :
    ∀ (s : Set X) (f : X → Set (Set X)),
      (∀ x ∈ s, f x ⊆ setsAt x) →
        (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
          ∃ t,
            (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0}
  {setsAt_1 : X → Set (Set X)} {measurableSet_1 : ∀ (x : X), ∀ s ∈ setsAt_1 x, MeasurableSet s}
  {nonempty_interior_1 : ∀ (x : X), ∀ s ∈ setsAt_1 x, (interior s).Nonempty}
  {nontrivial_1 : ∀ (x : X), ∀ ε > 0, ∃ s ∈ setsAt_1 x, s ⊆ Metric.closedBall x ε}
  {covering_1 :
    ∀ (s : Set X) (f : X → Set (Set X)),
      (∀ x ∈ s, f x ⊆ setsAt_1 x) →
        (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
          ∃ t,
            (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0},
  { setsAt := setsAt, measurableSet := measurableSet, nonempty_interior := nonempty_interior, nontrivial := nontrivial,
        covering := covering } =
      { setsAt := setsAt_1, measurableSet := measurableSet_1, nonempty_interior := nonempty_interior_1,
        nontrivial := nontrivial_1, covering := covering_1 } →
    setsAt = setsAt_1
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Matrix of coefficients the basic variables expressed through the free ones.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau.mat : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    (self : Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType) → matType self.basic.size self.free.size
-- Init.Data.UInt.Bitwise
UInt64.toBitVec_or : ∀ (a b : UInt64), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec