mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Hom
/-- If `φ₁` and `φ₂` are `R`-algebra homomorphisms with the
domain of `φ₁` equal to the codomain of `φ₂`, then
`φ₁.comp φ₂` is the algebra homomorphism `x ↦ φ₁ (φ₂ x)`.
 -/
AlgHom.comp : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      {C : Type u₁} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Semiring C] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra R B] → [inst_6 : Algebra R C] → (B →ₐ[R] C) → (A →ₐ[R] B) → A →ₐ[R] C
-- Mathlib.Probability.Kernel.Disintegration.Basic
ProbabilityTheory.Kernel.condKernelCountable.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : Countable α] (κCond κCond_1 : α → ProbabilityTheory.Kernel β Ω)
  (e_κCond : κCond = κCond_1) (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y),
  ProbabilityTheory.Kernel.condKernelCountable κCond h_atom = ProbabilityTheory.Kernel.condKernelCountable κCond_1 ⋯
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isStrictlySupported_mapHomologicalComplex_obj_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} {D : Type u_4}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Category.{v_2, u_4} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (K : HomologicalComplex C c') (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  (e : c.Embedding c') [F.Faithful],
  ((F.mapHomologicalComplex c').obj K).IsStrictlySupported e ↔ K.IsStrictlySupported e
-- Mathlib.Data.Finset.Image
/-- If a finset `t` is a subset of the image of another finset `s` under `f`, then it is equal to the
image of a subset of `s`.

For the version where `s` is a set, see `subset_set_image_iff`.
 -/
Finset.subset_image_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β},
  t ⊆ Finset.image f s ↔ ∃ s' ⊆ s, Finset.image f s' = t
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_sub : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Module R (Additive ℤˣ)] (s : ℤˣ) (x y : R), s ^ (x - y) = s ^ x / s ^ y
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Alternative constructor for `PreservesRightKanExtension`, phrased in terms of
`RightExtension.IsUniversal` instead. See `PreservesRightKanExtension.mk_of_preserves_isUniversal`
for a similar constructor taking as input a single `RightExtension`.  -/
CategoryTheory.Functor.PreservesRightKanExtension.mk' : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C),
  (∀ {E : L.RightExtension F} (a : CategoryTheory.CostructuredArrow.IsUniversal E),
      Nonempty
        (CategoryTheory.CostructuredArrow.IsUniversal
          ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj E))) →
    G.PreservesRightKanExtension F L
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesRxiSize.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : Std.Rxi.HasSize α] [inst_3 : Std.Rxi.HasSize β] {f : Std.PRange.UpwardEnumerable.Map α β},
  (∀ {b : α}, Std.Rxi.HasSize.size b = Std.Rxi.HasSize.size (f.toFun b)) → f.PreservesRxiSize
