mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (app : (a : B) → F.obj a ⟶ G.obj a) →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (F.map f) (app b) ⟶
                      CategoryTheory.CategoryStruct.comp (app a) (G.map f)) →
              autoParam
                  (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b))
                        (naturality g) =
                      CategoryTheory.CategoryStruct.comp (naturality f)
                        (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
                  CategoryTheory.Oplax.OplaxTrans.naturality_naturality._autoParam →
                autoParam
                    (∀ (a : B),
                      CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a))
                          (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a)) =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
                            (CategoryTheory.Bicategory.rightUnitor (app a)).inv))
                    CategoryTheory.Oplax.OplaxTrans.naturality_id._autoParam →
                  autoParam
                      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g))
                            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g)) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c))
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom)))))
                      CategoryTheory.Oplax.OplaxTrans.naturality_comp._autoParam →
                    CategoryTheory.Oplax.OplaxTrans F G
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The same-universe version of `Algebra.lift_rank_le_of_surjective_injective`.  -/
Algebra.rank_le_of_surjective_injective : ∀ {R : Type w} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {R' : Type w'}
  [inst_3 : CommSemiring R'] {S' : Type v} [inst_4 : Semiring S'] [inst_5 : Algebra R' S'] (i : R →+* R')
  (j : S →+* S'),
  Function.Surjective ⇑i →
    Function.Injective ⇑j → (algebraMap R' S').comp i = j.comp (algebraMap R S) → Module.rank R S ≤ Module.rank R' S'
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesIsoSc'_hom_iCycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom
      (CategoryTheory.CategoryStruct.comp (K.sc' i j k).iCycles h) =
    CategoryTheory.CategoryStruct.comp (K.iCycles j) h
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.equalizerCondition_w : ∀ {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] (P : CategoryTheory.Functor Cᵒᵖ D) {X B : C} {π : X ⟶ B}
  (c : CategoryTheory.Limits.PullbackCone π π),
  CategoryTheory.CategoryStruct.comp (P.map π.op) (P.map c.fst.op) =
    CategoryTheory.CategoryStruct.comp (P.map π.op) (P.map c.snd.op)
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.le_greatestFib : ∀ {m n : ℕ}, m ≤ n.greatestFib ↔ Nat.fib m ≤ n
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F),
  HasFDerivAt b (h.deriv p) p
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.fderiv_succ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F → G} {g : E → F},
  ContDiff 𝕜 (n + 1) (Function.uncurry f) → ContDiff 𝕜 n g → ContDiff 𝕜 n fun x => fderiv 𝕜 (f x) (g x)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.ruleSets : Aesop.Frontend.RuleSets → Aesop.Frontend.Feature
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- `Matrix.UnitaryGroup.toLin' A` is matrix multiplication of vectors by `A`, as a linear map.

After the group structure on `Matrix.unitaryGroup n` is defined, we show in
`Matrix.UnitaryGroup.toLinearEquiv` that this gives a linear equivalence.
 -/
Matrix.UnitaryGroup.toLin' : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} → [inst_2 : CommRing α] → [inst_3 : StarRing α] → ↥(Matrix.unitaryGroup n α) → (n → α) →ₗ[α] n → α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, k ∈ Std.ExtDTreeMap.Const.unitOfList l cmp ↔ l.contains k = true
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.hundred_le_m : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 → ε ≤ 1 → 100 ≤ Fintype.card α / SzemerediRegularity.stepBound P.parts.card
-- Init.Data.Rat.Lemmas
Rat.intCast_nonpos : ∀ {a : ℤ}, ↑a ≤ 0 ↔ a ≤ 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  (Std.ExtDHashMap.filterMap f m).getKey? k =
    (m.getKey? k).pfilter fun x_2 h' => (f x_2 (Std.ExtDHashMap.Const.get m x_2 ⋯)).isSome
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.forget₂_moduleCat_obj : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] (A : Rep.{w, u, v} k G),
  (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).obj A = ModuleCat.of k ↑A
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.eval.eq_2 : Turing.ToPartrec.Code.succ.eval = fun v => pure [v.headI.succ]
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.mk : {E : Type u} → {F : outParam (Type v)} → (E → F) → FourierTransform E F
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.reverse.inj : ∀ {n n_1 : Lean.Name},
  Batteries.Tactic.Alias.AliasInfo.reverse n = Batteries.Tactic.Alias.AliasInfo.reverse n_1 → n = n_1
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsBasis'.finite_iff_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsBasis' I X → (I.Finite ↔ M.IsRkFinite X)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `MorphismProperty.Over.pullback` commutes with `MorphismProperty.Over.forget`.  -/
CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        {X Y : T} →
          (f : X ⟶ Y) →
            [inst_2 : CategoryTheory.Limits.HasPullbacksAlong f] →
              [inst_3 : P.IsStableUnderBaseChangeAlong f] →
                [inst_4 : Q.IsStableUnderBaseChange] →
                  (CategoryTheory.MorphismProperty.Over.pullback P Q f).comp
                      (CategoryTheory.MorphismProperty.Over.forget P Q X) ≅
                    (CategoryTheory.MorphismProperty.Over.forget P Q Y).comp (CategoryTheory.Over.pullback f)
-- Init.Data.List.Zip
List.zipWith_foldr_eq_zip_foldr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {f : α → β → γ} {i : δ}
  {g : γ → δ → δ}, List.foldr g i (List.zipWith f l₁ l₂) = List.foldr (fun p r => g (f p.1 p.2) r) i (l₁.zip l₂)
-- Mathlib.Topology.Order.DenselyOrdered
nhdsGT_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] (a : α), (nhdsWithin a (Set.Ioi a)).NeBot
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If a function admits a finite power series expansion `p` on an open ball `B (x, r)`, then
it is continuously polynomial at every point of this ball.  -/
HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem : ∀ {𝕜 : 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}
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {x y : E},
  HasFiniteFPowerSeriesOnBall f p x n r → y ∈ Metric.eball x r → CPolynomialAt 𝕜 f y
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.unerase : Lean.Meta.SimpTheorems → Lean.Meta.Origin → Lean.Meta.SimpTheorems
-- Lean.Data.KVMap
Lean.KVMap.instToString : ToString Lean.KVMap
-- Init.Meta.Defs
/-- Syntax that represents a precedence (e.g. for an operator).
 -/
Lean.Syntax.Prec : Type
-- Lean.Meta.Tactic.Simp.Types
/-- Adds the fvars from `usedZetaDelta` to `s` if they are present in
the set `zetaDeltaSet` of fvars that are explicitly added to the simp context.

*Note:* `usedZetaDelta` might contain fvars that are not in `zetaDeltaSet`,
since within `withResetZetaDeltaFVarIds` it is possible for `whnf` to be run with different configurations,
ones that allow zeta-delta reducing fvars not in `zetaDeltaSet` (e.g. `withInferTypeConfig` sets `zetaDelta := true`).
This also means that `usedZetaDelta` set might be reporting fvars in `zetaDeltaSet` that weren't "used".
 -/
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.updateUsedSimpsWithZetaDeltaCore : Lean.Meta.Simp.UsedSimps → Lean.FVarIdSet → Lean.FVarIdSet → Lean.Meta.Simp.UsedSimps
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- The bijection `X.S ≃ Y.S` on simplices of simplicial sets that
is induced by an isomorphism `X ≅ Y`.  -/
SSet.S.equivOfIso : {X Y : SSet} → (X ≅ Y) → X.S ≃ Y.S
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- Internal tactic used in `coherence`.

Rewrites an equation `f = g` as `f₀ ≫ f₁ = g₀ ≫ g₁`,
where `f₀` and `g₀` are maximal prefixes of `f` and `g` (possibly after reassociating)
which are "liftable" (i.e. expressible as compositions of unitors and associators).
 -/
