mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
/-- A `LeftPreLieAlgebra` is a `LeftPreLieRing` with an action of a `CommRing` satisfying
`r • x * y = r • (x * y)` and ` x * (r • y) = r • (x * y)`.  -/
LeftPreLieAlgebra : (R : Type u_1) → [CommRing R] → (L : Type u_2) → [LeftPreLieRing L] → Type (max u_1 u_2)
-- Mathlib.Order.Interval.Set.SuccPred
Set.Iic_pred_eq_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (b : α),
  Set.Iic (Order.pred b) = Set.Iio b
-- Mathlib.Topology.Compactness.Compact
/-- Cantor's intersection theorem for sequences indexed by `ℕ`:
the intersection of a decreasing sequence of nonempty compact closed sets is nonempty.  -/
IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] (t : ℕ → Set X),
  (∀ (i : ℕ), t (i + 1) ⊆ t i) →
    (∀ (i : ℕ), (t i).Nonempty) → IsCompact (t 0) → (∀ (i : ℕ), IsClosed (t i)) → (⋂ i, t i).Nonempty
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_of_re_neg_of_im_neg : ∀ {x : ℂ}, x.re < 0 → x.im < 0 → x.arg = Real.arcsin ((-x).im / ‖x‖) - Real.pi
-- Mathlib.Data.Int.Cast.Lemmas
Int.coe_castRingHom : ∀ {α : Type u_3} [inst : NonAssocRing α], ⇑(Int.castRingHom α) = fun x => ↑x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- The q-expansion constant coefficient of the normalised Eisenstein series `E k` is `1`.  -/
EisensteinSeries.E_qExpansion_coeff_zero : ∀ {k : ℕ} (hk : 3 ≤ k), Even k → (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑(ModularForm.E hk)) = 1
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.disjoint_coe : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C₁ C₂ : ConvexCone R M}, Disjoint ↑C₁ ↑C₂ ↔ Disjoint C₁ C₂
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.mk.inj : ∀ {R : Type u_1} {inst : CommSemiring R} {asIdeal : Ideal R} {isPrime : asIdeal.IsPrime} {asIdeal_1 : Ideal R}
  {isPrime_1 : asIdeal_1.IsPrime},
  { asIdeal := asIdeal, isPrime := isPrime } = { asIdeal := asIdeal_1, isPrime := isPrime_1 } → asIdeal = asIdeal_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentHighlightParams.toJson : Lean.Lsp.DocumentHighlightParams → Lean.Json
-- Mathlib.Data.Rat.Defs
Rat.canLift : CanLift ℚ ℤ Int.cast fun q => q.den = 1
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- If `P` is local at the source, then it respects composition on the left with open immersions.  -/
AlgebraicGeometry.IsZariskiLocalAtSource.respectsLeft_isOpenImmersion : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P],
  P.RespectsLeft AlgebraicGeometry.IsOpenImmersion
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.isPretransitive_quotient : ∀ (G : Type u_1) [inst : Group G] (H : Subgroup G), MulAction.IsPretransitive G (G ⧸ H)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.AC.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.AC.EqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.AC.EqCnstrProof) →
      ((t : Lean.Meta.Grind.AC.EqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.AC.EqCnstrProof) → t.below → motive_2 t) → motive_2 t ×' t.below
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_cons : ∀ {α : Type u} (s : Stream'.WSeq α) (a : α), a ∈ Stream'.WSeq.cons a s
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.setOfPred_dep_eq`. -/
Matroid.setOf_dep_eq : ∀ {α : Type u_1} (M : Matroid α), {D | M.Dep D} = {I | M.Indep I}ᶜ ∩ Set.Iic M.E
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.associator_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H I : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B),
  (CategoryTheory.Lax.OplaxTrans.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ (k : α) (f : β → β), m₁.Equiv m₂ → (m₁.modify k f).Equiv (m₂.modify k f)
-- Mathlib.Data.Nat.Init
/-- Induction principle starting at a non-zero number.
To use in an induction proof, the syntax is `induction n, hn using Nat.le_induction` (or the same
for `induction'`).

This is an alias of `Nat.leRec`, specialized to `Prop`.  -/
Nat.le_induction : ∀ {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop},
  P m ⋯ → (∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) → ∀ (n : ℕ) (hmn : m ≤ n), P n hmn
-- Init.Data.UInt.Bitwise
UInt16.toUSize_shiftLeft_of_lt : ∀ (a b : UInt16), b < 16 → (a <<< b).toUSize = a.toUSize <<< b.toUSize % 65536
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalUnopUnop_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.unopUnop C) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.unopUnop C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit Cᵒᵖᵒᵖ))
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.eq_reflection_of_eq_subspace : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s s' : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : Nonempty ↥s'] [inst_7 : s.direction.HasOrthogonalProjection]
  [inst_8 : s'.direction.HasOrthogonalProjection],
  s = s' → ∀ (p : P), (EuclideanGeometry.reflection s) p = (EuclideanGeometry.reflection s') p
