mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.ematch : Lean.Meta.Grind.ExtensionState → Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.Equivalence.toIsoCat_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] (e : C ≌ D) (h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X)
  (h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y)
  (k :
    autoParam (∀ (X : C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯) CategoryTheory.Equivalence.toIsoCat._auto_1)
  (k' :
    autoParam (∀ (Y : D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯)
      CategoryTheory.Equivalence.toIsoCat._auto_3),
  (e.toIsoCat h h' k k').functor = e.functor
-- Std.Do.Triple.SpecLemmas
List.Cursor.mk.inj : ∀ {α : Type u} {l «prefix» suffix : List α} {property : «prefix» ++ suffix = l} {prefix_1 suffix_1 : List α}
  {property_1 : prefix_1 ++ suffix_1 = l},
  { «prefix» := «prefix», suffix := suffix, property := property } =
      { «prefix» := prefix_1, suffix := suffix_1, property := property_1 } →
    «prefix» = prefix_1 ∧ suffix = suffix_1
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.neg : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop} (j : J)
  (x : ↑(F.obj j)), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Order.Category.Lat
Lat.coe_comp : ∀ {X Y Z : Lat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.mk.inj : ∀ {m : Type w → Type w'} {β α : Type w} {inst : Std.Iterator α m β} {iterator : Std.IterM m β} {α_1 : Type w}
  {inst_1 : Std.Iterator α_1 m β} {iterator_1 : Std.IterM m β},
  { α := α, inst := inst, iterator := iterator } = { α := α_1, inst := inst_1, iterator := iterator_1 } →
    α = α_1 ∧ inst ≍ inst_1 ∧ iterator ≍ iterator_1
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.summable_toReal : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (x : α), f x ≠ ⊤ → Summable fun x => (f x).toReal
-- Mathlib.Data.Rat.Lemmas
Rat.mul_den_dvd : ∀ (q₁ q₂ : ℚ), (q₁ * q₂).den ∣ q₁.den * q₂.den
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.smul_def : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (r : R) (f : M →ₚₗ[R] N) (S : Type u) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S], (r • f).toFun' S = r • f.toFun' S
-- Mathlib.Topology.Homeomorph.Defs
/-- Precomposing by a homeomorphism does not change the image of the closure of a preimage.  -/
image_closure_preimage_comp : ∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X → Y),
  IsHomeomorph e → ∀ (f : Y → Z) (s : Set Z), f ∘ e '' closure (f ∘ e ⁻¹' s) = f '' closure (f ⁻¹' s)
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
/-- If `b` and `b'` are `ℚ`-bases of a number field `K` such that
`∀ i j, IsIntegral ℤ (b.toMatrix b' i j)` and `∀ i j, IsIntegral ℤ (b'.toMatrix b i j)` then
`discr ℚ b = discr ℚ b'`.  -/
Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral : ∀ {ι : Type u_2} {ι' : Type u_3} (K : Type u_1) [inst : Field K] [inst_1 : DecidableEq ι] [inst_2 : DecidableEq ι']
  [inst_3 : Fintype ι] [inst_4 : Fintype ι'] [inst_5 : NumberField K] {b : Module.Basis ι ℚ K}
  {b' : Module.Basis ι' ℚ K},
  (∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)) →
    (∀ (i : ι') (j : ι), IsIntegral ℤ (b'.toMatrix (⇑b) i j)) → Algebra.discr ℚ ⇑b = Algebra.discr ℚ ⇑b'
-- Std.Http.Protocol.H1.Reader
/-- Number of header bytes accumulated for the current message.
Counts name + value bytes plus 4 bytes per line for `: ` and `\r\n`.
 -/
Std.Http.Protocol.H1.Reader.headerBytesRead : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → ℕ
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of an `AddMonoid` inherits a zero.  -/
AddSubmonoid.zero : {M : Type u_4} → [inst : AddZeroClass M] → (S : AddSubmonoid M) → Zero ↥S
-- Mathlib.Data.List.Pairwise
/-- **Alias** of the reverse direction of `List.pairwise_reverse`. -/
List.Pairwise.reverse : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise (fun a b => R b a) l → List.Pairwise R l.reverse
-- Mathlib.Order.BoundedOrder.Basic
/-- Pullback a `BoundedOrder`.  -/
BoundedOrder.lift : {α : Type u} →
  {β : Type v} →
    [inst : LE α] →
      [inst_1 : Top α] →
        [inst_2 : Bot α] →
          [inst_3 : LE β] →
            [inst_4 : BoundedOrder β] →
              (f : α → β) → (∀ (a b : α), f a ≤ f b → a ≤ b) → f ⊤ = ⊤ → f ⊥ = ⊥ → BoundedOrder α
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformly.multipliable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {x : β} [inst_1 : UniformSpace α],
  MultipliableUniformly f → Multipliable fun x_1 => f x_1 x
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.div_zero : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  [inst_1 : IsAdicComplete I A], H.div 0 = 0
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.inclusion_mapComp : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b)
  (x_1 : b ⟶ c),
  (CategoryTheory.Bicategory.Pith.inclusion B).mapComp x x_1 =
    CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp x x_1).of
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.inverseFunctorObjIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (e : C ≌ D),
  e.inverseFunctorObjIso.inv = CategoryTheory.CategoryStruct.id (Opposite.op e.inverse)
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
_private.Mathlib.Combinatorics.Enumerative.Catalan.Tree.0.BinaryTree.treesOfNumNodesEq.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- **Krull's height theorem** (also known as **Krullscher Höhensatz**) :
In a commutative Noetherian ring `R`, any prime ideal that is minimal over an ideal generated
by `n` elements has height at most `n`.  -/
Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I p : Ideal R),
  p ∈ I.minimalPrimes → p.height ≤ Cardinal.toENat (Submodule.spanRank I)
