mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
Fin.consEquivL_symm_apply : ∀ {n : ℕ} (R : Type u_4) (M : Fin n.succ → Type u_5) [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : (i : Fin n.succ) → Module R (M i)]
  [inst_3 : (i : Fin n.succ) → TopologicalSpace (M i)] (a : (i : Fin (n + 1)) → M i),
  (Fin.consEquivL R M).symm a = (a 0, Fin.tail a)
-- Mathlib.RingTheory.KrullDimension.Basic
/-- If `f : R →+* S` is surjective, then `ringKrullDim S ≤ ringKrullDim R`.  -/
ringKrullDim_le_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  Function.Surjective ⇑f → ringKrullDim S ≤ ringKrullDim R
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.instFintypeElemIdealPrimesOver : {A : Type u_4} →
  [inst : CommRing A] →
    (p : Ideal A) →
      [hpm : p.IsMaximal] →
        (B : Type u_5) →
          [inst_1 : CommRing B] →
            [IsDedekindDomain B] →
              [inst_3 : Algebra A B] →
                [IsDomain A] → [Module.IsTorsionFree A B] → [Algebra.IsIntegral A B] → Fintype ↑(p.primesOver B)
-- Mathlib.Topology.Compactification.StoneCech
ultrafilter_extend_extends : ∀ {α : Type u} {γ : Type u_1} [inst : TopologicalSpace γ] [T2Space γ] (f : α → γ), Ultrafilter.extend f ∘ pure = f
-- Lean.Parser.Types
Lean.Parser.Error.toString : Lean.Parser.Error → String
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqNotification.beq : {α : Type u_1} → [BEq α] → Lean.JsonRpc.Notification α → Lean.JsonRpc.Notification α → Bool
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_of_isEmpty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {a : α} {fallback : β}, (↑m).isEmpty = true → Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.nonsingular_neg : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular (W.neg P)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₀) (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) = X.δ f₁ f₂ n₀ n₁ hn₁
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Closure of a non-unital subsemiring `S` equals `S`.  -/
NonUnitalSubsemiring.closure_eq : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R), NonUnitalSubsemiring.closure ↑s = s
-- Std.Internal.Do.Order.Basic
Lean.Order.of_top_le_prop : ∀ {x : Prop}, Lean.Order.PartialOrder.rel Lean.Order.top x → x
-- Mathlib.Topology.Maps.Strict.Basic
/-- A open continuous map is a strict map.  -/
IsOpenMap.isStrictMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → Continuous f → Topology.IsStrictMap f
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- Transfer creation of finite colimits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.createsFiniteColimitsOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          {h : F ≅ G} → [CategoryTheory.Limits.CreatesFiniteColimits F] → CategoryTheory.Limits.CreatesFiniteColimits G
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y)
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x : X),
  ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom.app
            X_1).fst.app
      x =
    CategoryTheory.CategoryStruct.id (ψ.left.obj (X_1.fst.obj (U.obj x)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey?_alter!_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).maxKey? = some k ↔
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true
-- Qq.Macro
Qq.Impl.MVarSynth.type.inj : ∀ {unquotedMVar unquotedMVar_1 : Lean.MVarId},
  Qq.Impl.MVarSynth.type unquotedMVar = Qq.Impl.MVarSynth.type unquotedMVar_1 → unquotedMVar = unquotedMVar_1
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_rename : ∀ {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (g : τ → α)
  (p : MvPolynomial σ R), (MvPolynomial.rename g) ((MvPolynomial.rename f) p) = (MvPolynomial.rename (g ∘ f)) p
-- Init.Data.BitVec.Lemmas
BitVec.neg_one_eq_zero_iff : ∀ {w : ℕ}, -1#w = 0#w ↔ w = 0
-- Mathlib.Algebra.Order.Ring.StandardPart
_private.Mathlib.Algebra.Order.Ring.StandardPart.0.ArchimedeanClass.stdPart.eq_1 : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x : K),
  ArchimedeanClass.stdPart x =
    if h : 0 ≤ ArchimedeanClass.mk x then
      (Classical.ofNonempty.comp ArchimedeanClass.FiniteResidueField.mk) (ArchimedeanClass.FiniteElement.mk x h)
    else 0
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.beq_iff_equiv : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [LawfulBEq α],
  m₁.WF → m₂.WF → ((m₁ == m₂) = true ↔ m₁.Equiv m₂)
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
/-- The property that a category `C` and a regular cardinal `κ`
satisfy `P.IsCardinalFilteredGenerators κ` for a suitable essentially
small `P : ObjectProperty C`.  -/
CategoryTheory.HasCardinalFilteredGenerator : (C : Type u) → [hC : CategoryTheory.Category.{v, u} C] → (κ : Cardinal.{w}) → [hκ : Fact κ.IsRegular] → Prop
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_not : ∀ {a : USize} (h : System.Platform.numBits = 32), (~~~a).toBitVec32 h = ~~~a.toBitVec32 h
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.isOpenQuotientMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : Group G] [inst_3 : MulAction G E], IsQuotientCoveringMap f G → IsOpenQuotientMap f
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_mul_vecMulVec : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m]
  (u : l → α) (v w : m → α) (x : n → α), Matrix.vecMulVec u v * Matrix.vecMulVec w x = Matrix.vecMulVec u ((v ⬝ᵥ w) • x)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousWithinAt.continuousLinearMapCoprod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5}
  [inst_7 : TopologicalSpace X] {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun x => (f x).coprod (g x)) s x