-- Init.Data.UInt.Lemmas
UInt8.toNat_inj : ∀ {a b : UInt8}, a.toNat = b.toNat ↔ a = b
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex'_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq fst snd f g), sq.shortComplex'.X₂ = (X₂ ⊞ X₃)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet.coe_smul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] [inst_3 : Algebra S R]
  {G : Type u_1} [inst_4 : Monoid G] [inst_5 : MulSemiringAction G R] [inst_6 : SMulCommClass G S R] {f : Polynomial S}
  (g : G) (x : ↑(f.rootSet R)), ↑(g • x) = g • ↑x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_subtype : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {p : ι → Prop} {F : Fintype (Subtype p)} (s : Finset ι),
  (∀ (x : ι), x ∈ s ↔ p x) → ∀ (f : ι → M), ∑ a ∈ s, f a = ∑ a, f ↑a
-- Lean.Meta.Diagnostics
Lean.Meta.mkDiagSummary : Lean.Name → Lean.PHashMap Lean.Name ℕ → (optParam (Lean.Name → Bool) fun x => true) → Lean.MetaM Lean.Meta.DiagSummary
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.endsWith_prop_eq_false_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice},
  s.endsWith P = false ↔ ∀ (h : s.endPos ≠ s.startPos), ¬P ((s.endPos.prev h).get ⋯)
-- Init.Data.Array.Find
Array.find?_eq_none : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.find? p xs = none ↔ ∀ x ∈ xs, ¬p x = true
-- Mathlib.Order.SuccPred.Basic
Order.Iic_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α), Set.Iic (Order.pred a) = Set.Iio a
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between a `π / 2` rotation of a vector and that vector is zero.  -/
Orientation.inner_rotation_pi_div_two_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), inner ℝ ((o.rotation ↑(Real.pi / 2)) x) x = 0
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_iff_limsup_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  UpperSemicontinuousOn f s ↔ ∀ x ∈ s, Filter.limsup f (nhdsWithin x s) ≤ f x
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Every split epimorphism is a regular epimorphism.  -/
CategoryTheory.RegularEpi.ofSplitEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.IsSplitEpi f] → CategoryTheory.RegularEpi f
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.mor : Mathlib.Meta.FunProp.GeneralTheorem → Mathlib.Meta.FunProp.Theorem
-- Mathlib.Topology.Algebra.Order.Field
Filter.Tendsto.const_div_atBot : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {g : α → 𝕜},
  Filter.Tendsto g l Filter.atBot → ∀ (r : 𝕜), Filter.Tendsto (fun n => r / g n) l (nhds 0)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : Inv β] (f : UniformFun α β), UniformFun.toFun f⁻¹ = (UniformFun.toFun f)⁻¹
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_mono_enorm_ae : ∀ {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) → MeasureTheory.eLpNormEssSup f μ ≤ MeasureTheory.eLpNormEssSup g μ
-- Init.Data.UInt.Bitwise
UInt64.toUInt32_and : ∀ (a b : UInt64), (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X₁ X₂).inv.left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).inv
      (CategoryTheory.Limits.pushoutSymmetry (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom)).inv
