mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.leftModule : {R : Type u_1} → [inst : Ring R] → (I : TwoSidedIdeal R) → Module R ↥I
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.Y_sub_Y_mul_Y_sub_negY : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 0 * Q 2 = Q 0 * P 2 → P 2 * Q 2 * (P 1 * Q 2 - Q 1 * P 2) * (P 1 * Q 2 - W'.negY Q * P 2) = 0
-- Mathlib.Algebra.GroupWithZero.Defs
/-- The inverse of `0` in a group with zero is `0`.  -/
CommGroupWithZero.inv_zero : ∀ {G₀ : Type u_2} [self : CommGroupWithZero G₀], 0⁻¹ = 0
-- Mathlib.Data.Num.Bitwise
PosNum.instOrOp : OrOp PosNum
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).natTrailingDegree = p.natTrailingDegree
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr_refl : ∀ {α : Sort u_1} {β : Sort u_2}, (Equiv.refl α).arrowCongr (Equiv.refl β) = Equiv.refl (α → β)
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- `AlgebraicIndependent R x` states the family of elements `x`
is algebraically independent over `R`, meaning that the canonical
map out of the multivariable polynomial ring is injective.  -/
AlgebraicIndependent : {ι : Type u_1} →
  (R : Type u_3) → {A : Type u_5} → (ι → A) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop
-- Std.Async.TCP
/-- Enables the Nagle algorithm for the client socket.
 -/
Std.Async.TCP.Socket.Client.noDelay : Std.Async.TCP.Socket.Client → IO Unit
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableOn_atlas : ∀ {𝕜 : 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 : OpenPartialHomeomorph M H} [IsManifold I 1 M],
  e ∈ atlas H M → MDiff[e.source] ↑e
-- Mathlib.RingTheory.Invariant.Basic
/-- If `Q` lies over `P`, then the stabilizer of `Q` acts on `Frac(B/Q)/Frac(A/P)`.  -/
IsFractionRing.stabilizerHom : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (G : Type u_3) →
            [inst_3 : Group G] →
              [inst_4 : MulSemiringAction G B] →
                [SMulCommClass G A B] →
                  (P : Ideal A) →
                    (Q : Ideal B) →
                      [inst_6 : Q.LiesOver P] →
                        (K : Type u_4) →
                          (L : Type u_5) →
                            [inst_7 : Field K] →
                              [inst_8 : Field L] →
                                [inst_9 : Algebra (A ⧸ P) K] →
                                  [inst_10 : Algebra (B ⧸ Q) L] →
                                    [inst_11 : Algebra (A ⧸ P) L] →
                                      [IsScalarTower (A ⧸ P) (B ⧸ Q) L] →
                                        [inst_13 : Algebra K L] →
                                          [IsScalarTower (A ⧸ P) K L] →
                                            [IsFractionRing (A ⧸ P) K] →
                                              [IsFractionRing (B ⧸ Q) L] → ↥(MulAction.stabilizer G Q) →* Gal(L/K)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsTwoSided.instHPowNat : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} [I.IsTwoSided] (n : ℕ), (I ^ n).IsTwoSided
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.up_size_toArray_eq_count : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  (fun x => { down := x.size }) <$> it.toArray = it.length
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.Context.table : Lean.PrettyPrinter.Formatter.Context → Lean.Parser.TokenTable
-- Mathlib.Computability.Reduce
OneOneReducible.of_equiv_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {e : α ≃ β} (q : β → Prop),
  Computable ⇑e.symm → q ≤₁ (q ∘ ⇑e)
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toIntertwiningMap_mk' : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (e : V ≃ₗ[A] W) (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e),
  ↑(Representation.Equiv.mk e he) = { toLinearMap := ↑e, isIntertwining' := he }
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.rankFinite_of_finite : ∀ {α : Type u_1} (M : Matroid α) [M.Finite], M.RankFinite
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.map_unop_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : Mᵐᵒᵖ),
  Filter.map MulOpposite.unop (nhds x) = nhds (MulOpposite.unop x)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.rootSet_prod : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra R S]
  {ι : Type u_1} (f : ι → Polynomial R) (s : Finset ι), s.prod f ≠ 0 → (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S
-- Mathlib.RingTheory.DedekindDomain.Different
coeSubmodule_differentIdeal : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} (B : Type u_3) [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L]
  [IsIntegrallyClosed A] [inst_17 : IsDedekindDomain B] [inst_18 : Module.IsTorsionFree A B] [IsFractionRing B L],
  IsLocalization.coeSubmodule L (differentIdeal A B) = 1 / Submodule.traceDual A K 1
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.ofMapBounded_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] (f : α → β)
  {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)} (a : α),
  (LocallyBoundedMap.ofMapBounded f h) a = f a
