mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t ≠ ∅}, (cmp (t.maxKey he) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.left_unitor_inv_hom : ∀ {B : Type u} [inst : Quiver B] {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f).vcomp (CategoryTheory.FreeBicategory.Hom₂.left_unitor f))
    (CategoryTheory.FreeBicategory.Hom₂.id f)
-- Mathlib.Tactic.ITauto
/-- `(p: ⊥) ⊢ A`  -/
Mathlib.Tactic.ITauto.Proof.exfalso' : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Batteries.Classes.Order
Std.LawfulCmp.toLawfulLTCmp : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] {cmp : α → α → Ordering} [self : Std.LawfulCmp cmp], Std.LawfulLTCmp cmp
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.id_hom : ∀ (X : FintypeCat), CategoryTheory.CategoryStruct.id X.obj = TypeCat.ofHom id
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcompose_map_hom : ∀ {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} (α : F ⟶ G) {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y),
  ((CategoryTheory.Limits.Cone.postcompose α).map f).hom = f.hom
-- Mathlib.Data.Nat.Bits
Nat.bitCasesOn_bit0 : ∀ {motive : ℕ → Sort u} (H : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)) (n : ℕ), Nat.bitCasesOn (2 * n) H = H false n
-- Mathlib.Algebra.Quandle
Rack.toEnvelGroup.mapAux.eq_4 : ∀ {R : Type u_1} [inst : Rack R] {G : Type u_2} [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G))
  (a : Rack.PreEnvelGroup R), Rack.toEnvelGroup.mapAux f a.inv = (Rack.toEnvelGroup.mapAux f a)⁻¹
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- `e C i` is the locally constant map from `C : Set (I → Bool)` to `ℤ` sending `f` to 1 if
`f.val i = true`, and 0 otherwise.
 -/
Profinite.NobelingProof.e : {I : Type u} → (C : Set (I → Bool)) → I → LocallyConstant ↑C ℤ
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.re_complexMGF_ofReal : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (x : ℝ),
  (ProbabilityTheory.complexMGF X μ ↑x).re = ProbabilityTheory.mgf X μ x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.inc.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (n : ℕ) (check persistent : Bool)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_11),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h) =
    1 + sizeOf fvarId + sizeOf n + sizeOf check + sizeOf persistent + sizeOf h
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Pasting two pushout cocones vertically is isomorphic to the pushout cocone obtained by flipping
them, pasting horizontally, and then flipping the result again.  -/
CategoryTheory.Limits.PushoutCocone.pasteVertFlip : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y₃ Y₂ Y₁ X₃ : C} →
      {g₂ : Y₃ ⟶ Y₂} →
        {g₁ : Y₂ ⟶ Y₁} →
          {i₃ : Y₃ ⟶ X₃} →
            (t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃) →
              {i₂ : Y₂ ⟶ t₁.pt} →
                (t₂ : CategoryTheory.Limits.PushoutCocone g₁ i₂) →
                  (hi₂ : i₂ = t₁.inl) → (t₁.pasteVert t₂ hi₂).flip ≅ t₁.flip.pasteHoriz t₂.flip hi₂
-- Mathlib.Algebra.FreeAlgebra
/-- An inductively defined relation on `Pre R X` used to force the initial algebra structure on
the associated quotient.
 -/
FreeAlgebra.Rel : (R : Type u_1) → (X : Type u_2) → [CommSemiring R] → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X → Prop
-- Mathlib.ModelTheory.Syntax
/-- The sentence indicating that a basic relation symbol is total.  -/
FirstOrder.Language.Relations.total : {L : FirstOrder.Language} → L.Relations 2 → L.Sentence
-- Init.Data.BitVec.Basic
BitVec.udiv_eq : ∀ {w : ℕ} (x y : BitVec w), x.udiv y = x / y
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.mkOrderEmbedding.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α}
  (b : ↥s), Localization.mkOrderEmbedding b = { toFun := fun a => Localization.mk a b, inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_empty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ}, Dynamics.netMaxcard T ∅ U n = 0
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isCompl_range_coe_infty : ∀ {X : Type u_1}, IsCompl (Set.range OnePoint.some) {OnePoint.infty}
-- Mathlib.Algebra.Free
/-- The embedding `α → FreeSemigroup α`.  -/
FreeSemigroup.of : {α : Type u} → α → FreeSemigroup α
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Technical lemma to rewrite suitably the preimage of an intersection under an extended chart, to
bring it into a convenient form to apply derivative lemmas.  -/
OpenPartialHomeomorph.extend_preimage_inter_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s t : Set M},
  ↑(f.extend I).symm ⁻¹' (s ∩ t) ∩ Set.range ↑I = ↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I ∩ ↑(f.extend I).symm ⁻¹' t