-- Mathlib.CategoryTheory.Action.Limits
Action.forget_preservesZeroMorphisms : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V], (Action.forget V G).PreservesZeroMorphisms
-- Mathlib.GroupTheory.OrderOfElement
zpow_mod_natCard : ∀ {G : Type u_6} [inst : Group G] (a : G) (n : ℤ), a ^ (n % ↑(Nat.card G)) = a ^ n
-- Mathlib.Analysis.Seminorm
rescale_to_shell_zpow : ∀ {𝕜 : Type u_3} {F : Type u_10} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  {c : 𝕜},
  1 < ‖c‖ →
    ∀ {ε : ℝ},
      0 < ε → ∀ {x : F}, x ≠ 0 → ∃ n, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Measure.integrable_compProd_iff : ∀ {α : Type u_5} {β : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {E : Type u_8}
  [inst : NormedAddCommGroup E] {f : α × β → E},
  MeasureTheory.AEStronglyMeasurable f (μ.compProd κ) →
    (MeasureTheory.Integrable f (μ.compProd κ) ↔
      (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y => f (x, y)) (κ x)) ∧
        MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ)
-- Init.Data.UInt.Lemmas
USize.sub_right_inj : ∀ {a b : USize} (c : USize), c - a = c - b ↔ a = b
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.baseSupp_apply_smul_f : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] (i : ι) (x : ↥H),
  (b.baseSupp i) x • b.f i = -⁅x, b.f i⁆
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.sdiff_singleton_indep : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} {e : α}, M.IsCircuit C → e ∈ C → M.Indep (C \ {e})
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk_sub : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a b : G), ↑(a - b) = ↑a - ↑b
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The `fixingSubgroup` of a finite subset of cardinal `d`
in an `n`-transitive action acts `n-d`-transitively on the complement.  -/
SubMulAction.ofFixingSubgroup.isMultiplyPretransitive : ∀ (G : Type u_1) {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {m n : ℕ}
  [Hn : MulAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s],
  s.ncard + m = n → MulAction.IsMultiplyPretransitive (↥(fixingSubgroup G s)) (↥(SubMulAction.ofFixingSubgroup G s)) m
-- Init.Data.List.Lex
List.le_refl : ∀ {α : Type u_1} [inst : LT α] [i₀ : Std.Irrefl fun x1 x2 => x1 < x2] (l : List α), l ≤ l
-- Mathlib.Order.Filter.AtTopBot.Group
/-- $\lim_{x\to+\infty}|x|=+\infty$  -/
Filter.tendsto_abs_atTop_atTop : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G], Filter.Tendsto abs Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.map_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (a : Quotient (CategoryTheory.isIsomorphicSetoid C)),
  (CategoryTheory.ThinSkeleton.map F).obj a = Quotient.map F.obj ⋯ a
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instUnique : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Subsingleton R] → Unique (MonoidAlgebra R M)
-- Mathlib.Order.Interval.Finset.Basic
Finset.filter_lt_le_eq_Ioc : ∀ {α : Type u_2} (a b : α) [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Fintype α]
  [inst_3 : DecidablePred fun j => a < j ∧ j ≤ b], {j | a < j ∧ j ≤ b} = Finset.Ioc a b
-- Mathlib.Analysis.RCLike.Basic
/-- This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.
 -/
RCLike : semiOutParam (Type u_1) → Type u_1
-- Mathlib.Topology.DiscreteQuotient
/-- The type of discrete quotients of a topological space.  -/
DiscreteQuotient : (X : Type u_5) → [TopologicalSpace X] → Type u_5
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_dvd_opow : ∀ (a : Ordinal.{u_1}) {b c : Ordinal.{u_1}}, b ≤ c → a ^ b ∣ a ^ c
-- Std.Http.Data.URI.Basic
/-- Extracts the path component from a request target, if available.
Returns an empty relative path for targets without a path.
 -/