-- Mathlib.RingTheory.PowerSeries.PiTopology
PowerSeries.WithPiTopology.hasSum_iff_hasSum_coeff : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_2} {f : ι → PowerSeries R}
  {g : PowerSeries R}, HasSum f g ↔ ∀ (d : ℕ), HasSum (fun i => (PowerSeries.coeff d) (f i)) ((PowerSeries.coeff d) g)
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.Array.MergeSort.Internal.merge.eq_1 : ∀ {α : Type u_1} (xs ys : Array α) (le : α → α → Bool),
  Array.MergeSort.Internal.merge✝ xs ys le =
    if hxs : 0 < xs.size then
      if hys : 0 < ys.size then
        Array.MergeSort.Internal.merge.go✝ le (Std.Rii.Sliceable.mkSlice xs *...*) (Std.Rii.Sliceable.mkSlice ys *...*)
          ⋯ ⋯ (Array.emptyWithCapacity (xs.size + ys.size))
      else xs
    else ys
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.countPerms.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (m m_1 : Multiset α),
  m = m_1 → m.countPerms = m_1.countPerms
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.subsemigroupComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (N' : AddSubsemigroup N),
  f.subsemigroupComap N' = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_add' := ⋯ }
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onSentence_symm_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (φ : L ≃ᴸ L') (a : L'.BoundedFormula Empty 0),
  φ.onSentence.symm a = φ.invLHom.onBoundedFormula a
-- Mathlib.LinearAlgebra.Dual.Basis
/-- Try using `Set.toFinite` to dispatch a `Set.Finite` goal.  -/
evalUseFiniteInstance : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Symmetrized
/-- The element of `α` represented by `x : αˢʸᵐ`.  -/
SymAlg.unsym : {α : Type u_1} → αˢʸᵐ ≃ α
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.nonempty_cauchyFilter_iff : ∀ {α : Type u} [inst : UniformSpace α], Nonempty (CauchyFilter α) ↔ Nonempty α
-- Lean.Data.Lsp.Utf16
/-- Returns the number of bytes required to encode this `Char` in UTF-16.  -/
Lean.Char.utf16Size : Char → UInt32
-- Mathlib.Algebra.GroupWithZero.Action.Units
Commute.smul_right_iff₀ : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α} [inst_2 : Mul β]
  [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}, a ≠ 0 → (Commute x (a • y) ↔ Commute x y)
-- Mathlib.Topology.Inseparable
GeneralizingMap.stableUnderGeneralization_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  GeneralizingMap f → ∀ {s : Set X}, StableUnderGeneralization s → StableUnderGeneralization (f '' s)
-- Mathlib.CategoryTheory.Square
/-- The map `Square Cᵒᵖ → Square C` which switches `X₁` and `X₃`, but
does not move `X₂` and `X₃`.  -/
CategoryTheory.Square.unop : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square Cᵒᵖ → CategoryTheory.Square C
-- Aesop.RuleTac.Cases
Aesop.CasesTarget'.decl.injEq : ∀ (decl decl_1 : Lean.Name), (Aesop.CasesTarget'.decl decl = Aesop.CasesTarget'.decl decl_1) = (decl = decl_1)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsSymmetricProjection.le_iff_range_le_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {p q : E →ₗ[𝕜] E}, p.IsSymmetricProjection → q.IsSymmetricProjection → (p ≤ q ↔ p.range ≤ q.range)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.Spec.structureSheaf.eq_1 : ∀ (R : Type u) [inst : CommRing R],
  AlgebraicGeometry.Spec.structureSheaf R = { obj := AlgebraicGeometry.structurePresheafInCommRingCat R, property := ⋯ }