-- Mathlib.Tactic.IntervalCases
/-- The numeric value of the target expression  -/
Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal.value : Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal → ℤ
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountablyGenerated.isCountablyGenerated : ∀ {α : Type u_3} {m : MeasurableSpace α} [self : MeasurableSpace.CountablyGenerated α],
  ∃ b, b.Countable ∧ m = MeasurableSpace.generateFrom b
-- Mathlib.Data.Finset.Sups
Finset.compls_subset_iff : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s t : Finset α}, s.compls ⊆ t ↔ s ⊆ t.compls
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {c : ℕ}, (Std.HashSet.Raw.emptyWithCapacity c).WF
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.vertex_coe : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X]
  [inst_3 : IsOrderedRing S] [inst_4 : DecidableEq X] (x : X), ⇑(stdSimplex.vertex x) = Pi.single x 1
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.comp_right_injective : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (e : M ≃* N), Function.Injective fun f => (↑e).comp f
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_inf_le : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N N₂ : LieSubmodule R L M},
  LieSubmodule.map f (N ⊓ N₂) ≤ LieSubmodule.map f N ⊓ LieSubmodule.map f N₂
-- Lean.ReservedNameAction
_private.Lean.ReservedNameAction.0.Lean.reservedNameActionsRef : IO.Ref (Array Lean.ReservedNameAction)
-- Init.Grind.Lemmas
Lean.Grind.Bool.false_of_not_eq_self : ∀ {a : Bool}, (!a) = a → False
-- Mathlib.Order.Category.BddOrd
BddOrd.Iso.mk_inv : ∀ {α β : BddOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd), (BddOrd.Iso.mk e).inv = BddOrd.ofHom ↑e.symm
-- Mathlib.Topology.ContinuousMap.Star
/-- `ContinuousMap.compStarAlgHom` sends the identity `StarAlgHom` on `A` to the identity
`StarAlgHom` on `C(X, A)`.  -/
ContinuousMap.compStarAlgHom_id : ∀ (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} [inst : TopologicalSpace X] [inst_1 : CommSemiring 𝕜]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : IsTopologicalSemiring A] [inst_5 : Star A]
  [inst_6 : ContinuousStar A] [inst_7 : Algebra 𝕜 A],
  ContinuousMap.compStarAlgHom X (StarAlgHom.id 𝕜 A) ⋯ = StarAlgHom.id 𝕜 C(X, A)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.transfer : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {H : SimpleGraph V} {q : G.Walk u u},
  q.IsCycle → ∀ (hq : ∀ e ∈ q.edges, e ∈ H.edgeSet), (q.transfer H hq).IsCycle
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
/-- The equivalence of categories between monoids internal to `C`
and monoids internal to the monoidal opposite of `C` lies over
the equivalence `C ≌ Cᴹᵒᵖ` via the forgetful functors.  -/
MonObj.mopEquivCompForgetIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (MonObj.mopEquiv C).functor.comp (CategoryTheory.Mon.forget Cᴹᵒᵖ) ≅
        (CategoryTheory.Mon.forget C).comp (CategoryTheory.MonoidalOpposite.mopEquiv C).functor