Std.Http.RequestTarget.path : Std.Http.RequestTarget → Std.Http.URI.Path
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instReprArgSpec.repr : Lean.Doc.ArgSpec✝ → ℕ → Std.Format
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.StdWall.standard.sizeOf_spec : sizeOf Std.Time.TimeZone.StdWall.standard = 1
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.hχ : ∀ {N : ℕ} [inst : NeZero N] (self : DirichletCharacter.BadChar✝ N),
  DirichletCharacter.LFunction (DirichletCharacter.BadChar.χ✝ self) 1 = 0
-- Mathlib.NumberTheory.Chebyshev
/-- The Chebyshev lower bound for `θ`.  -/
Chebyshev.theta_ge : ∀ (n : ℕ), ↑n * Real.log 2 - Real.log (↑n + 1) - 2 * √↑n * Real.log ↑n ≤ Chebyshev.theta ↑n
-- Init.MetaTypes
Lean.Meta.Simp.NormCastConfig.mk.sizeOf_spec : ∀ (toConfig : Lean.Meta.Simp.Config), sizeOf { toConfig := toConfig } = 1 + sizeOf toConfig
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendComp_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt),
  (s.extendComp f g).inv.hom = CategoryTheory.CategoryStruct.id X
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂'Aux.eq_1 : ∀ {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : Semiring R₁] [inst_1 : Semiring S₁] [inst_2 : Semiring R₂] [inst_3 : Semiring S₂] [inst_4 : AddCommMonoid N₂]
  [inst_5 : Module S₁ N₂] [inst_6 : Module S₂ N₂] [inst_7 : SMulCommClass S₂ S₁ N₂] [inst_8 : Fintype n]
  [inst_9 : Fintype m] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) (f : Matrix n m N₂),
  Matrix.toLinearMap₂'Aux σ₁ σ₂ f = LinearMap.mk₂'ₛₗ σ₁ σ₂ (fun v w => ∑ i, ∑ j, σ₂ (w j) • σ₁ (v i) • f i j) ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- This is the addition map `I × I × I → I` for an additive monoid `I`.  -/
CategoryTheory.GradedObject.Monoidal.r₁₂₃ : {I : Type u} → [AddMonoid I] → I × I × I → I
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.instCommRing : (R : Type u_3) →
  (M : Type u_4) →
    [inst : CommRing R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → CommRing (SymmetricAlgebra R M)
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.counit_def : ∀ {R : Type u} [inst : CommRing R] (X : CoalgCat R),
  CategoryTheory.ComonObj.counit = ModuleCat.ofHom CoalgebraStruct.counit
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabDescr.mk.inj : ∀
  {mkInductiveView mkInductiveView_1 :
    Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep1},
  { mkInductiveView := mkInductiveView } = { mkInductiveView := mkInductiveView_1 } →
    mkInductiveView = mkInductiveView_1
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.completeTheory.mem_or_not_mem : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M] (φ : L.Sentence),
  φ ∈ L.completeTheory M ∨ FirstOrder.Language.Formula.not φ ∈ L.completeTheory M
-- Mathlib.RingTheory.DedekindDomain.Instances
_private.Mathlib.RingTheory.DedekindDomain.Instances.0.termP'' : Lean.ParserDescr
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.writeLspMessage : IO.FS.Stream → Lean.JsonRpc.Message → IO Unit
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.mul_param_pow : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β],
  Asymptotics.SuperpolynomialDecay l k f → ∀ (n : ℕ), Asymptotics.SuperpolynomialDecay l k (f * k ^ n)
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_sumRingEquiv : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} (p : MvPolynomial (σ ⊕ ι) R) (i : σ),
  (MvPolynomial.pderiv i) ((MvPolynomial.sumRingEquiv R σ ι) p) =
    (MvPolynomial.sumRingEquiv R σ ι) ((MvPolynomial.pderiv (Sum.inl i)) p)
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.arcosh.eq_1 : ∀ (x : ℝ), Real.arcosh x = Real.log (x + √(x ^ 2 - 1))
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.depth.eq_2 : ∀ {α : Type u_1} (c : RBTree.RBColor) (a : RBTree.RBNode α) (v : α) (b : RBTree.RBNode α),
  (RBTree.RBNode.node c a v b).depth = max a.depth b.depth + 1
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum may be split into such sums over two subsets.  -/
Finset.weightedVSub_sdiff : ∀ {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} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
  s₂ ⊆ s → ∀ (w : ι → k) (p : ι → P), ((s \ s₂).weightedVSub p) w + (s₂.weightedVSub p) w = (s.weightedVSub p) w
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.ext_iff : ∀ {G : Type u_1} {inst : Group G} {x y : FiniteIndexNormalSubgroup G}, x = y ↔ x.carrier = y.carrier
-- Batteries.Tactic.OpenPrivate
/-- The command `export private a b c in foo bar` is similar to `open private`, but instead of opening
them in the current scope it will create public aliases to the private definition. The definition
will exist at exactly the original location and name, as if the `private` keyword was not used
originally.

