mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.toModuleCat_tensor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] (X Y : QuadraticModuleCat R),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).toModuleCat =
    CategoryTheory.MonoidalCategoryStruct.tensorObj X.toModuleCat Y.toModuleCat
-- Init.Data.List.Scan.Lemmas
List.scanr_ne_nil : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β}, List.scanr f b l ≠ []
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Node.id.inj : ∀ {a a_1 : Mathlib.Tactic.Widget.StringDiagram.IdNode},
  Mathlib.Tactic.Widget.StringDiagram.Node.id a = Mathlib.Tactic.Widget.StringDiagram.Node.id a_1 → a = a_1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.AddMon C),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- The exterior derivative of a `0`-form given by a function `f` within a set
is the 1-form given by the derivative of `f` within the set.  -/
extDerivWithin_constOfIsEmpty : ∀ {𝕜 : 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] {s : Set E} {x : E} (f : E → F),
  UniqueDiffWithinAt 𝕜 s x →
    extDerivWithin (fun x => ContinuousAlternatingMap.constOfIsEmpty 𝕜 E (Fin 0) (f x)) s x =
      (ContinuousAlternatingMap.ofSubsingleton 𝕜 E F 0) (fderivWithin 𝕜 f s x)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_lt_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommSemiring α] [inst_2 : PartialOrder α] [OrderBot α]
  [inst_4 : CanonicallyOrderedAdd α] [PosMulStrictMono α] {a₁ a₂ b₁ b₂ : WithTop α},
  a₁ < a₂ → b₁ < b₂ → a₁ * b₁ < a₂ * b₂
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.toPartialEquiv : {X : Type u_7} →
  {Y : Type u_8} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → PartialHomeomorph X Y → PartialEquiv X Y
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.comap_equiv_top : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (f : G →g H), SimpleGraph.Subgraph.comap f ⊤ = ⊤
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The index type for the relations in the standard presentation of `⋀[R]^n M`,
in the particular case `ι` is `Fin n`.  -/
exteriorPower.presentation.Rels : Type u → Type u_4 → Type u_5 → Type (max (max u u_4) u_5)
-- Init.Data.SInt.Lemmas
Int8.toInt_div : ∀ (a b : Int8), (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 8)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.below : {ρ : Type} →
  {pat : ρ} →
    [inst : String.Slice.Pattern.Model.PatternModel pat] →
      {s : String.Slice} →
        {motive :
            (a : s.Pos) →
              (a_1 : List (String.Slice.Pattern.SearchStep s)) →
                String.Slice.Pattern.Model.IsValidRevSearchFrom pat a a_1 → Prop} →
          {a : s.Pos} →
            {a_1 : List (String.Slice.Pattern.SearchStep s)} →
              String.Slice.Pattern.Model.IsValidRevSearchFrom pat a a_1 → Prop
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.rotate_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C), T.rotate.mor₂ = T.mor₃
-- Mathlib.Algebra.Algebra.Basic
ULift.algebra : {R : Type u_1} →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra R (ULift.{u_4, u_2} A)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.instSymmFinsetIsUniform : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {G : SimpleGraph α}
  [inst_2 : DecidableRel G.Adj] {ε : 𝕜}, Std.Symm (G.IsUniform ε)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRootsFinset_def : ∀ (n : ℕ) {R : Type u_1} (a : R) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R],
  Polynomial.nthRootsFinset n a = (Polynomial.nthRoots n a).toFinset
-- Mathlib.Computability.Primrec.List
Primrec.list_cons : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ List.cons
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_deriv_norm : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (n : ℕ),
  ‖(Polynomial.aeval (newton_seq_gen✝ hnorm n)) (Polynomial.derivative F)‖ =
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Const.getD (Std.DTreeMap.Const.insertMany t l) k fallback = Std.DTreeMap.Const.getD t k fallback
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFiniteType : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.LocallyOfFiniteType
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.Arrows.Compatible.familyOfElements.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C}
  {I : Type u_1} {X : I → C} {π π_1 : (i : I) → X i ⟶ B} (e_π : π = π_1) {x x_1 : (i : I) → P.obj (Opposite.op (X i))}
  (e_x : x = x_1) (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) ⦃Y : C⦄ (f f_1 : Y ⟶ B) (e_f : f = f_1)
  (a : CategoryTheory.Presieve.ofArrows X π f), hx.familyOfElements f a = ⋯.familyOfElements f_1 ⋯
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Given a function `m : Set X → ℝ≥0∞`, `mkMetric' m` is the supremum of `mkMetric'.pre m r`
over `r > 0`. Equivalently, it is the limit of `mkMetric'.pre m r` as `r` tends to zero from
the right.  -/
MeasureTheory.OuterMeasure.mkMetric' : {X : Type u_2} → [EMetricSpace X] → (Set X → ENNReal) → MeasureTheory.OuterMeasure X
-- Init.Data.Array.Basic
/-- Removes the element at a given index from an array. Does nothing if the index is out of bounds.

This function takes worst-case `O(n)` time because it back-shifts all elements at positions greater
than `i`.

Examples:
* `#["apple", "pear", "orange"].eraseIdxIfInBounds 0 = #["pear", "orange"]`
* `#["apple", "pear", "orange"].eraseIdxIfInBounds 1 = #["apple", "orange"]`
* `#["apple", "pear", "orange"].eraseIdxIfInBounds 2 = #["apple", "pear"]`
* `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
* `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
Array.eraseIdxIfInBounds : {α : Type u} → Array α → ℕ → Array α
-- Init.Data.Ord.BitVec
BitVec.instTransOrd : ∀ {n : ℕ}, Std.TransOrd (BitVec n)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_Ioo : ∀ {n : ℕ} (i j : Fin n), Fin.rev ⁻¹' Set.Ioo i j = Set.Ioo j.rev i.rev
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_roc : ∀ {m n k : ℕ}, Array.map (fun x => x + k) (m<...=n).toArray = ((m + k)<...=n + k).toArray
-- Mathlib.Order.Interval.Set.LinearOrder
Set.compl_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, (Set.Ioc a b)ᶜ = Set.Iic a ∪ Set.Ioi b
-- Init.Grind.Lemmas
Lean.Grind.decide_eq_false : ∀ {p : Prop} {x : Decidable p}, p = False → decide p = false
-- Std.Data.ExtTreeSet.Basic
/-- Transforms the tree set into an array of elements in ascending order.  -/
Std.ExtTreeSet.toArray : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → Array α
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_5.splitter : (C : Type u_2) →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    {x y : (CategoryTheory.WithInitial C)ᵒᵖ} →
      (motive : (x ⟶ y) → Sort u_3) →
        (x_1 : x ⟶ y) → ((f : Opposite.unop y ⟶ Opposite.unop x) → motive (Opposite.op f)) → motive x_1
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.del.eq_def : ∀ {α : Type u_1} (cut : α → Ordering) (x : RBTree.RBNode α),
  RBTree.RBNode.del cut x =
    match x with
    | RBTree.RBNode.nil => RBTree.RBNode.nil
    | RBTree.RBNode.node c a y b =>
      match cut y with
      | Ordering.lt =>
        match a.isBlack with
        | RBTree.RBColor.black => (RBTree.RBNode.del cut a).balLeft y b
        | RBTree.RBColor.red => RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.del cut a) y b
      | Ordering.gt =>
        match b.isBlack with
        | RBTree.RBColor.black => a.balRight y (RBTree.RBNode.del cut b)
        | RBTree.RBColor.red => RBTree.RBNode.node RBTree.RBColor.red a y (RBTree.RBNode.del cut b)
      | Ordering.eq => a.append b
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.lt : ℕ → ℕ → Lean.Expr → Mathlib.Tactic.Order.AtomicFact
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If `F` and `G` are right adjoints then `F ⋙ G` is a right adjoint too.  -/
CategoryTheory.Functor.isRightAdjoint_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D E} [F.IsRightAdjoint] [G.IsRightAdjoint], (F.comp G).IsRightAdjoint
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.normal : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], (alternatingGroup α).Normal
-- Init.Data.Array.Monadic
/-- We can express a for loop over an array which always yields as a fold.  -/
Array.forIn'_yield_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  (f : (a : α) → a ∈ xs → β → m γ) (g : (a : α) → a ∈ xs → β → γ → β) (init : β),
  (forIn' xs init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    Array.foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init xs.attach
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- (implementation) the associator for R-modules  -/
SemimoduleCat.MonoidalCategory.associator : {R : Type u} →
  [inst : CommSemiring R] →
    (M : SemimoduleCat R) →
      (N : SemimoduleCat R) →
        (K : SemimoduleCat R) →
          SemimoduleCat.MonoidalCategory.tensorObj (SemimoduleCat.MonoidalCategory.tensorObj M N) K ≅
            SemimoduleCat.MonoidalCategory.tensorObj M (SemimoduleCat.MonoidalCategory.tensorObj N K)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_zero : ∀ {α : Type u} [inst : AddMonoid α], ↑0 = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.eval : {α : Type u_1} → {β : Type u_2} → [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → (α → Bool) → β → Bool
-- Std.Time.Zoned.TimeZone
/-- A TimeZone structure that stores the timezone offset, the name, abbreviation and if it's in daylight
saving time.
 -/
Std.Time.TimeZone : Type
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.foldr_eq_foldr_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {f : α → δ → δ} {init : δ},
  Std.TreeSet.foldr f init t = Array.foldr f init t.toArray
-- Mathlib.Analysis.Complex.Basic
RCLike.re_eq_complex_re : ⇑RCLike.re = Complex.re
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt.injEq : ∀ (a b toIntThm : Lean.Expr) (lhs rhs : Int.Internal.Linear.Expr) (a_1 b_1 toIntThm_1 : Lean.Expr)
  (lhs_1 rhs_1 : Int.Internal.Linear.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt a b toIntThm lhs rhs =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt a_1 b_1 toIntThm_1 lhs_1 rhs_1) =
    (a = a_1 ∧ b = b_1 ∧ toIntThm = toIntThm_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Data.Nat.Prime.Defs
/-- **Alias** of the reverse direction of `Nat.prime_iff`. -/
Prime.nat_prime : ∀ {p : ℕ}, Prime p → Nat.Prime p
-- Aesop.Tree.Data
Aesop.GoalData.lastExpandedInIteration : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.Iteration
-- Mathlib.GroupTheory.Perm.Fin
isCycle_finRotate_of_le : ∀ {n : ℕ}, 2 ≤ n → (finRotate n).IsCycle
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousOn_continuousLinearMapCoordChange : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  {σ : 𝕜₁ →+* 𝕜₂} {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] {e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj}
  {e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : (x : B) → TopologicalSpace (E₂ x)] [inst_16 : FiberBundle F₂ E₂]
  [RingHomIsometric σ] [inst_18 : VectorBundle 𝕜₁ F₁ E₁] [inst_19 : VectorBundle 𝕜₂ F₂ E₂]
  [inst_20 : MemTrivializationAtlas e₁] [inst_21 : MemTrivializationAtlas e₁'] [inst_22 : MemTrivializationAtlas e₂]
  [inst_23 : MemTrivializationAtlas e₂'],
  ContinuousOn (Bundle.Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.exists_lt_omega0_opow' : ∀ {α : Sort u_1} {o b : Ordinal.{u_2}},
  1 < b →
    Order.IsSuccLimit o →
      ∀ {f : α → Ordinal.{u_2}},
        (∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i) → ∀ ⦃a : Ordinal.{u_2}⦄, a < b ^ o → ∃ i, a < b ^ f i
-- Mathlib.Analysis.InnerProductSpace.Calculus
OpenPartialHomeomorph.contDiff_unitBallBall : ∀ {n : ℕ∞} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {c : E} {r : ℝ} (hr : 0 < r),
  ContDiff ℝ ↑n ↑(OpenPartialHomeomorph.unitBallBall c r hr)
-- Mathlib.Algebra.Star.StarAlgHom
StarRingEquivClass.toStarRingEquiv.congr_simp : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Add A] [inst_1 : Mul A] [inst_2 : Star A] [inst_3 : Add B]
  [inst_4 : Mul B] [inst_5 : Star B] [inst_6 : EquivLike F A B] [inst_7 : StarRingEquivClass F A B] (f f_1 : F),
  f = f_1 → ↑f = ↑f_1
-- Mathlib.RingTheory.Adjoin.Singleton
Algebra.RingHom.adjoinAlgebraMap.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C]
  [inst_6 : IsScalarTower A B C] (b : B), Algebra.RingHom.adjoinAlgebraMap b = Algebra.RingHom.adjoinAlgebraMap b
-- Mathlib.Data.EReal.Operations
EReal.coe_zsmul : ∀ (n : ℤ) (x : ℝ), ↑(n • x) = n • ↑x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toList_toArray : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.edist_le_of_mem_pairSet : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
  1 < a → ↑J.card ≤ a ^ n → ∀ {s t : T}, (s, t) ∈ PairReduction.pairSet J a c → edist s t ≤ ↑n * c
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ⟶ Z) [inst_2 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.inv f))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
-- Init.Data.Option.Monadic
Option.forIn_yield_eq_elim : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option α)
  (f : α → β → m γ) (g : α → β → γ → β) (b : β),
  (forIn o b fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = o.elim (pure b) fun a => g a b <$> f a b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.tan_arccos : ∀ (x : ℝ), Real.tan (Real.arccos x) = √(1 - x ^ 2) / x
-- Init.Grind.ToInt
Lean.Grind.ToInt.wrap_toInt : ∀ {α : Type u_1} (I : Lean.Grind.IntInterval) [inst : Lean.Grind.ToInt α I] (x : α), I.wrap ↑x = ↑x
-- Mathlib.Computability.MyhillNerode
/-- **Myhill–Nerode theorem**. A language is regular if and only if the set of left quotients is finite.
 -/
Language.isRegular_iff_finite_range_leftQuotient : ∀ {α : Type u} {L : Language α}, L.IsRegular ↔ (Set.range L.leftQuotient).Finite
-- Mathlib.RingTheory.TensorProduct.Basic
/-- (Implementation detail)
The multiplication map on `A ⊗[R] B`,
as an `R`-bilinear map.
 -/
Algebra.TensorProduct.mul : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonUnitalNonAssocSemiring B] →
                  [inst_6 : Module R B] →
                    [SMulCommClass R B B] →
                      [IsScalarTower R B B] → TensorProduct R A B →ₗ[R] TensorProduct R A B →ₗ[R] TensorProduct R A B
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J K : C} (f : I ⟶ J) (g : J ⟶ K)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)]
  [inst_4 : CategoryTheory.ExponentiableMorphism f] [inst_5 : CategoryTheory.ExponentiableMorphism g]
  [inst_6 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.comp f g)]
  {Z : CategoryTheory.Functor (CategoryTheory.Over K) (CategoryTheory.Over K)}
  (h :
    (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.comp f g)).comp
        ((CategoryTheory.ExponentiableMorphism.pushforward f).comp
          (CategoryTheory.ExponentiableMorphism.pushforward g)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g)).unit
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.comp f g)).whiskerLeft
          (CategoryTheory.ExponentiableMorphism.pushforwardComp f g).hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g)).unit h
-- Init.Data.BitVec.Bootstrap
BitVec.ofNat_toNat : ∀ {n : ℕ} (m : ℕ) (x : BitVec n), BitVec.ofNat m x.toNat = BitVec.setWidth m x
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instAbelianSheafEtaleSmallEtaleTopology : {S : AlgebraicGeometry.Scheme} →
  {A : Type u'} →
    [inst : CategoryTheory.Category.{u, u'} A] →
      {FA : A → A → Type u_1} →
        {CD : A → Type u} →
          [inst_1 : (X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory A FA] →
              [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] →
                [CategoryTheory.Limits.HasColimits A] →
                  [CategoryTheory.Limits.HasLimits A] →
                    [(CategoryTheory.forget A).ReflectsIsomorphisms] →
                      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1}
                            (CategoryTheory.forget A)] →
                        [CategoryTheory.Abelian A] →
                          CategoryTheory.Abelian (CategoryTheory.Sheaf S.smallEtaleTopology A)
-- Init.Data.UInt.Lemmas
UInt16.neg_neg : ∀ {a : UInt16}, - -a = a
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.right'_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.MonoidalCoherence X Y],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCoherence.iso ≪≫ (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).symm
-- Mathlib.Topology.Algebra.Group.Basic
instContinuousConstSMulConjActOfSeparatelyContinuousMul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G],
  ContinuousConstSMul (ConjAct G) G
-- Lean.Parser.Syntax
Lean.Parser.Command.macroArg.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Filter.Lift
/-- If `(p : ι → Prop, s : ι → Set α)` is a basis of a filter `f`, `g` is a monotone function
`Set α → Filter γ`, and for each `i`, `(pg : β i → Prop, sg : β i → Set α)` is a basis
of the filter `g (s i)`, then
`(fun (i : ι) (x : β i) ↦ p i ∧ pg i x, fun (i : ι) (x : β i) ↦ sg i x)`
is a basis of the filter `f.lift g`.

This basis is parametrized by `i : ι` and `x : β i`, so in order to formulate this fact using
`has_basis` one has to use `Σ i, β i` as the index type. See also `Filter.HasBasis.mem_lift_iff`
for the corresponding `mem_iff` statement formulated without using a sigma type.  -/
Filter.HasBasis.lift : ∀ {α : Type u_1} {γ : Type u_3} {ι : Type u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α},
  f.HasBasis p s →
    ∀ {β : ι → Type u_5} {pg : (i : ι) → β i → Prop} {sg : (i : ι) → β i → Set γ} {g : Set α → Filter γ},
      (∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)) →
        Monotone g → (f.lift g).HasBasis (fun i => p i.fst ∧ pg i.fst i.snd) fun i => sg i.fst i.snd
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.symm_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.symm.h₀ = -h.h₀
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.map_iConvexComb : ∀ {R : Type u_1} {I : Type u_6} {J : Type u_7} {K : Type u_8} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] {f : J → K} (s : Convexity.StdSimplex R I) (g : I → Convexity.StdSimplex R J),
  Convexity.StdSimplex.map f (Convexity.iConvexComb s g) = Convexity.iConvexComb s (Convexity.StdSimplex.map f ∘ g)
-- Batteries.CodeAction.Misc
/-- Invoking hole code action "Start a tactic proof" will fill in a hole with `by done`.  -/
Batteries.CodeAction.startTacticStub : Lean.CodeAction.HoleCodeAction
-- Mathlib.Data.PNat.Factors
/-- **Alias** of the reverse direction of `PrimeMultiset.prod_dvd_iff`. -/
PrimeMultiset.prod_dvd_prod : ∀ {u v : PrimeMultiset}, u ≤ v → u.prod ∣ v.prod