-- Mathlib.RingTheory.AdjoinRoot
/-- Adjoining a root is preserved under base change.  -/
AdjoinRoot.tensorAlgEquiv : {R : Type u_6} →
  {S : Type u_7} →
    {T : Type u_8} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                (p : Polynomial S) →
                  (q : Polynomial (TensorProduct R T S)) →
                    Polynomial.map Algebra.TensorProduct.includeRight.toRingHom p = q →
                      TensorProduct R T (AdjoinRoot p) ≃ₐ[T] AdjoinRoot q
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        k ∈ m₂ → Std.DTreeMap.Raw.Const.getD (m₁ ∩ m₂) k fallback = Std.DTreeMap.Raw.Const.getD m₁ k fallback
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- `C` has all limits over any type `J` whose objects and morphisms lie in the same universe
and which has `FinType` objects and morphisms  -/
CategoryTheory.Limits.HasFiniteLimits.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteLimits C] (J : Type)
  [𝒥 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J], CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] {Z : C}
  (h : e.inverse.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (e.inverse.map (CategoryTheory.Functor.OplaxMonoidal.η e.functor)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε e.inverse) h
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.write_move_right_n : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (f : Γ → Γ) (L R : Turing.ListBlank Γ) (n : ℕ),
  Turing.Tape.write (f (R.nth n)) ((Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' L R)) =
    (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' L (Turing.ListBlank.modifyNth f n R))
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_span : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂),
  AffineSubspace.comap (↑f) (affineSpan k s) = affineSpan k (⇑f ⁻¹' s)
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
  (e : CategoryTheory.Arrow.mk i ≅ CategoryTheory.Arrow.mk i') (p : X ⟶ Y),
  CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty i' p
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
Equiv.mulRight₀_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (ha : a ≠ 0), ⇑(Equiv.mulRight₀ a ha) = fun x => x * a
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.StateStack.mk.sizeOf_spec : ∀ {α β σ : Type} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ]
  (stateStack : List (Lean.ScopedEnvExtension.State σ)) (scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β)
  (newEntries : List (Lean.ScopedEnvExtension.Entry α)),
  sizeOf { stateStack := stateStack, scopedEntries := scopedEntries, newEntries := newEntries } =
    1 + sizeOf stateStack + sizeOf scopedEntries + sizeOf newEntries
-- Mathlib.Analysis.Complex.Norm
Complex.norm_zpow : ∀ (z : ℂ) (n : ℤ), ‖z ^ n‖ = ‖z‖ ^ n
-- Mathlib.Algebra.FreeMonoid.Count
/-- `List.count` as a bundled additive monoid homomorphism.  -/
FreeMonoid.count : {α : Type u_1} → [DecidableEq α] → α → FreeMonoid α →* Multiplicative ℕ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_union_of_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeRightOp_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F.rightOp),
  (CategoryTheory.Limits.coneOfCoconeRightOp c).π = CategoryTheory.NatTrans.removeRightOp c.ι
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDeriv_zero_eq_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  iteratedFDeriv 𝕜 0 f = ⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The tensor product of two graded objects `X₁` and `X₂` exists if for any `n`,
the coproduct of the objects `X₁ i ⊗ X₂ j` for `i + j = n` exists.  -/
CategoryTheory.GradedObject.HasTensor : {I : Type u} →
  [AddMonoid I] →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [CategoryTheory.MonoidalCategory C] → CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → Prop
-- Mathlib.Order.Ideal
Order.Cofinal.mk.inj : ∀ {P : Type u_2} {inst : Preorder P} {carrier : Set P} {isCofinal : IsCofinal carrier} {carrier_1 : Set P}
  {isCofinal_1 : IsCofinal carrier_1},
  { carrier := carrier, isCofinal := isCofinal } = { carrier := carrier_1, isCofinal := isCofinal_1 } →
    carrier = carrier_1
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : CategoryTheory.Monad C} → {c c' : CategoryTheory.Kleisli T} → (c.of ⟶ T.obj c'.of) → c.Hom c'
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.brecOn_1.go : {motive_1 : Lean.Lsp.Ipc.CallHierarchy → Sort u} →
  {motive_2 : Array Lean.Lsp.Ipc.CallHierarchy → Sort u} →
    {motive_3 : List Lean.Lsp.Ipc.CallHierarchy → Sort u} →
      (t : Array Lean.Lsp.Ipc.CallHierarchy) →
        ((t : Lean.Lsp.Ipc.CallHierarchy) → t.below → motive_1 t) →
          ((t : Array Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_1 t → motive_2 t) →
            ((t : List Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_2 t → motive_3 t) →
              motive_2 t ×' Lean.Lsp.Ipc.CallHierarchy.below_1 t
-- Lean.Expr
/-- Replace occurrences of the free variable `fvar` in `e` with `v`  -/
Lean.Expr.replaceFVar : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Group.Ext
CancelMonoid.toRightCancelMonoid_injective : ∀ {M : Type u}, Function.Injective (@CancelMonoid.toRightCancelMonoid M)
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.empty : ∀ {X : Type u_2} [inst : TopologicalSpace X], Topology.IsLocallyConstructible ∅
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- If `ξ` is an irrational real number, then there are infinitely many good
rational approximations to `ξ`.  -/
Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational : ∀ {ξ : ℝ}, Irrational ξ → {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.eval_gcd_eq_zero : ∀ {R : Type u} [inst : Field R] [inst_1 : DecidableEq R] {f g : Polynomial R} {α : R},
  Polynomial.eval α f = 0 → Polynomial.eval α g = 0 → Polynomial.eval α (EuclideanDomain.gcd f g) = 0
-- Mathlib.Order.Filter.Pointwise
Filter.smul_le_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f₁ f₂ : Filter α} {g₁ g₂ : Filter β},
  f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ • g₁ ≤ f₂ • g₂
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries.eq_1 : ∀ (G : Type u_1) [inst : Group G] (n : ℕ), Subgroup.upperCentralSeries G n = (Subgroup.upperCentralSeriesAux G n).fst
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₁_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1}
  (left :
    F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⟶ G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4)
  (right :
    F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ⟶ G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)
          right =
        CategoryTheory.CategoryStruct.comp left
          (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5))
      CategoryTheory.ComposableArrows.homMk₁._auto_1)
  (i : Fin (1 + 1)),
  (CategoryTheory.ComposableArrows.homMk₁ left right w).app i =
    match i with
    | ⟨0, isLt⟩ => left
    | ⟨1, isLt⟩ => right
-- Aesop.Stats.File
Aesop.StatsFileRecord.file : Aesop.StatsFileRecord → String
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightId_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightId L R).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Comma.lift.eq_1 : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {C : Type u_4} [inst_5 : CategoryTheory.Category.{v_4, u_4} C]
  (F : CategoryTheory.Functor C (CategoryTheory.Comma L R)) (hP : ∀ (X : C), P (F.obj X).hom)
  (hQ : ∀ {X Y : C} (f : X ⟶ Y), Q (F.map f).left) (hW : ∀ {X Y : C} (f : X ⟶ Y), W (F.map f).right),
  CategoryTheory.MorphismProperty.Comma.lift F hP hQ hW =
    {
      obj := fun X =>
        let __spread.0 := F.obj X;
        { toComma := __spread.0, prop := ⋯ },
      map := fun {X Y} f =>
        let __spread.0 := F.map f;
        { toCommaMorphism := __spread.0, prop_hom_left := ⋯, prop_hom_right := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Logic.Equiv.Prod
Equiv.prodPiEquivSumPi_symm_apply : ∀ {ι : Type u_9} {ι' : Type u_10} (π : ι → Type u) (π' : ι' → Type u) (a : (i : ι ⊕ ι') → Sum.elim π π' i),
  (Equiv.prodPiEquivSumPi π π').symm a = (Equiv.sumPiEquivProdPi (Sum.elim π π')) a
-- Mathlib.RingTheory.WittVector.Defs
WittVector.coeff_mk : ∀ (p : ℕ) {R : Type u_1} (x : ℕ → R), (WittVector.mk p x).coeff = x
-- Init.Data.UInt.Lemmas
USize.toFin_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toFin = OfNat.ofNat n
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Returns `mat[i, j]`.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.getElem : {α : ℕ → ℕ → Type} →
  [self : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α] → {n m : ℕ} → α n m → ℕ → ℕ → ℚ
-- Aesop.Tree.Data
Aesop.Goal.isIrrelevant : Aesop.Goal → Bool
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.ofRepresentableBy_yonedaAddGrpObjRepresentableBy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.AddGrpObj.ofRepresentableBy G (CategoryTheory.yonedaAddGrpObj G)
      (CategoryTheory.yonedaAddGrpObjRepresentableBy G) =
    inst_2
-- Mathlib.Algebra.Group.Units.Equiv
val_unitsEquivProdSubtype_symm_apply : ∀ (α : Type u_2) [inst : Monoid α] (p : { p // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }),
  ↑((unitsEquivProdSubtype α).symm p) = (↑p).1
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.hasProd_iff_tendsto_nat : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m : M} [T2Space M] {f : ℕ → M},
  Multipliable f → (HasProd f m ↔ Filter.Tendsto (fun n => ∏ i ∈ Finset.range n, f i) Filter.atTop (nhds m))
-- Lean.Data.Lsp.CodeActions
/-- Weather code action supports the `data` property which is preserved between a `textDocument/codeAction` and a `codeAction/resolve` request.  -/
Lean.Lsp.CodeActionClientCapabilities.dataSupport? : Lean.Lsp.CodeActionClientCapabilities → Option Bool
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.d.eq_1 : ∀ {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₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) (hn₃ : n₂ + 1 = n₃),
  X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    X.descE f₃ f₄ f₅ (CategoryTheory.CategoryStruct.comp f₃ f₄) ⋯ n₀ n₁ n₂
      (CategoryTheory.CategoryStruct.comp
        (X.δ (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp f₃ f₄) n₁ n₂ hn₂)
        (CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ (CategoryTheory.CategoryStruct.comp f₁ f₂) ⋯ n₂)
          (X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃)))
      ⋯ hn₁ ⋯ ⋯
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →* B` and `ψ : B →* C` define a short exact sequence of topological groups, then we
can integrate a continuous compactly supported function on `B` by integrating over `A` and `C`.  -/
TopologicalGroup.IsSES.integrate : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {E : Type u_4} →
        [inst : Group A] →
          [inst_1 : Group B] →
            [inst_2 : Group C] →
              [inst_3 : TopologicalSpace A] →
                [inst_4 : TopologicalSpace B] →
                  [inst_5 : TopologicalSpace C] →
                    {φ : A →* B} →
                      {ψ : B →* C} →
                        TopologicalGroup.IsSES φ ψ →
                          [IsTopologicalGroup A] →
                            [IsTopologicalGroup B] →
                              [inst_8 : NormedAddCommGroup E] →
                                [inst_9 : MeasurableSpace A] →
                                  [BorelSpace A] →
                                    (μA : MeasureTheory.Measure A) →
                                      [hμA : μA.IsHaarMeasure] →
                                        [inst : NormedSpace ℝ E] →
                                          [IsTopologicalGroup C] →
                                            [LocallyCompactSpace B] →
                                              [inst_13 : MeasurableSpace C] →
                                                [BorelSpace C] →
                                                  (μC : MeasureTheory.Measure C) →
                                                    [hμC : μC.IsHaarMeasure] →
                                                      CompactlySupportedContinuousMap B E →ₗ[ℝ] E
-- Mathlib.Topology.Algebra.Monoid
Submonoid.top_closure_mul_self_eq : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [SeparatelyContinuousMul M] (s : Submonoid M),
  closure ↑s * closure ↑s = closure ↑s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Lean.CoreM
Lean.Core.SavedState.mk : Lean.Core.State → ℕ → Lean.Core.SavedState
-- Mathlib.Data.List.Triplewise
List.triplewise_triple : ∀ {α : Type u_1} {a b c : α} {p : α → α → α → Prop}, List.Triplewise p [a, b, c] ↔ p a b c
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_Icc : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h '' Set.Icc i j = Set.Icc (Fin.castLE h i) (Fin.castLE h j)