-- Mathlib.RingTheory.LinearDisjoint
LinearEquiv.ofFinrankEq.congr_simp : ∀ {R : Type u} (M : Type v) (M' : Type v') [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [inst_6 : Module.Free R M']
  [inst_7 : StrongRankCondition R] [inst_8 : Module.Finite R M] [inst_9 : Module.Finite R M']
  (cond : Module.finrank R M = Module.finrank R M'),
  LinearEquiv.ofFinrankEq M M' cond = LinearEquiv.ofFinrankEq M M' cond
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_indicator_of_mem_union_disjoint : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β)
  (f : β → α), Pairwise (Function.onFun Disjoint s) → ∀ i ∈ ⋃ d, s d, ∑' (d : γ), (s d).indicator f i = f i
-- Init.Data.Array.Lemmas
Array.getElem?_setIfInBounds_self : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α}, (xs.setIfInBounds i a)[i]? = if i < xs.size then some a else none
-- Lean.Environment
Lean.instBEqModuleIdx : BEq Lean.ModuleIdx
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.lift_fac : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f]
  (H' : Set.range ⇑g ⊆ Set.range ⇑f),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.lift f g H') f = g
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_eq'`. -/
setOf_gauge_lt_eq' : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Absorbent ℝ s → ∀ (a : ℝ), {x | gauge s x < a} = ⋃ r, ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Lifting universe and morphism levels preserves wide pullback diagrams.  -/
CategoryTheory.Limits.WidePullbackShape.uliftEquivalence : {J : Type w} →
  CategoryTheory.ULiftHom (ULift.{w', w} (CategoryTheory.Limits.WidePullbackShape J)) ≌
    CategoryTheory.Limits.WidePullbackShape (ULift.{w', w} J)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.toGradedRingHom_ofClass : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {F : Type u_11}
  [inst_9 : FunLike F A B] [inst_10 : GradedFunLike F 𝒜 ℬ] [inst_11 : AlgHomClass F R A B] (f : F),
  (GradedAlgHom.ofClass f).toGradedRingHom = ↑f
-- Init.Data.BitVec.Lemmas
BitVec.toFin_setWidth : ∀ {w v : ℕ} {x : BitVec w}, (BitVec.setWidth v x).toFin = Fin.ofNat (2 ^ v) x.toNat
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.DTreeMap.getKeyLED : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → α → α
-- Mathlib.Data.Nat.Bitwise
Nat.bitwise_zero_right : ∀ {f : Bool → Bool → Bool} (n : ℕ), Nat.bitwise f n 0 = if f true false = true then n else 0
-- Mathlib.Order.Filter.Finite
Filter.EventuallyEq.iInter : ∀ {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α},
  (∀ (i : ι), s i =ᶠ[l] t i) → ⋂ i, s i =ᶠ[l] ⋂ i, t i
-- Mathlib.Data.List.ReduceOption
List.reduceOption_concat : ∀ {α : Type u_1} (l : List (Option α)) (x : Option α), (l.concat x).reduceOption = l.reduceOption ++ x.toList
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.toSubmonoid_closure : ∀ {A : Type u_4} [inst : AddZeroClass A] (S : Set A),
  AddSubmonoid.toSubmonoid (AddSubmonoid.closure S) = Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
/-- The class of epimorphisms modulo a Serre class: given a
Serre class `P : ObjectProperty C`, this is the class of morphisms `f`
such that `cokernel f` satisfies `P`.  -/
CategoryTheory.ObjectProperty.epiModSerre : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (P : CategoryTheory.ObjectProperty C) → [P.IsSerreClass] → CategoryTheory.MorphismProperty C
-- Init.Prelude
/-- Create syntax node with 8 children  -/
Lean.Syntax.node8 : Lean.SourceInfo →
  Lean.SyntaxNodeKind →
    Lean.Syntax →
      Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
/-- If `F : J ⥤ C` is well-order-continuous and `h : α <i J` is a principal
segment such that `h.top` is a limit element, then
`F.obj h.top` identifies to the colimit of the `F.obj j` for `j : α`.  -/
CategoryTheory.Functor.isColimitOfIsWellOrderContinuous' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : PartialOrder J] →
        (F : CategoryTheory.Functor J C) →
          [F.IsWellOrderContinuous] →
            {α : Type u_1} →
              [inst_3 : PartialOrder α] →
                (f : α <i J) → Order.IsSuccLimit f.top → CategoryTheory.Limits.IsColimit (f.cocone F)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.comp_eval : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Polynomial R)
  (q : PolynomialModule R M) (r : R),
  (PolynomialModule.eval r) ((PolynomialModule.comp p) q) = (PolynomialModule.eval (Polynomial.eval r p)) q
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.mvPolynomialBasis_repr_symm_single : ∀ (R : Type u) [inst : CommRing R] (σ : Type u_1) (i : σ) (x : MvPolynomial σ R),
  ((KaehlerDifferential.mvPolynomialBasis R σ).repr.symm fun₀ | i => x) =
    x • (KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The program corresponding to state transitions at the end of a stack. Here we start out just
after the top of the stack, and should end just after the new top of the stack.  -/
Turing.TM2to1.trStAct : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        [DecidableEq K] →
          {k : K} →
            Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ →
              Turing.TM2to1.StAct K Γ σ k → Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.types_π_surjective : ∀ (D : CategoryTheory.GlueData (Type u_1)), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom D.π)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- `id e a` is the expression for `𝟙 a`, where `e` is the underlying lean expression.  -/
Mathlib.Tactic.BicategoryLike.Mor₁.id : Lean.Expr → Mathlib.Tactic.BicategoryLike.Obj → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.SetTheory.Cardinal.Basic
/-- See also `Cardinal.aleph0_le_mul_iff`.  -/
Cardinal.aleph0_le_mul_iff : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (Cardinal.aleph0 ≤ a ∨ Cardinal.aleph0 ≤ b)
-- Mathlib.GroupTheory.IsSubnormal
/-- If `H` is a subnormal subgroup of `K` and `K` is a subnormal subgroup of `G`,
then `H` is a subnormal subgroup of `G`.
 -/
Subgroup.IsSubnormal.trans : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  H ≤ K → (H.subgroupOf K).IsSubnormal → K.IsSubnormal → H.IsSubnormal
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
/-- The left adjoint of the functor `Hom(G, ·)`, which can be thought of as `· ⊗ G`.  -/
CategoryTheory.IsGrothendieckAbelian.tensorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] →
        (G : C) → CategoryTheory.Functor (ModuleCat (CategoryTheory.End G)ᵐᵒᵖ) C
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.multiples_fg : ∀ {M : Type u_1} [inst : AddMonoid M] (r : M), (AddSubmonoid.multiples r).FG
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_eq_abs_det : ∀ {U : Type u_5} [inst : NormedAddCommGroup U] [inst_1 : InnerProductSpace ℝ U] [inst_2 : FiniteDimensional ℝ U]
  (f : U →ₗ[ℝ] U), f.normDet = |LinearMap.det f|
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untopD_add : ∀ {α : Type u_1} [inst : Add α] {a b : WithTop α} {c : α},
  a ≠ ⊤ → b ≠ ⊤ → WithTop.untopD c (a + b) = WithTop.untopD c a + WithTop.untopD c b
-- Lean.Meta.Tactic.Grind.EqResolution
_private.Lean.Meta.Tactic.Grind.EqResolution.0.Lean.Meta.Grind.topsortMVars?.visit : Array Lean.Expr → Lean.Expr → Lean.Meta.Grind.TopSortM Unit
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Convenience reformulation of the second iterated derivative, as a map from `E` to linear maps
`E ⊗[𝕜] E →ₗ[𝕜] F`.
 -/
tensorIteratedFDerivTwo : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → (E → F) → E → TensorProduct 𝕜 E E →ₗ[𝕜] F
-- Batteries.Data.String.Matcher
/-- Returns true iff `pattern` occurs as a substring of `s`.
 -/
String.containsSubstr : String → Substring.Raw → Bool
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.add : {α : Type u} →
  [inst : Lean.Grind.Semiring α] →
    Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalName : Lean.Meta.ReduceEval Lean.Name
-- Mathlib.Data.Nat.ModEq
Nat.modulus_mul_add_modEq_iff : ∀ {n a b c : ℕ}, n * b + a ≡ c [MOD n] ↔ a ≡ c [MOD n]
-- Lean.Level
Lean.Level.PP.Context.mk.sizeOf_spec : ∀ (mvars : Bool) (lIndex? : Lean.LMVarId → Option ℕ), sizeOf { mvars := mvars, lIndex? := lIndex? } = 1 + sizeOf mvars
-- Lean.CoreM
/-- Throws an internal interrupt exception if cancellation has been requested. The exception is not
caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
level of elaboration. In particular, we want to skip producing further incremental snapshots after
the exception has been thrown.

Like `checkSystem` but without the global heartbeat check, for callers that have their own
heartbeat tracking (e.g. `SynthInstance`).
  -/
Lean.Core.checkInterrupted : Lean.CoreM Unit
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_le_sum : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {ι : Type u_6} {s : Finset ι} {f : ι → R} {g : Γ₀}, (∀ i ∈ s, g ≤ v (f i)) → g ≤ v (∑ i ∈ s, f i)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- Given `ℌ : DayConvolutionInternalHom F H`, if we think of `H.obj G`
as the internal hom `[F, G]`, then this is the transformation
corresponding to the component at `G` of the "evaluation" natural morphism
`F ⊛ [F, _] ⟶ 𝟭`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_app : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            [inst_4 : CategoryTheory.MonoidalClosed V] →
              {F G H : CategoryTheory.Functor C V} →
                [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F H] →
                  CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H →
                    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F H ⟶ G)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.continuous_comp_left : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (f : A →ₜ* B),
  Continuous fun g => g.comp f
-- Mathlib.Order.Filter.Subsingleton
Filter.subsingleton_bot : ∀ {α : Type u_1}, ⊥.Subsingleton
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_inv_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ≅ g) {Z : F.obj a ⟶ F.obj b} (h : F.map g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map₂ η.inv) (CategoryTheory.CategoryStruct.comp (F.map₂ η.hom) h) = h
-- Mathlib.Algebra.BigOperators.Finprod
/-- The product of `f y` over `y ∈ g '' s` equals the product of `f (g i)` over `s` provided that
`g` is injective on `s`.  -/
finprod_mem_image : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set β} {g : β → α},
  Set.InjOn g s → ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_bot : ∀ {α : Type u_1} [inst : LE α], ↑⊥ = ∅
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.quot_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat),
  Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) RingCat.Colimits.Prequotient.zero = 0