-- Std.Data.TreeMap.Raw.Basic
/-- Returns the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.TreeMap.Raw.keyAtIdx! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap.Raw α β cmp → ℕ → α
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.supDegree_pow : ∀ {R : Type u_1} [inst : Semiring R] {A : Type u_8} {B : Type u_9} [inst_1 : AddMonoid A] [inst_2 : AddMonoid B]
  [inst_3 : LinearOrder B] [inst_4 : OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B}
  {p : AddMonoidAlgebra R A} {n : ℕ},
  D 0 = 0 →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      Function.Injective D →
        ∀ [Nontrivial R],
          AddMonoidAlgebra.Monic D p → AddMonoidAlgebra.supDegree D (p ^ n) = n • AddMonoidAlgebra.supDegree D p
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.hasLeftCalculusOfFractions' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  [F.Full] [F.Faithful] (adj : G ⊣ F),
  ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G).HasLeftCalculusOfFractions
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The flip of a pullback square is a pullback square.  -/
CategoryTheory.Limits.PullbackCone.flipIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {t : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsLimit t → CategoryTheory.Limits.IsLimit t.flip
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'.go.induct_unfolding : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α)
  (motive : Lean.Grind.CommRing.Poly → α → α → Prop),
  (∀ (acc : α), motive (Lean.Grind.CommRing.Poly.num 0) acc acc) →
    (∀ (acc : α) (k : ℤ), (k = 0 → False) → motive (Lean.Grind.CommRing.Poly.num k) acc (acc + ↑k)) →
      (∀ (acc : α) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
          motive p (acc + Lean.Grind.CommRing.denoteTerm ctx k m)
              (Lean.Grind.CommRing.Poly.denote'.go ctx p (acc + Lean.Grind.CommRing.denoteTerm ctx k m)) →
            motive (Lean.Grind.CommRing.Poly.add k m p) acc
              (Lean.Grind.CommRing.Poly.denote'.go ctx p (acc + Lean.Grind.CommRing.denoteTerm ctx k m))) →
        ∀ (p : Lean.Grind.CommRing.Poly) (acc : α), motive p acc (Lean.Grind.CommRing.Poly.denote'.go ctx p acc)
-- Mathlib.Data.Ordmap.Ordset
Ordset.mem.decidable : {α : Type u_1} → [inst : Preorder α] → [inst_1 : DecidableLE α] → (x : α) → (s : Ordset α) → Decidable (x ∈ s)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} [inst_1 : Inhabited (β k)],
  (Std.DTreeMap.filter f t).get! k = (Option.filter (f k) (t.get? k)).get!
-- Mathlib.Data.Set.Order
Set.monotone_ofPred : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {p : α → β → Prop},
  (∀ (b : β), Monotone fun a => p a b) → Monotone fun a => {b | p a b}
-- Mathlib.Analysis.Calculus.FDeriv.Const
HasCompactSupport.fderiv : ∀ (𝕜 : 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] {f : E → F}, HasCompactSupport f → HasCompactSupport (fderiv 𝕜 f)
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.pentagon_inv_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (W X Y Z : C) {Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) Z ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
          (CategoryTheory.CategoryStruct.id Z))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
              Z).inv
          h))
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.Hom.id : {J : Type w} → (X : CategoryTheory.Limits.WidePullbackShape J) → X.Hom X
-- Init.Data.SInt.Basic
/-- Strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `<` operator.
 -/
Int8.lt : Int8 → Int8 → Prop
-- Batteries.Data.AssocList
Batteries.AssocList.mapVal.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ),
  Batteries.AssocList.mapVal f Batteries.AssocList.nil = Batteries.AssocList.nil
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_smul : ∀ {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : SMul S R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃),
  (s • a).re = s • a.re
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_le_edist_of_mem : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} {x : α}, x ∈ s → ∀ {y : α}, y ∈ s → x ≠ y → s.einfsep ≤ edist x y
-- Mathlib.Algebra.Order.Archimedean.Class
/-- The upper set in `ArchimedeanClass M` consisting of an upper set in
`FiniteArchimedeanClass M` plus `⊤`.  -/
FiniteArchimedeanClass.toUpperSetAddArchimedeanClass : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] → UpperSet (FiniteArchimedeanClass M) ↪o UpperSet (ArchimedeanClass M)
-- Mathlib.Util.AtomM
/-- If an atomic expression has already been encountered, return `true`, the index and the stored
form of the atom (which will be defeq at the specified transparency, but not necessarily
syntactically equal). If the atomic expression has *not* already been encountered, store it in the
list of atoms, and return the new index (and the stored form of the atom, which will be itself).

In a normalizing tactic, the expression returned by `containsThenAdd` should be considered
the normal form.
 -/
Mathlib.Tactic.AtomM.containsThenAdd : Lean.Expr → Mathlib.Tactic.AtomM (Bool × ℕ × Lean.Expr)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.mk : ℕ →
  Lean.Expr →
    Lean.Level →
      Lean.Expr →
        Lean.Expr →
          Option (Lean.Expr × ℕ) →
            Option Lean.Expr →
              Option Lean.Expr →
                Option Lean.Expr →
                  Option Lean.Expr →
                    Option Lean.Expr →
                      Option Lean.Expr →
                        Option Lean.Expr →
                          Option Lean.Expr →
                            Lean.PArray Lean.Expr →
                              Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var →
                                Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr →
                                  Lean.Meta.Grind.Arith.CommRing.Ring