-- Batteries.Data.Fin.Coding
Fin.encodeSubtype.eq_1 : ∀ (n_2 : ℕ) (P_2 : Fin (n_2 + 1) → Prop) (inst_2 : DecidablePred P_2) (hp : P_2 0),
  Fin.encodeSubtype P_2 ⟨⟨0, ⋯⟩, hp⟩ = ⟨0, ⋯⟩
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_zsmul : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) {n : ℤ} {x : 𝕜}, ↑(n • x) = n • ↑x
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_monomial : ∀ {R : Type u} {σ : Type u_1} {r : R} {s : σ →₀ ℕ} [inst : CommSemiring R],
  r ≠ 0 → ((MvPolynomial.monomial s) r).vars = s.support
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: the image of a `Set.OrdConnected` set under `f'` is a `Set.OrdConnected`
set, `deriv` version.  -/
Set.OrdConnected.image_deriv : ∀ {f : ℝ → ℝ} {s : Set ℝ}, s.OrdConnected → (∀ x ∈ s, DifferentiableAt ℝ f x) → (deriv f '' s).OrdConnected
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- The **Weinstein–Aronszajn identity**. Note the `1` on the LHS is of shape m×m, while the `1` on
the RHS is of shape n×n.  -/
Matrix.det_one_add_mul_comm : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m n α) (B : Matrix n m α),
  (1 + A * B).det = (1 + B * A).det
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.single_mul_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MulZeroClass (α i)] [inst_1 : DecidableEq ι] {i : ι}
  {f : (i : ι) → α i} (a : α i), Pi.single i (a * f i) = Pi.single i a * f
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_appTop : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V),
  AlgebraicGeometry.Scheme.Hom.appTop (X.homOfLE e) = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Lean.Parser.Do
Lean.Parser.Term.doWhile.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instSMul : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] →
          {R : Type u_2} →
            [inst_3 : Zero R] →
              [inst_4 : SMulWithZero R β] → [ContinuousConstSMul R β] → SMul R (ZeroAtInftyContinuousMap α β)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.fst =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Data.Int.Fib.Basic
_private.Mathlib.Data.Int.Fib.Basic.0.Int.fib_natCast_add : ∀ (m : ℕ) (n : ℤ), Int.fib (↑m + n) = Int.fib (↑m - 1) * Int.fib n + Int.fib ↑m * Int.fib (n + 1)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The identity refinement of a pre-`1`-hypercover.  -/
CategoryTheory.PreOneHypercover.Hom.id : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S : C} → (E : CategoryTheory.PreOneHypercover S) → E.Hom E
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.WF → m₂.WF → (m₁ \ m₂).WF
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.State.letRecsToLift : Lean.Elab.Term.State → List Lean.Elab.Term.LetRecToLift
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
/-- Explicit lower bound on the **Ruzsa-Szemerédi problem**.