Mathlib.Tactic.Coherence.liftable_prefixes : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray.eq_1 : ∀ {α : Type u} {β : Type v} (t : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.toArray t =
    Std.DTreeMap.Internal.Impl.foldl (fun l k v => l.push (k, v)) (Array.emptyWithCapacity t.size) t
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.overrideComputedFields : Lean.Elab.ComputedFields.M Unit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_one : Real.arctan 1 = Real.pi / 4
-- Aesop.Forward.State
/-- Does this `Hyp` represent a pattern substitution?  -/
Aesop.Hyp.isPatSubst : Aesop.Hyp → Bool
-- Mathlib.Data.Multiset.Interval
Multiset.card_uIcc : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  (Finset.uIcc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(Multiset.count i t) - ↑(Multiset.count i s)).natAbs + 1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertMany_cons : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {l : List (α × β)} {k : α} {v : β},
  m.insertMany ((k, v) :: l) = (m.insert k v).insertMany l
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.instIsModHomInvOfHom : ∀ {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 : D} [inst_5 : CategoryTheory.ModObj A M]
  [inst_6 : CategoryTheory.ModObj A N] (f : M ≅ N) [CategoryTheory.IsModHom A f.hom], CategoryTheory.IsModHom A f.inv
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mk.sizeOf_spec : ∀ {α : Type u} [inst : MeasurableSpace α] {β : Type v} [inst_1 : SizeOf α] [inst_2 : SizeOf β] (toFun : α → β)
  (measurableSet_fiber' : ∀ (x : β), MeasurableSet (toFun ⁻¹' {x})) (finite_range' : (Set.range toFun).Finite),
  sizeOf { toFun := toFun, measurableSet_fiber' := measurableSet_fiber', finite_range' := finite_range' } =
    1 + sizeOf finite_range'
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
/-- If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an
invertible derivative `f'` at `g a` in the strict sense, then `g` has the derivative `f'⁻¹` at `a`
in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an
inverse function.  -/
HasStrictFDerivAt.of_local_left_inverse : ∀ {𝕜 : 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} {f' : E ≃L[𝕜] F}
  {g : F → E} {a : F},
  ContinuousAt g a →
    HasStrictFDerivAt f (↑f') (g a) → (∀ᶠ (y : F) in nhds a, f (g y) = y) → HasStrictFDerivAt g (↑f'.symm) a
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.div : ∀ {𝕜 : 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] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedField F'] [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'} {p' q' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt[s] p z p' →
    HasMFDerivAt[s] q z q' → q z ≠ 0 → HasMFDerivAt[s] (p / q) z ((1 / q z) • p' - (p z / q z ^ 2) • q')
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- Any finitely generated ideal is principal.  -/
IsBezout.isPrincipal_of_FG : ∀ {R : Type u} {inst : Semiring R} [self : IsBezout R] (I : Ideal R), I.FG → Submodule.IsPrincipal I
-- Mathlib.Algebra.Group.AddChar
AddChar.sum_ne_zero_iff_eq_zero : ∀ {A : Type u_1} {R : Type u_2} [inst : AddGroup A] [inst_1 : Fintype A] [inst_2 : CommSemiring R] [IsDomain R]
  {ψ : AddChar A R} [CharZero R], ∑ x, ψ x ≠ 0 ↔ ψ = 0
-- Mathlib.Control.Fix
/-- loop body for finding the fixed point of `f`  -/
Part.fixAux : {α : Type u_1} →
  {β : α → Type u_2} →
    (((a : α) → Part (β a)) → (a : α) → Part (β a)) →
      {p : ℕ → Prop} → (i : Nat.Upto p) → ((j : Nat.Upto p) → i < j → (a : α) → Part (β a)) → (a : α) → Part (β a)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_nil : ∀ {α : Type u}, Stream'.WSeq.nil.head = Computation.pure none
-- Init.Data.Repr
instReprAtomChar : ReprAtom Char
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofNat_eq_ofENat : ∀ {m : ℕ} {n : ℕ∞} [inst : m.AtLeastTwo], OfNat.ofNat m = ↑n ↔ OfNat.ofNat m = n
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_symm_pi_apply : ∀ {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} (x : (i : ι) → E i) (i : ι),
  (WithCStarModule.equiv A ((i : ι) → E i)).symm x i = x i
-- Mathlib.Order.JordanHolder
CompositionSeries.lt_succ : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X) (i : Fin s.length),
  s.toFun i.castSucc < s.toFun i.succ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Filter.Tendsto.arcsin : ∀ {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto (fun x => Real.arcsin (f x)) l (nhds (Real.arcsin x))
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The limit cone for the product with a zero object.  -/
CategoryTheory.Limits.binaryFanZeroRight : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → CategoryTheory.Limits.BinaryFan X 0
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_id : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A], ⇑(CoalgHom.id R A) = id
-- Init.Data.Array.Lemmas
Array.append_singleton_assoc : ∀ {α : Type u_1} {a : α} {xs ys : Array α}, xs ++ (#[a] ++ ys) = xs.push a ++ ys
-- Mathlib.Data.Fin.SuccPred
Fin.eq_castSucc_of_ne_last : ∀ {n : ℕ} {x : Fin (n + 1)}, x ≠ Fin.last n → ∃ y, y.castSucc = x
-- Mathlib.Tactic.NormNum.Abs
Mathlib.Meta.NormNum.isNat_abs_neg : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : Lattice α] [IsOrderedRing α] {a : α} {na : ℕ},
  Mathlib.Meta.NormNum.IsInt a (Int.negOfNat na) → Mathlib.Meta.NormNum.IsNat |a| na
-- Mathlib.Topology.Perfect
/-- A set `C` is preperfect if all of its points are accumulation points of itself.
If `α` is a T1 space, this is equivalent to the closure of `C` being perfect,
see `preperfect_iff_perfect_closure`. This property is also called dense-in-itself.  -/
Preperfect : {α : Type u_1} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.GroupTheory.PresentedGroup
_private.Mathlib.GroupTheory.PresentedGroup.0.PresentedGroup.termF : Lean.ParserDescr
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.vadd_ae : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G),
  c +ᵥ MeasureTheory.ae μ = MeasureTheory.ae μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_alter_eq_add_one : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)}, k ∉ t → (f (t.get? k)).isSome = true → (t.alter k f).size = t.size + 1