-- Mathlib.Data.List.Sublists
List.sublists_append : ∀ {α : Type u} (l₁ l₂ : List α),
  (l₁ ++ l₂).sublists = do
    let x ← l₂.sublists
    List.map (fun x_1 => x_1 ++ x) l₁.sublists
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.foldl.match_1.splitter : {α : Type u_3} →
  {β : Type u_1} →
    (motive : α → List β → Sort u_2) →
      (x : α) →
        (x_1 : List β) → ((a : α) → motive a []) → ((a : α) → (b : β) → (l : List β) → motive a (b :: l)) → motive x x_1
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.id_app : ∀ {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 : CategoryTheory.Functor C (Type w)) (X : C) (x : A.obj X),
  (CategoryTheory.Functor.HomObj.id A).app X x = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Data.Int.ModEq
Int.add_mul_modulus_modEq_iff : ∀ {n a b c : ℤ}, a + b * n ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
-- Mathlib.Analysis.Normed.Lp.PiLp
_private.Mathlib.Analysis.Normed.Lp.PiLp.0.PiLp.isUniformInducing_ofLp_aux : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : Fact (1 ≤ p)] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
  [inst_2 : Fintype ι], IsUniformInducing WithLp.ofLp
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_injective : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o],
  Function.Injective Matrix.blockDiagonal'
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (L : F →L[𝕜] G) {f : E → F} {s : Set E} {x : E}
  {N : WithTop ℕ∞} {n : ℕ},
  ContDiffWithinAt 𝕜 N f s x →
    UniqueDiffOn 𝕜 s → x ∈ s → ↑n ≤ N → ‖iteratedFDerivWithin 𝕜 n (⇑L ∘ f) s x‖ ≤ ‖L‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