There exists a graph with `n` vertices and
`(n / 3 - 2) * (n - 3) / 6 * exp (-4 * √(log ((n - 3) / 6)))` edges such that each edge belongs
to exactly one triangle.  -/
ruzsaSzemerediNumberNat_lower_bound : ∀ (n : ℕ), (↑n / 3 - 2) * ↑((n - 3) / 6) * Real.exp (-4 * √(Real.log ↑((n - 3) / 6))) ≤ ↑(ruzsaSzemerediNumberNat n)
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstLEInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.GroupTheory.Index
AddSubgroup.index_bot : ∀ {G : Type u_1} [inst : AddGroup G], ⊥.index = Nat.card G
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.add.sizeOf_spec : ∀ (a a_1 : Mathlib.Tactic.Linarith.CompSource), sizeOf (a.add a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.sInfGen_def : ∀ {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) (t : Set α),
  MeasureTheory.OuterMeasure.sInfGen m t = ⨅ μ ∈ m, μ t
-- Mathlib.RingTheory.Derivation.Basic
Derivation.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  (toLinearMap : A →ₗ[R] M) (map_one_eq_zero' : toLinearMap 1 = 0)
  (leibniz' : ∀ (a b : A), toLinearMap (a * b) = a • toLinearMap b + b • toLinearMap a) (toLinearMap_1 : A →ₗ[R] M)
  (map_one_eq_zero'_1 : toLinearMap_1 1 = 0)
  (leibniz'_1 : ∀ (a b : A), toLinearMap_1 (a * b) = a • toLinearMap_1 b + b • toLinearMap_1 a),
  ({ toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' } =
      { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.continuousOn_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜] [Finite ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜 F]
  {G : Type u_5} [inst_8 : AddCommGroup G] [inst_9 : TopologicalSpace G] [inst_10 : Module 𝕜 G]
  [inst_11 : ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {s : Set (G × ((i : ι) → E i))},
  ContinuousOn (fun p => (f p.1) p.2) s
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Constant functions are harmonic
 -/
InnerProductSpace.harmonicAt_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {x : E} (c : F),
  InnerProductSpace.HarmonicAt (fun x => c) x
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- When a function has a limit at infinity, and its derivative is nonnegative, then the derivative
is automatically integrable on `(a, +∞)`. Version assuming differentiability
on `[a, +∞)`.  -/
MeasureTheory.integrableOn_Ioi_deriv_of_nonneg' : ∀ {g g' : ℝ → ℝ} {a l : ℝ},
  (∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x) →
    (∀ x ∈ Set.Ioi a, 0 ≤ g' x) →
      Filter.Tendsto g Filter.atTop (nhds l) → MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
-- Mathlib.Algebra.Homology.Localization
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor : ∀ {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] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι)
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.CategoryWithHomology C] [inst_5 : CategoryTheory.CategoryWithHomology D]
  [inst_6 : F.Additive] [inst_7 : F.PreservesHomology],
  (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).functor = F.mapHomologicalComplex c
-- Mathlib.Data.Int.Notation
/-- The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
 -/
termℤ : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.first?_eq_match_step : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Productive α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β},
  it.first? =
    match ↑it.step with
    | Std.IterStep.yield it out => some out
    | Std.IterStep.skip it' => it'.first?
    | Std.IterStep.done => none
-- Mathlib.Tactic.CategoryTheory.Bicategory.Basic
/-- Use the coherence theorem for bicategories to solve equations in a bicategory,
where the two sides only differ by replacing strings of bicategory structural morphisms
(that is, associators, unitors, and identities)
with different strings of structural morphisms with the same source and target.

That is, `bicategory` can handle goals of the form
`a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'`
where `a = a'`, `b = b'`, and `c = c'` can be proved using `bicategory_coherence`.
 -/
Mathlib.Tactic.Bicategory.bicategory : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.IsSplitEqualizer.map_leftRetraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X} (q : CategoryTheory.IsSplitEqualizer f g ι)
  (F : CategoryTheory.Functor C D), (q.map F).leftRetraction = F.map q.leftRetraction
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_mem_smul_set_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set β} {a : α} {x : β},
  a • x ∈ a • s ↔ x ∈ s
-- Mathlib.Data.List.Defs
List.headI_cons : ∀ {α : Type u_1} [inst : Inhabited α] {h : α} {t : List α}, (h :: t).headI = h
-- Mathlib.Algebra.Order.Quantale
/-- Addition is distributive over join in a quantale  -/
IsAddQuantale.add_sSup_distrib : ∀ {α : Type u_1} {inst : AddSemigroup α} {inst_1 : CompleteLattice α} [self : IsAddQuantale α] (x : α) (s : Set α),
  x + sSup s = ⨆ y ∈ s, x + y
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.ext : ∀ {V : Type u_1} {G : SimpleGraph V} (d₁ d₂ : G.Dart), d₁.toProd = d₂.toProd → d₁ = d₂
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a},
  (↑m).WF → (↑(Std.DHashMap.Internal.Raw₀.map f m)).size = (↑m).size
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Monotone.expGrowthInf_comp_le : ∀ {u : ℕ → ENNReal} {v : ℕ → ℕ},
  Monotone u →
    (LinearGrowth.linearGrowthSup fun n => ↑(v n)) ≠ 0 →
      (LinearGrowth.linearGrowthSup fun n => ↑(v n)) ≠ ⊤ →
        ExpGrowth.expGrowthInf (u ∘ v) ≤ (LinearGrowth.linearGrowthSup fun n => ↑(v n)) * ExpGrowth.expGrowthInf u
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
/-- (Implementation) The definition of `functorToInterchange`.  -/
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type u)) →
      {J : Type} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          (K : CategoryTheory.Functor J Cᵒᵖ) →
            CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K ≅
              K.comp
                (CategoryTheory.coyoneda.comp
                  ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) C
                        (Type u)).obj
                    (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A)))
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Right homotopy is closed under composition (on the left).  -/
CategoryTheory.Arrow.RightHomotopy.compLeft : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v w : CategoryTheory.Arrow V} →
        {f g : v ⟶ w} →
          CategoryTheory.Arrow.RightHomotopy f g →
            (e : u ⟶ v) →
              CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp e f)
                (CategoryTheory.CategoryStruct.comp e g)
-- Init.Ext
PUnit.ext_iff : ∀ {a b : PUnit.{u_1}}, a = b ↔ True
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instMul : {D : Type u_1} → {Q : Type u_2} → [Group D] → [Group Q] → Mul (D ≀ᵣ Q)
-- Mathlib.Analysis.InnerProductSpace.Calculus
hasStrictFDerivAt_norm_sq : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F),
  HasStrictFDerivAt (fun x => ‖x‖ ^ 2) (2 • (innerSL ℝ) x) x
-- Mathlib.NumberTheory.MahlerMeasure
/-- If an integer polynomial has Mahler measure equal to 1, then all its complex roots have norm at
most 1.  -/
Polynomial.norm_root_le_one_of_mahlerMeasure_eq_one : ∀ {p : Polynomial ℤ}, (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 → ∀ {z : ℂ}, z ∈ p.aroots ℂ → ‖z‖ ≤ 1
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *non-unital ⋆-algebra homomorphism* is a non-unital algebra homomorphism between
non-unital `R`-algebras `A` and `B` equipped with a `star` operation, and this homomorphism is
also `star`-preserving.  -/
«term_→⋆ₙₐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (P Q : CategoryTheory.ProjectiveResolution X) {Z : HomologicalComplex C (ComplexShape.down ℕ)}
  (h : (ChainComplex.single₀ C).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).hom (CategoryTheory.CategoryStruct.comp Q.π h) =
    CategoryTheory.CategoryStruct.comp P.π h
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of the results of subtracting a base point from the
given points, as a linear map on the weights.  The main cases of
interest are where the sum of the weights is 0, in which case the sum
is independent of the choice of base point, and where the sum of the
weights is 1, in which case the sum added to the base point is
independent of the choice of base point.  -/
Finset.weightedVSubOfPoint : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [S : AddTorsor V P] → {ι : Type u_4} → Finset ι → (ι → P) → P → (ι → k) →ₗ[k] V
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.ι_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.ι f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)) h