-- Mathlib.Analysis.Analytic.Constructions
/-- `(f x)⁻¹` is analytic away from `f x = 0`  -/
AnalyticOnNhd.inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → (∀ x ∈ s, f x ≠ 0) → AnalyticOnNhd 𝕜 f⁻¹ s
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derivedη_fac_app_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [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.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₁ : CategoryTheory.MorphismProperty C₁) [inst_4 : L₁.IsLocalization W₁] {G' : CategoryTheory.Functor D₁ D₂}
  {F' : CategoryTheory.Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F')
  [inst_5 :
    (G'.comp F').IsLeftDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (L₁.associator G' F').inv (CategoryTheory.Functor.whiskerRight α F')) W₁]
  (X₁ : C₁) {Z : D₁} (h : F'.obj (L₂.obj (G.obj X₁)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((adj.derivedη W₁ α β).app (L₁.obj X₁))
      (CategoryTheory.CategoryStruct.comp (F'.map (α.app X₁)) h) =
    CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁))
      (CategoryTheory.CategoryStruct.comp (β.app (G.obj X₁)) h)
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Ring.HasFiniteQuotients.instPerfectFieldResidueFieldOfFractionRing : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] [inst_2 : IsDomain R] [PerfectField (FractionRing R)]
  (P : Ideal R) [inst_4 : P.IsPrime], PerfectField P.ResidueField
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_singleton : ∀ {α : Type u} {a : α}, {a}.Subsingleton
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.distinct_keys_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) t.toList
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.mk.injEq : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (obj : C → D) (map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y)
  (map_id :
    autoParam
      (∀ (X : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) = CategoryTheory.eId V (obj X))
      CategoryTheory.EnrichedFunctor.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ (X Y Z : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z))
            (CategoryTheory.eComp V (obj X) (obj Y) (obj Z)))
      CategoryTheory.EnrichedFunctor.map_comp._autoParam)
  (obj_1 : C → D) (map_1 : (X Y : C) → (X ⟶[V] Y) ⟶ obj_1 X ⟶[V] obj_1 Y)
  (map_id_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map_1 X X) = CategoryTheory.eId V (obj_1 X))
      CategoryTheory.EnrichedFunctor.map_id._autoParam)
  (map_comp_1 :
    autoParam
      (∀ (X Y Z : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map_1 X Z) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map_1 X Y) (map_1 Y Z))
            (CategoryTheory.eComp V (obj_1 X) (obj_1 Y) (obj_1 Z)))
      CategoryTheory.EnrichedFunctor.map_comp._autoParam),
  ({ obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
      { obj := obj_1, map := map_1, map_id := map_id_1, map_comp := map_comp_1 }) =
    (obj = obj_1 ∧ map ≍ map_1)
-- Mathlib.Algebra.Order.IsBotOne
/-- Create an `OrderBot` instance, setting `1` as the bottom element.  -/
IsBotOneClass.toOrderBot : (α : Type u_1) → [inst : LE α] → [inst_1 : One α] → [IsBotOneClass α] → OrderBot α
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.petersson_symm : ∀ (k : ℤ) (f f' : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),
  UpperHalfPlane.petersson k f' f τ = (starRingEnd ℂ) (UpperHalfPlane.petersson k f f' τ)
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.instCoeSortType : CoeSort CompactlyGenerated (Type u_1)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_lt : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [inst : Preorder ι] {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.Kernel.iIndepSet s κ μ →
      ∀ (i : ι),
        ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {s i})
          (MeasurableSpace.generateFrom {t | ∃ j < i, s j = t}) κ μ
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalNestedConv : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.map_smul : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B) (c : R) (x : A), f (c • x) = φ c • f x
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_of_L1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x : WithLp 1 (α × β)), ‖x‖ = ‖x.fst‖ + ‖x.snd‖
-- Init.Data.Array.Zip
Array.lt_size_left_of_zip : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {as : Array α} {bs : Array β}, i < (as.zip bs).size → i < as.size
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
/-- A functor defines a morphism of vertex groups.  -/
CategoryTheory.Functor.mapVertexGroup : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.Groupoid D] → (φ : CategoryTheory.Functor C D) → (c : C) → (c ⟶ c) →* (φ.obj c ⟶ φ.obj c)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.constantsToVars.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (f : (L.withConstants γ).Functions 0)
  (ts : Fin 0 → (L.withConstants γ).Term α),
  (FirstOrder.Language.func f ts).constantsToVars =
    Sum.casesOn f (fun f => FirstOrder.Language.func f fun i => (ts i).constantsToVars) fun c =>
      FirstOrder.Language.var (Sum.inl c)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {ι : Type u_2} {c : ComplexShape ι} {x y : TopPair.HomologyPretheory C c},
  x.Hₚ = y.Hₚ → x.H = y.H → x.iso ≍ y.iso → x.δ ≍ y.δ → x = y
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.mk.injEq : ∀ {V : Type u₁} [inst : CategoryTheory.ReflQuiver V] {W : Type u₂} [inst_1 : CategoryTheory.ReflQuiver W]
  (toPrefunctor : V ⥤q W)
  (map_id :
    autoParam
      (∀ (X : V), toPrefunctor.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (toPrefunctor.obj X))
      CategoryTheory.ReflPrefunctor.map_id._autoParam)
  (toPrefunctor_1 : V ⥤q W)
  (map_id_1 :
    autoParam
      (∀ (X : V),
        toPrefunctor_1.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (toPrefunctor_1.obj X))
      CategoryTheory.ReflPrefunctor.map_id._autoParam),
  ({ toPrefunctor := toPrefunctor, map_id := map_id } = { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }) =
    (toPrefunctor = toPrefunctor_1)