-- Init.Data.Repr
/-- Adds parentheses to `f` if the precedence `prec` from the context is at least that of function
application.

Together with `reprArg`, this can be used to correctly parenthesize function application
syntax.
 -/
Repr.addAppParen : Std.Format → ℕ → Std.Format
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.subsetProdLex : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] {s : Set (Lex (α × β))},
  ((fun x => (ofLex x).1) '' s).IsPWO → (∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO) → s.IsPWO
-- Mathlib.RepresentationTheory.Induced
Rep.coinvariantsTensorIndNatIso_inv_app : ∀ {k : Type u} [inst : CommRing k] {G H : Type u} [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{u, u, u} k G) (X : Rep.{u, u, u} k H),
  (Rep.coinvariantsTensorIndNatIso φ A).inv.app X = Rep.coinvariantsTensorIndInv φ A X
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.integrable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ (a : α) (q : ℚ), MeasureTheory.Integrable (fun c => f (a, c) q) (ν a)
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.monoCoprodOfHasZeroMorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.Limits.MonoCoprod C
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.X j ≅ K.opCycles j` when the differential to `j` is zero.  -/
HomologicalComplex.pOpcyclesIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) → c.prev j = i → K.d i j = 0 → [inst_2 : K.HasHomology j] → K.X j ≅ K.opcycles j
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
List.sum_toFinset : ∀ {ι : Type u_1} {M : Type u_5} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] (f : ι → M) {l : List ι},
  l.Nodup → l.toFinset.sum f = (List.map f l).sum
-- Init.Core
/-- Transfer a decidability proof across an equality of propositions.  -/
decidable_of_decidable_of_eq : {p q : Prop} → [Decidable p] → p = q → Decidable q
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_zero : Complex.sinh 0 = 0
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.exists_notMem_col : ∀ (μ : YoungDiagram) (j : ℕ), ∃ i, (i, j) ∉ μ.cells
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.withSeminorms_eq : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E], WithSeminorms p → t = p.moduleFilterBasis.topology
-- Init.Data.Int.Gcd
Int.gcd_eq_zero_iff : ∀ {a b : ℤ}, a.gcd b = 0 ↔ a = 0 ∧ b = 0
-- Init.System.Promise
/-- Checks whether the promise has already been resolved, i.e. whether access to `result*` will return
immediately.
 -/
IO.Promise.isResolved : {α : Type} → IO.Promise α → BaseIO Bool
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_ofClass : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {F : Type u_11}
  [inst_9 : FunLike F A B] [inst_10 : GradedFunLike F 𝒜 ℬ] [inst_11 : AlgHomClass F R A B] (f : F),
  ⇑(GradedAlgHom.ofClass f) = ⇑f
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.normal.injEq : ∀ (promise promise_1 : IO.Promise Unit),
  (Std.CancellationToken.Consumer.normal promise = Std.CancellationToken.Consumer.normal promise_1) =
    (promise = promise_1)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_max?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true → t.max?.isSome = true
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the left.  -/
vectorSpan_range_eq_span_range_vsub_left : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i0 : ι),
  vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i0 -ᵥ p i)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_sub_comm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] (f g : α → E) (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm (f - g) p μ = MeasureTheory.lpNorm (g - f) p μ
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.solved : Lean.Meta.Simp.UsedSimps → Aesop.SimpResult
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instNontrivialSubtypeMemTop : ∀ {G : Type u_1} [inst : AddGroup G] [Nontrivial G], Nontrivial ↥⊤