It will also open the newly created alias definition under the provided short name, like
`open private`.
It is also possible to specify the module instead with
`export private a b c from Other.Module`.
 -/
Lean.Elab.Command.exportPrivate : Lean.ParserDescr
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.GeneralTheorem.mk : Lean.Name →
  Lean.Name →
    List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry) →
      ℕ → Mathlib.Meta.FunProp.GeneralTheorem
-- Mathlib.LinearAlgebra.Basis.Submodule
/-- If the submodule `P` has a finite basis,
`x ∈ P` iff it is a linear combination of basis vectors.  -/
Module.Basis.mem_submodule_iff' : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] {P : Submodule R M} (b : Module.Basis ι R ↥P) {x : M}, x ∈ P ↔ ∃ c, x = ∑ i, c i • ↑(b i)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_div : ∀ {b x y : ℝ}, x ≠ 0 → y ≠ 0 → Real.logb b (x / y) = Real.logb b x - Real.logb b y
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The morphism of sheaves of modules `sheafify α φ ⟶ sheafify α φ'`
induced by morphisms `τ₀ : M₀ ⟶ M₀'` and `τ : A ⟶ A'`
which satisfy `τ₀.hom ≫ φ' = φ ≫ τ.val`.  -/
PresheafOfModules.sheafifyMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          [J.WEqualsLocallyBijective AddCommGrpCat] →
                            {M₀' : PresheafOfModules R₀} →
                              {A' : CategoryTheory.Sheaf J AddCommGrpCat} →
                                (φ' : M₀'.presheaf ⟶ A'.obj) →
                                  [inst_6 : CategoryTheory.Presheaf.IsLocallyInjective J φ'] →
                                    [inst_7 : CategoryTheory.Presheaf.IsLocallySurjective J φ'] →
                                      (τ₀ : M₀ ⟶ M₀') →
                                        (τ : A ⟶ A') →
                                          CategoryTheory.CategoryStruct.comp ((PresheafOfModules.toPresheaf R₀).map τ₀)
                                                φ' =
                                              CategoryTheory.CategoryStruct.comp φ τ.hom →
                                            (PresheafOfModules.sheafify α φ ⟶ PresheafOfModules.sheafify α φ')
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- `tsum_iSup_decode₂` specialized to the complete lattice of sets.  -/
tsum_iUnion_decode₂ : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4}
  [inst_2 : Encodable β] (m : Set α → M),
  m ∅ = 0 → ∀ (s : β → Set α), ∑' (i : ℕ), m (⋃ b ∈ Encodable.decode₂ β i, s b) = ∑' (b : β), m (s b)
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- A Lipschitz continuous map is a locally bounded map.  -/
LipschitzWith.toLocallyBoundedMap : {α : Type u} →
  {β : Type v} →
    [inst : PseudoMetricSpace α] →
      [inst_1 : PseudoMetricSpace β] → {K : NNReal} → (f : α → β) → LipschitzWith K f → LocallyBoundedMap α β
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.C_inv : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (r : k), (MvPowerSeries.C r)⁻¹ = MvPowerSeries.C r⁻¹
-- Std.Async.System
Std.Async.System.UserId.mk.sizeOf_spec : ∀ (toNat : ℕ), sizeOf { toNat := toNat } = 1 + sizeOf toNat