-- Mathlib.LinearAlgebra.Dual.Basis
/-- `h.toDualFlip v` is the linear map sending `w` to `h.toDual w v`.  -/
Module.Basis.toDualFlip : {R : Type uR} →
  {M : Type uM} →
    {ι : Type uι} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [DecidableEq ι] → Module.Basis ι R M → M → M →ₗ[R] R
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The morphism between `M`'s monoidal category and `N`'s monoidal category  -/
Bimod.Hom.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : CategoryTheory.Mon C} → {M N : Bimod A B} → M.Hom N → (M.X ⟶ N.X)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- If a `Cofan` is colimit, then its opposite is limit.  -/
CategoryTheory.Limits.Cofan.IsColimit.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} →
      {Z : α → C} →
        {c : CategoryTheory.Limits.Cofan Z} → CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsLimit c.op
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add_one : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ), x ^ (y + 1) = x ^ y * x
-- Mathlib.Topology.Filter
/-- The topology on `Filter α` is generated by the sets `Set.Iic (𝓟 s) = {l : Filter α | s ∈ l}`,
`s : Set α`. A set `s : Set (Filter α)` is open if and only if it is a union of a family of these
basic open sets, see `Filter.isOpen_iff`.  -/
Filter.instTopologicalSpace : {α : Type u_2} → TopologicalSpace (Filter α)
-- Batteries.Data.ByteArray
_private.Batteries.Data.ByteArray.0.ByteArray.get.match_1.splitter : (motive : (x : ByteArray) → (x_1 : ℕ) → x_1 < x.size → Sort u_1) →
  (x : ByteArray) →
    (x_1 : ℕ) →
      (x_2 : x_1 < x.size) →
        ((bs : Array UInt8) → (i : ℕ) → (x : i < { data := bs }.size) → motive { data := bs } i x) → motive x x_1 x_2
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G) (j : J),
  CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom (t.π.app j) =
    CategoryTheory.CategoryStruct.comp (s.π.app j) (w.hom.app j)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `f : α →ᵤ[𝔖] β` is continuous at `x` and `x` admits a neighbourhood `V ∈ 𝔖`,
then evaluation of `g : α →ᵤ[𝔖] β` at `y : α` is continuous in `(g, y)` at `(f, x)`.  -/
UniformOnFun.continuousAt_eval₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : TopologicalSpace α]
  {f : UniformOnFun α β 𝔖} {x : α},
  (∃ V ∈ 𝔖, V ∈ nhds x) →
    ContinuousAt ((UniformOnFun.toFun 𝔖) f) x → ContinuousAt (fun fx => (UniformOnFun.toFun 𝔖) fx.1 fx.2) (f, x)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Icc_castLE : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.Icc (Fin.castLE h a) (Fin.castLE h b), f i = ∑ i ∈ Finset.Icc a b, f (Fin.castLE h i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, k ∉ t → (f t[k]?).isNone = true → (t.alter k f).size = t.size
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCompletionItem : Hashable Lean.Lsp.CompletionItem
-- Init.Data.Bool
/-- Boolean “exclusive or”. `xor x y` can be written `x ^^ y`.

`x ^^ y` is `true` when precisely one of `x` or `y` is `true`. Unlike `and` and `or`, it does not
have short-circuiting behavior, because one argument's value never determines the final value. Also
unlike `and` and `or`, there is no commonly-used corresponding propositional connective.

Examples:
 * `false ^^ false = false`
 * `true ^^ false = true`
 * `false ^^ true = true`
 * `true ^^ true = false`


Conventions for notations in identifiers:

 * The recommended spelling of `^^` in identifiers is `xor`. -/
Bool.«term_^^_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.distortion.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι),
  I.distortion = Finset.univ.sup fun i => nndist I.lower I.upper / nndist (I.lower i) (I.upper i)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toCoalgHom_eq_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (f : A ≃ₗc[R] B), f.toCoalgHom = ↑f