-- Init.Data.String.Decode
List.utf8DecodeChar?_utf8Encode_cons : ∀ {l : List Char} {c : Char}, (c :: l).utf8Encode.utf8DecodeChar? 0 = some c
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_Icc : ∀ {n : ℕ} (i j : Fin n), Fin.succ '' Set.Icc i j = Set.Icc i.succ j.succ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context.toIntId : Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context → ℕ
-- Mathlib.Algebra.Algebra.Spectrum.Basic
Units.zero_notMem_spectrum : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : Aˣ), 0 ∉ spectrum R ↑a
-- Mathlib.Topology.Instances.CantorSet
/-- The Cantor set is the subset of the unit interval obtained as the intersection of all
pre-Cantor sets. This means that the Cantor set is obtained by iteratively removing the
open middle third of each subinterval, starting from the unit interval `[0, 1]`.
 -/
cantorSet : Set ℝ
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instLieGroupOfSomeENatTopOfLEInfty : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {a : WithTop ℕ∞} [LieGroup I (↑⊤) G]
  [h : ENat.LEInfty a], LieGroup I a G
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.importEnv?.unsafe_1 : Lean.Environment → Option Lean.Environment
-- Init.Data.List.Lemmas
List.append_eq_cons_iff : ∀ {α : Type u_1} {as bs : List α} {x : α} {c : List α},
  as ++ bs = x :: c ↔ as = [] ∧ bs = x :: c ∨ ∃ as', as = x :: as' ∧ c = as' ++ bs
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
angle-at-point form where the apex is given as the center of a circle.  -/
EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left : ∀ {V : Type u_3} {P : Type u_4} [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)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s →
    p₂ ∈ s → p₁ ≠ p₂ → EuclideanGeometry.oangle p₁ s.center p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle s.center p₂ p₁
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_add_natCast : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 ≤ a → ∀ (n : ℕ), ⌈a + ↑n⌉₊ = ⌈a⌉₊ + n
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom =
    CategoryTheory.FunctorToTypes.coprod.inl
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.IsIPC.isIPCOfShape : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasProducts C}
  {inst_2 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, u_3, v_1, u_1} C} [self : CategoryTheory.Limits.IsIPC C]
  (ι : Type w), CategoryTheory.Limits.IsIPCOfShape.{w, w, v_1, u_1} ι C
-- Mathlib.Algebra.Group.Action.Pi
Pi.smul_apply' : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} (i : ι) [inst : (i : ι) → SMul (α i) (β i)] (s : (i : ι) → α i)
  (x : (i : ι) → β i), (s • x) i = s i • x i
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.id_indexEquiv_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (a : ι),
  (RootPairing.Hom.id P).indexEquiv.symm a = a
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.divConst.congr_simp : ∀ {G : Type u_1} [inst : Group G] {inst_1 : DecidableEq G} [inst_2 : DecidableEq G] (A A_1 : Finset G),
  A = A_1 → ∀ (B B_1 : Finset G), B = B_1 → A.divConst B = A_1.divConst B_1
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated : ∀ {β : Type u_2} {α : Type u_3} [inst : MeasurableSpace β] [h : MeasurableSpace.CountablyGenerated β],
  MeasurableSpace.CountableOrCountablyGenerated α β
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isUniformInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → UniformContinuous f → IsUniformInducing f
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_Ici : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a : α),
  -Set.Ici a = Set.Iic (-a)
-- Mathlib.Data.Nat.Digits.Defs
/-- The digits in the base b+2 expansion of n are all less than b+2  -/
Nat.digits_lt_base' : ∀ {b m d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.NatTrans.whiskerLeft_app_tensor_app_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  {F G F' G' : CategoryTheory.Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X' Y' : J} (f : X' ⟶ Y') (X : J) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F'.obj X) (G'.obj Y') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (G.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app Y')) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F'.obj X) (G'.map f)) h)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (-f) s