-- Mathlib.CategoryTheory.PUnit
/-- Any two functors to `Discrete PUnit` are *equal*.
You probably want to use `punitExt` instead of this.  -/
CategoryTheory.Functor.punit_ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1})), F = G
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.succMany? pref.size Std.PRange.UpwardEnumerable.least).get ⋯
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `continuousOn_finsetProd`. -/
continuousOn_finset_prod : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Finset ι) {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∏ i ∈ s, f i a) t
-- Mathlib.Order.Filter.Prod
Filter.Eventually.diag_of_prod_right : ∀ {α : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter γ} {p : α × γ × γ → Prop},
  (∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
-- Lean.Meta.Tactic.TryThis
/-- Add term suggestions.

The parameters are:
* `ref`: the span of the widget diagnostic
* `es`: an array of the replacement expressions
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
  If not provided it defaults to `ref`.
* `header`: a string which precedes the list of suggestions. By default, it's `"Try these:"`.
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
  used.
 -/
Lean.Meta.Tactic.TryThis.addTermSuggestions : Lean.Syntax →
  Array Lean.Expr →
    optParam (Option Lean.Syntax) none → optParam String "Try these:" → optParam (Option String) none → Lean.MetaM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.stdSimplex.ext₀ : ∀ {X : SSet} {f g : X ⟶ SSet.stdSimplex.obj { len := 0 }}, f = g
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_uInt16ToBitVec : ∀ (x : UInt16), Int16.ofBitVec x.toBitVec = x.toInt16
-- Batteries.Data.Array.Merge
/-- `O(|xs| log |xs|)`. Sort and deduplicate an array.  -/
Array.sortDedup : {α : Type u_1} → [ord : Ord α] → Array α → Array α
-- Batteries.Data.Fin.Lemmas
Fin.divNat_mkDivMod : ∀ {m n : ℕ} (i : Fin m) (j : Fin n), (i.mkDivMod j).divNat = i
-- Mathlib.Algebra.DirectSum.Basic
DFinsupp.liftAddHom.eq_1 : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ],
  DFinsupp.liftAddHom =
    { toFun := DFinsupp.sumAddHom, invFun := fun F i => F.comp (DFinsupp.singleAddHom β i), left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_bijective_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.Bijective ⇑(AdicCompletion.of I M) ↔ IsAdicComplete I M
-- Mathlib.Data.Int.Bitwise
/-- `Int.natBitwise` is an auxiliary definition for `Int.bitwise`.  -/
Int.natBitwise : (Bool → Bool → Bool) → ℕ → ℕ → ℤ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) {β β' : b ⟶ c}
  (y : β ⟶ β'),
  (CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft α y).τl = CategoryTheory.Bicategory.whiskerLeft α.l y.τl
-- Mathlib.Analysis.Seminorm
Seminorm.continuous_of_continuousAt_zero : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E}, ContinuousAt (⇑p) 0 → Continuous ⇑p
-- Mathlib.RingTheory.Ideal.Over
Ideal.over_def : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [P.LiesOver p], p = Ideal.under A P
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.IsLocallyFreeData.shrink : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.LocalGeneratorsData) [q.IsLocallyFreeData], q.shrink.IsLocallyFreeData
-- Mathlib.LinearAlgebra.Eigenspace.Charpoly
Module.End.mem_spectrum_iff_isRoot_charpoly : ∀ {K : Type u_3} {V : Type u_4} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : Module.Finite K V] (f : Module.End K V) (μ : K), μ ∈ spectrum K f ↔ (LinearMap.charpoly f).IsRoot μ
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A bounded variation function tends to its right-limit on its right.  -/
BoundedVariationOn.tendsto_rightLim : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : α → E},
  BoundedVariationOn f Set.univ → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (Function.rightLim f x))
-- Mathlib.Data.Seq.Defs
Stream'.Seq.get?_tail : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), s.tail.get? n = s.get? (n + 1)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- This lemma demonstrates the relation between `Equiv.Perm.IsCycle` and `Equiv.Perm.IsCycleOn`
in non-degenerate cases.  -/
Equiv.Perm.isCycle_iff_exists_isCycleOn : ∀ {α : Type u_2} {f : Equiv.Perm α},
  f.IsCycle ↔ ∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬Function.IsFixedPt (⇑f) x → x ∈ s
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.isHole : Lean.Syntax → Bool
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_le_restrict_range : ∀ {α : Type u_1} {β : Type u_3} {ma : MeasureTheory.OuterMeasure α} {mb : MeasureTheory.OuterMeasure β} {f : α → β},
  (MeasureTheory.OuterMeasure.map f) ma ≤ (MeasureTheory.OuterMeasure.restrict (Set.range f)) mb ↔
    (MeasureTheory.OuterMeasure.map f) ma ≤ mb
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_lt_eq_self : ∀ (a : ENNReal), ⨆ b, ⨆ (_ : b < a), b = a
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- If the image of a family of vectors under a linear map is linearly independent, then so is
the original family.  -/
LinearIndependent.of_comp : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  LinearIndependent R (⇑f ∘ v) → LinearIndependent R v
-- Mathlib.Order.Filter.Basic
Filter.iSup_neBot : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α}, (⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot