mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Basic
/-- An iterator that sequentially emits values of type `β` in the monad `m`. It may be finite
or infinite.

See the root module `Std.Data.Iterators` for a more comprehensive overview over the iterator
framework.

See `Std.Data.Iterators.Producers` for ways to iterate over common data structures.
By convention, the monadic iterator associated with an object can be obtained via dot notation.
For example, `List.iterM IO` creates an iterator over a list in the monad `IO`.

See `Init.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
convert an iterator `it` into a list and `it.ensureTermination.toList` guarantees that this
operation will terminate, given a proof that the iterator is finite.
It is also always possible to manually iterate using
`it.step`, relying on the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.

See `Iter` for a more convenient interface in case that no monadic effects are needed (`m = Id`).

Internally, `IterM m β` wraps an element of type `α` containing state information.
The type `α` determines the implementation of the iterator using a typeclass mechanism.
The concrete typeclass implementing the iterator is `Iterator α m β`.

When using combinators, `α` can become very complicated. It is an implicit parameter
of `α` so that the pretty printer will not print this large type by default. If a declaration
returns an iterator, the following will not work:

```lean
def x : IterM IO Nat := [1, 2, 3].iterM IO
```

Instead the declaration type needs to be completely omitted:

```lean
def x := [1, 2, 3].iterM IO

-- if you want to ensure that `x` is an iterator in `IO` emitting `Nat`
def x := ([1, 2, 3].iterM IO : IterM IO Nat)
```
 -/
Std.IterM : {α : Type w} → (Type w → Type w') → Type w → Type w
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.disjointUnion_apply : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
  (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x ∈ e.source)]
  [inst_1 : (y : β) → Decidable (y ∈ e.target)], ↑(e.disjointUnion e' hs ht) = e.source.piecewise ↑e ↑e'
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.finrank_cotangentSpace_le_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) ≤ 1 ↔
    Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The counit of the constructed pointwise right Kan extension when
`HasPointwiseRightKanExtension L F` holds.  -/
CategoryTheory.Functor.pointwiseRightKanExtensionCounit : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseRightKanExtension F] → L.comp (L.pointwiseRightKanExtension F) ⟶ F
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- Equivalence relation identifying vertices connected by directed paths in both directions.  -/
Quiver.stronglyConnectedSetoid : (V : Type u_2) → [Quiver V] → Setoid V
-- Batteries.Data.List.Basic
List.zipWithLeftTR.go.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : List α) (a_1 : Array γ),
  (a = [] → False) → List.zipWithLeftTR.go f a [] a_1 = (List.foldl (fun acc a => acc.push (f a none)) a_1 a).toList
-- Mathlib.Data.Seq.Defs
Stream'.Seq.cons_not_terminatedAt_zero : ∀ {α : Type u} {x : α} {s : Stream'.Seq α}, ¬(Stream'.Seq.cons x s).TerminatedAt 0
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_mem_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, k ∈ m.toList → k ∈ m
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_keys_unit_perm : ∀ {α : Type u} {m₁ m₂ : Std.DHashMap.Raw α fun x => Unit}, m₁.keys.Perm m₂.keys → m₁.Equiv m₂
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_id : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : N), (f.lift ⋯) x = x
-- Mathlib.Data.Rat.Lemmas
Rat.num_dvd : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → (Rat.divInt a b).num ∣ a
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.μ_natural_left_assoc : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h :
    (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map f)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X₂ Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X₁ Y).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))
        h)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_congr : ∀ {r s : ENNReal}, (∀ (n : ℕ∞), r ≤ ↑n ↔ s ≤ ↑n) → ⌈r⌉ₑ = ⌈s⌉ₑ
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.isWF : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.IsPWO → s.IsWF
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.isUnit_basicOpen : ∀ {R : Type u} [inst : CommRing R] (f : R),
  IsUnit
    ((algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) f)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.toContinuousLinearMap_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i),
  (f.toContinuousLinearMap m i) x = f (Function.update m i x)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivAt.eq_1 : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : M → M') (x : M)
  (f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)),
  HasMFDerivAt% f x f' =
    (ContinuousAt f x ∧ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (Set.range ↑I) (↑(extChartAt I x) x))
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.Pos.find?_bool_eq_none_iff_of_splits : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} {t u : String},
  pos.Splits t u → (pos.find? p = none ↔ ∀ c ∈ u.toList, p c = false)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_le : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {p : Submodule R M}, Submodule.span R s ≤ p ↔ s ⊆ ↑p
-- Mathlib.Data.Nat.Factorization.PrimePow
isPrimePow_iff_card_primeFactors_eq_one : ∀ {n : ℕ}, IsPrimePow n ↔ n.primeFactors.card = 1
-- Init.Data.Array.Lemmas
Array.flatten_empty : ∀ {α : Type u_1}, #[].flatten = #[]
-- Init.Data.Nat.Lemmas
Nat.div_left_inj : ∀ {a b d : ℕ}, d ∣ a → d ∣ b → (a / d = b / d ↔ a = b)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.data_dropWhile : ∀ (p : Char → Bool) {s : Substring.Raw}, s.Valid → (s.dropWhile p).toString.toList = List.dropWhile p s.toString.toList
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.isLUB_sSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] (s : Set (WithTop α)), IsLUB s (sSup s)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.toComplex_ofComplex : ∀ (c : ℂ), CliffordAlgebraComplex.toComplex (CliffordAlgebraComplex.ofComplex c) = c
-- Mathlib.LinearAlgebra.Prod
LinearMap.fst_eq_coprod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.fst R M M₂ = LinearMap.id.coprod 0
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsInitial.mono_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.InitialMonoClass C] {I X : C}
  (hI : CategoryTheory.Limits.IsInitial I) (f : I ⟶ X), CategoryTheory.Mono f
-- Std.Time.Format.Modifier
Std.Time.Year.fourDigit.sizeOf_spec : sizeOf Std.Time.Year.fourDigit = 1
-- Mathlib.Data.Num.Lemmas
Num.cast_bit1 : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : Num), ↑n.bit1 = 2 * ↑n + 1
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.xa_mul_xa : ∀ {n : ℕ} (i j : ZMod (2 * n)), QuaternionGroup.xa i * QuaternionGroup.xa j = QuaternionGroup.a (↑n + j - i)
-- Mathlib.Order.Bounds.Basic
isGLB_congr : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α} {a : α}, lowerBounds s = lowerBounds t → (IsGLB s a ↔ IsGLB t a)
-- Mathlib.Topology.Algebra.Support
continuous_of_tsupport : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β] {f : α → β},
  (∀ x ∈ tsupport f, ContinuousAt f x) → Continuous f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_ofList_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  (Std.DTreeMap.ofList l cmp).inner.size ≤ l.length
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) [K₁.HasMapBifunctor K₂ F],
  K₁.HasMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F
-- Mathlib.Data.Set.Lattice
Set.iUnion_of_singleton_coe : ∀ {α : Type u_1} (s : Set α), ⋃ i, {↑i} = s
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ideal.quotOfMul.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (a : R) (I : Ideal R), Ideal.quotOfMul a I = Submodule.factor ⋯
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.norm_def : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)]
  (f : (i : ι) → G i), ‖f‖ = ↑(Finset.univ.sup fun b => ‖f b‖₊)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points not equal to `p`, the angle between the first and the third at `p` minus
the angle between the first and the second equals the angle between the second and the third.  -/
EuclideanGeometry.oangle_sub_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  p₁ ≠ p →
    p₂ ≠ p →
      p₃ ≠ p → EuclideanGeometry.oangle p₁ p p₃ - EuclideanGeometry.oangle p₁ p p₂ = EuclideanGeometry.oangle p₂ p p₃
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzero.congr_simp : ∀ {α : Type u} {x x_1 : WithZero α} (e_x : x = x_1) (a : x ≠ 0), WithZero.unzero a = WithZero.unzero ⋯
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.exists_edist_eq_eccent_of_finite : ∀ {α : Type u_1} {G : SimpleGraph α} [Finite α] (u : α), ∃ v, G.edist u v = G.eccent u
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for append on `BitVec`.  -/
BitVec.reduceAppend : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Equivalence.mk'.congr_simp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C)
  (unitIso unitIso_1 : CategoryTheory.Functor.id C ≅ functor.comp inverse) (e_unitIso : unitIso = unitIso_1)
  (counitIso counitIso_1 : inverse.comp functor ≅ CategoryTheory.Functor.id D) (e_counitIso : counitIso = counitIso_1)
  (functor_unitIso_comp :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) =
        CategoryTheory.CategoryStruct.id (functor.obj X)),
  { functor := functor, inverse := inverse, unitIso := unitIso, counitIso := counitIso,
      functor_unitIso_comp := functor_unitIso_comp } =
    { functor := functor, inverse := inverse, unitIso := unitIso_1, counitIso := counitIso_1,
      functor_unitIso_comp := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The morphism in `B` associated with the comonad.  -/
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.hom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → (m : CategoryTheory.Bicategory.OplaxTrans.ComonadBicat B) → m.obj ⟶ m.obj
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
/-- Implicit function `ψ : E₁ → E₂` associated with the (uncurried) bivariate function
`f : E₁ × E₂ → F` at `u : E₁ × E₂`.  -/
HasStrictFDerivAt.implicitFunctionOfProdDomain : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E₁ : Type u_2} →
      [inst_1 : NormedAddCommGroup E₁] →
        [inst_2 : NormedSpace 𝕜 E₁] →
          [CompleteSpace E₁] →
            {E₂ : Type u_3} →
              [inst_4 : NormedAddCommGroup E₂] →
                [inst_5 : NormedSpace 𝕜 E₂] →
                  [CompleteSpace E₂] →
                    {F : Type u_4} →
                      [inst_7 : NormedAddCommGroup F] →
                        [inst_8 : NormedSpace 𝕜 F] →
                          [CompleteSpace F] →
                            {u : E₁ × E₂} →
                              {f : E₁ × E₂ → F} →
                                {f'u : E₁ × E₂ →L[𝕜] F} →
                                  HasStrictFDerivAt f f'u u →
                                    (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible → E₁ → E₂
-- Aesop.Frontend.Extension
Aesop.Frontend.checkRuleSetNotDeclared : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [MonadLiftT IO m] → Aesop.RuleSetName → m Unit
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.beq_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  [inst_3 : (k : α) → BEq (β k)] {m₁ m₂ : Std.DHashMap.Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF),
  m₁.beq m₂ = Std.DHashMap.Internal.Raw₀.beq ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.convex_open_basis_zero : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [ZeroLEOneClass 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [LocallyConvexSpace 𝕜 E], (nhds 0).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) id
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k a : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).getKey! a =
        if compare k a = Ordering.eq ∧ k ∉ t then k else t.getKey! a
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair_iConvexComb_left : ∀ {R : Type u_1} {M : Type u_3} {J : Type u_7} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t)
  (h : s + t = 1) (g : Convexity.StdSimplex R J) (e : J → M) (m : M),
  Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb g e) m =
    Convexity.sConvexComb
      (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.map e g) (Convexity.StdSimplex.single m))
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Define a morphism between left extensions by cancelling the whiskered identities.  -/
CategoryTheory.Bicategory.LeftExtension.whiskerIdCancel : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          (s :
              CategoryTheory.Bicategory.LeftExtension f
                (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))) →
            {t : CategoryTheory.Bicategory.LeftExtension f g} →
              (s ⟶ t.whisker (CategoryTheory.CategoryStruct.id c)) → (s.ofCompId ⟶ t)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_div : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), √(x / y) = √x / √y
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.image_source_inter_eq' : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α), ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
-- Mathlib.NumberTheory.Dioph
Poly.one_apply : ∀ {α : Type u_1} (x : α → ℕ), 1 x = 1
-- Mathlib.Order.RelClasses
Order.Preimage.antisymm : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Antisymm r] {f : β → α},
  Function.Injective f → Std.Antisymm (f ⁻¹'o r)
-- Mathlib.Data.Set.Lattice
Set.sUnion_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → Set γ) (s : Set α) (t : Set β),
  ⋃₀ Set.image2 f s t = ⋃ a ∈ s, ⋃ b ∈ t, f a b
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Complex.isTheta_exp_arg_mul_im : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℂ},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |(g x).im|) →
    (fun x => Real.exp ((f x).arg * (g x).im)) =Θ[l] fun x => 1
-- Mathlib.Computability.Encoding
Computability.decodePosNum.eq_def : ∀ (x : List Bool),
  Computability.decodePosNum x =
    match x with
    | false :: l => (Computability.decodePosNum l).bit0
    | true :: l => if l = [] then PosNum.one else (Computability.decodePosNum l).bit1
    | x => PosNum.one
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_swap_swap : ∀ {α : Type u_1} [inst : DecidableEq α] {x y z t : α}, [x, y, z, t].Nodup → (Equiv.swap x y).Disjoint (Equiv.swap z t)
-- Mathlib.Geometry.Manifold.Algebra.SMul
instContMDiffVAddOfNatWithTopENatOfContinuousVAdd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : VAdd G M] [ContinuousVAdd G M],
  ContMDiffVAdd I I' 0 G M
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.instDistribMulAction : {M : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : AddZeroClass A] →
        [inst_1 : AddCommMonoid B] → [inst_2 : Monoid M] → [DistribMulAction M B] → DistribMulAction M (A →+ B)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : β k → β k}
  {he : (Std.DTreeMap.Internal.Impl.modify k f t).isEmpty = false},
  (Std.DTreeMap.Internal.Impl.modify k f t).minKey he = t.minKey ⋯
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.mk.inj : ∀ {G : Type u_1} {inst : Group G} {toSubgroup : Subgroup G}
  {isNormal' : autoParam toSubgroup.Normal FiniteIndexNormalSubgroup.isNormal'._autoParam}
  {isFiniteIndex' : autoParam toSubgroup.FiniteIndex FiniteIndexNormalSubgroup.isFiniteIndex'._autoParam}
  {toSubgroup_1 : Subgroup G}
  {isNormal'_1 : autoParam toSubgroup_1.Normal FiniteIndexNormalSubgroup.isNormal'._autoParam}
  {isFiniteIndex'_1 : autoParam toSubgroup_1.FiniteIndex FiniteIndexNormalSubgroup.isFiniteIndex'._autoParam},
  { toSubgroup := toSubgroup, isNormal' := isNormal', isFiniteIndex' := isFiniteIndex' } =
      { toSubgroup := toSubgroup_1, isNormal' := isNormal'_1, isFiniteIndex' := isFiniteIndex'_1 } →
    toSubgroup = toSubgroup_1
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_sdiff_add_ncard`. -/
Set.ncard_diff_add_ncard : ∀ {α : Type u_1} (s t : Set α),
  autoParam s.Finite Set.ncard_sdiff_add_ncard._auto_1 →
    autoParam t.Finite Set.ncard_sdiff_add_ncard._auto_3 → (s \ t).ncard + t.ncard = (s ∪ t).ncard
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.add_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G},
  IsBoundedBilinearMap 𝕜 f → ∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
CommGrpCat.FilteredColimits.colimitCoconeIsColimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommGrpCat),
  CommGrpCat.FilteredColimits.colimitCoconeIsColimit F =
    CategoryTheory.Limits.isColimitOfReflects (CategoryTheory.forget₂ CommGrpCat GrpCat)
      (GrpCat.FilteredColimits.colimitCoconeIsColimit (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat)))
-- Mathlib.Data.ENNReal.Operations
ENNReal.not_lt_zero : ∀ {a : ENNReal}, ¬a < 0
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_add_of_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A B : Set α},
  MeasurableSet A → MeasurableSet B → A ⊆ B → v A + v (B \ A) = v B
-- Init.Tactics
/-- `subst x...` substitutes each hypothesis `x` with a definition found in the local context,
then eliminates the hypothesis.
- If `x` is a local definition, then its definition is used.
- Otherwise, if there is a hypothesis of the form `x = e` or `e = x`,
  then `e` is used for the definition of `x`.

If `h : a = b`, then `subst h` may be used if either `a` or `b` unfolds to a local hypothesis.
This is similar to the `cases h` tactic.

See also: `subst_vars` for substituting all local hypotheses that have a defining equation.
 -/
Lean.Parser.Tactic.subst : Lean.ParserDescr
-- Std.Data.DTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `fallback`.
The key in the returned pair will compare equal to the input `a`.
 -/
Std.DTreeMap.getEntryD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → (a : α) × β a → (a : α) × β a
-- Init.Data.SInt.Lemmas
Int16.toInt_minValue_lt_zero : Int16.minValue.toInt < 0