mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_subset_closure_of_subset_closure : ∀ {α : Type u_2} {M : Matroid α} {X Y : Set α}, X ⊆ M.closure Y → M.closure X ⊆ M.closure Y
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates colimits of shape `J` and `J ≌ J'`, then `F` creates colimits of shape `J'`.  -/
CategoryTheory.createsColimitsOfShapeOfEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {J' : Type w₁} →
              [inst_3 : CategoryTheory.Category.{w'₁, w₁} J'] →
                (J ≌ J') →
                  (F : CategoryTheory.Functor C D) →
                    [CategoryTheory.CreatesColimitsOfShape J F] → CategoryTheory.CreatesColimitsOfShape J' F
-- Mathlib.CategoryTheory.Shift.Linear
CategoryTheory.Shift.linear_of_localization : ∀ (R : Type u_1) [inst : Ring R] {C : Type u_4} [inst_1 : CategoryTheory.Category.{v_1, u_4} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {D : Type u_2}
  [inst_4 : CategoryTheory.Category.{v_2, u_2} D] [inst_5 : CategoryTheory.Preadditive D]
  [inst_6 : CategoryTheory.Linear R D] {M : Type u_3} [inst_7 : AddMonoid M] [inst_8 : CategoryTheory.HasShift C M]
  [∀ (n : M), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [CategoryTheory.Functor.Linear R L]
  [inst_12 : CategoryTheory.HasShift D M] [L.CommShift M] (n : M),
  CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor D n)
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.zero_lt_exp_iff : ∀ {a : EReal}, 0 < a.exp ↔ ⊥ < a
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.MonadRing : (Type → Type) → Type
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.mapValueGroupWithZero_valuation : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B] (a : A),
  (ValuativeExtension.mapValueGroupWithZero A B) ((ValuativeRel.valuation A) a) =
    (ValuativeRel.valuation B) ((algebraMap A B) a)
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_comp_map_inclusion : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {M N M' N' : Submodule R S} (hM : M' ≤ M) (hN : N' ≤ N),
  M.mulMap N ∘ₗ TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN) = M'.mulMap N'
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.eq_1 : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} (f : M → N) (g : N → P) [inst : One P],
  Function.MulExact f g = ∀ (y : N), g y = 1 ↔ y ∈ Set.range f
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix_apply : ∀ {κ : Type w} (A : Type u) {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (b : κ → B)
  (i j : κ), Algebra.traceMatrix A b i j = ((Algebra.traceForm A B) (b i)) (b j)
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
/-- If `w : TwoSquare T L R B` is a Guitart exact square, with `B` essentially surjective,
and `E` is a left extension of `F` along `R`, then `E` is a pointwise
left Kan extension of `F` along `R` provided `E.compTwoSquare w` is a pointwise left
Kan extension of `T ⋙ F` along `L`.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionOfCompTwoSquare : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        {D : Type u₅} →
          [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
            [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D] →
                    {T : CategoryTheory.Functor C₁ C₂} →
                      {L : CategoryTheory.Functor C₁ C₃} →
                        {R : CategoryTheory.Functor C₂ C₄} →
                          {B : CategoryTheory.Functor C₃ C₄} →
                            {F : CategoryTheory.Functor C₂ D} →
                              (E : R.LeftExtension F) →
                                (w : CategoryTheory.TwoSquare T L R B) →
                                  [w.GuitartExact] →
                                    [B.EssSurj] →
                                      (E.compTwoSquare w).IsPointwiseLeftKanExtension → E.IsPointwiseLeftKanExtension
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List α} {k : α}, l.contains k = false → k ∈ t.insertMany l → k ∈ t
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- The **Erdős–Ko–Rado theorem**.

The maximum size of an intersecting family in `α` where all sets have size `r` is bounded by
`(card α - 1).choose (r - 1)`. This bound is sharp.  -/
Finset.erdos_ko_rado : ∀ {n : ℕ} {𝒜 : Finset (Finset (Fin n))} {r : ℕ},
  (↑𝒜).Intersecting → Set.Sized r ↑𝒜 → r ≤ n / 2 → 𝒜.card ≤ (n - 1).choose (r - 1)
-- Init.System.Platform
/-- Gets the LLVM target triple of the current platform, or `""` if this was missing when Lean was
compiled.
 -/
System.Platform.getTarget : Unit → String
-- Mathlib.ModelTheory.Syntax
/-- `iAlls f φ` transforms a `L.Formula (α ⊕ β)` into a `L.Formula α` by universally
quantifying over all variables `Sum.inr _`.  -/
FirstOrder.Language.Formula.iAlls : {L : FirstOrder.Language} → {α : Type u'} → (β : Type v') → [Finite β] → L.Formula (α ⊕ β) → L.Formula α
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddLeftCancelMonoid : {α : Type u_1} → [AddRightCancelMonoid α] → AddLeftCancelMonoid αᵃᵒᵖ
-- Init.Data.String.Lemmas.Pattern.Split.Char
String.Slice.toList_splitToSubslice_char : ∀ {s : String.Slice} {c : Char},
  List.map (String.Slice.copy ∘ String.Slice.Subslice.toSlice) (s.splitToSubslice c).toList =
    List.map String.ofList (List.splitOn c s.copy.toList)
-- Mathlib.Algebra.Group.AddChar
/-- An additive character maps multiples by natural numbers to powers.  -/
AddChar.map_nsmul_eq_pow : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M) (n : ℕ) (x : A),
  ψ (n • x) = ψ x ^ n
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabel_falsum : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ},
  FirstOrder.Language.BoundedFormula.relabel g FirstOrder.Language.BoundedFormula.falsum =
    FirstOrder.Language.BoundedFormula.falsum
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- A structure expressing that `X : C` is the colimit of a functor
`diag : J ⥤ C` such that `P (diag.obj j)` holds for all `j`.  -/
CategoryTheory.ObjectProperty.ColimitOfShape : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C →
      (J : Type u') → [CategoryTheory.Category.{v', u'} J] → C → Type (max (max (max u' u_1) v') v_1)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.sum_pow_le_max_aleph0 : ∀ (x : Cardinal.{u_1}), (Cardinal.sum fun n => x ^ n) ≤ max Cardinal.aleph0 x
-- Mathlib.FieldTheory.Minpoly.Basic
/-- A minimal polynomial is not a unit.  -/
minpoly.not_isUnit : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) [Nontrivial B],
  ¬IsUnit (minpoly A x)
-- Mathlib.Logic.Function.Conjugate
/-- Reinterpret `Function.Semiconj f g g` as `Function.Commute f g`. These two predicates are
definitionally equal but have different dot-notation lemmas.  -/
Function.Semiconj.commute : ∀ {α : Type u_1} {f g : α → α}, Function.Semiconj f g g → Function.Commute f g
-- Batteries.Data.Vector.Lemmas
Vector.scanl_eq_scanlM : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n},
  Vector.scanl f init as = (Vector.scanlM (fun x1 x2 => pure (f x1 x2)) init as).run
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.Idempotents.fullyFaithfulToKaroubi.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.Idempotents.fullyFaithfulToKaroubi C =
    { preimage := fun {X Y} f => f.f, map_preimage := ⋯, preimage_map := ⋯ }
-- Mathlib.Order.CompleteLattice.Lemmas
codisjoint_of_sInf_codisjoint_of_le_of_le : ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α} {c d : Set α},
  (∀ e ∈ c, a ≤ e) → (∀ e ∈ d, b ≤ e) → Codisjoint a b → ⊤ ∉ c ∨ ⊤ ∉ d → Disjoint c d
-- Mathlib.Data.Set.Prod
Set.pi_update_of_notMem : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {i : ι} [inst : DecidableEq ι],
  i ∉ s →
    ∀ (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α j → Set (β j)),
      (s.pi fun j => t j (Function.update f i a j)) = s.pi fun j => t j (f j)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.BinaryInput.lhs : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.BinaryInput → aig.Ref
-- Mathlib.Analysis.Convex.Approximation
/-- A function `φ : E → ℝ` that is convex and lower-semicontinuous is the supremum of a family of
of continuous affine linear functions.  -/
ConvexOn.univ_sSup_affine_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E],
  LowerSemicontinuous φ → ConvexOn ℝ Set.univ φ → sSup {f | f ≤ φ ∧ ∃ l c, f = ⇑RCLike.re ∘ ⇑l + Function.const E c} = φ
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₂_app : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) (X_1 : J),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X).τ₂.app X_1 =
    CategoryTheory.CategoryStruct.id (X.X₂.obj X_1)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The abscissa of (absolute) convergence of the arithmetic function `ζ` is `1`.  -/
ArithmeticFunction.abscissaOfAbsConv_zeta : (LSeries.abscissaOfAbsConv fun n => ↑(ArithmeticFunction.zeta n)) = 1
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsFunOfQuotHom.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} {f f_1 : R ⧸ I →+* A ⧸ J} (e_f : f = f_1) (hf : Function.Surjective ⇑f),
  IsDedekindDomain.idealFactorsFunOfQuotHom hf = IsDedekindDomain.idealFactorsFunOfQuotHom ⋯
-- Aesop.Rule.Forward
Aesop.ForwardRulePriority.unsafe.injEq : ∀ (p p_1 : Aesop.Percent), (Aesop.ForwardRulePriority.unsafe p = Aesop.ForwardRulePriority.unsafe p_1) = (p = p_1)
-- Mathlib.LinearAlgebra.FreeModule.IdealQuotient
/-- A nonzero ideal over a free finite extension of `ℤ` has a finite quotient.
It can't be an instance because of the side condition `I ≠ ⊥`.
 -/
Ideal.finiteQuotientOfFreeOfNeBot : ∀ {S : Type u_3} [inst : CommRing S] [IsDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (I : Ideal S),
  I ≠ ⊥ → Finite (S ⧸ I)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The restriction of scalars by a composition of ring morphisms identifies to the
composition of the restriction of scalars functors.  -/
ModuleCat.restrictScalarsComp' : {R₁ : Type u₁} →
  {R₂ : Type u₂} →
    {R₃ : Type u₃} →
      [inst : Ring R₁] →
        [inst_1 : Ring R₂] →
          [inst_2 : Ring R₃] →
            (f : R₁ →+* R₂) →
              (g : R₂ →+* R₃) →
                (gf : R₁ →+* R₃) →
                  gf = g.comp f →
                    (ModuleCat.restrictScalars gf ≅ (ModuleCat.restrictScalars g).comp (ModuleCat.restrictScalars f))
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Function.Injective.hasSum_comap_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} {f : β → α} {a : α} {g : γ → β} (hg : Function.Injective g),
  (∀ x ∉ Set.range g, f x = 0) → (HasSum (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasSum f a L)
-- Mathlib.Data.SetLike.Basic
SetLike.mem_of_subset : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {s : Set B}, s ⊆ ↑p → ∀ {x : B}, x ∈ s → x ∈ p
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpaceChain_neg : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) (p q : ℤ),
  LieModule.genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = LieModule.genWeightSpaceChain M χ₁ χ₂ p q
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend_left : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β),
  Set.IccExtend h f a = f ⟨a, ⋯⟩
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv'_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (f g : (n → R) →ₗ[R] n → R),
  LinearMap.toMatrixAlgEquiv' (f ∘ₗ g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- A matrix acts trivially on `ℍ` iff it belongs to the center of `GL(2, ℝ)`,
i.e., it's a diagonal matrix.  -/
UpperHalfPlane.forall_smul_eq_self_iff_mem_center : ∀ {g : GL (Fin 2) ℝ}, (∀ (z : UpperHalfPlane), g • z = z) ↔ g ∈ Subgroup.center (GL (Fin 2) ℝ)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplex.congr_simp : ∀ {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 X_1 : CategoryTheory.Abelian.SpectralObject C ι),
  X = X_1 →
    ∀ {i j k l : ι} (f₁ f₁_1 : i ⟶ j),
      f₁ = f₁_1 →
        ∀ (f₂ f₂_1 : j ⟶ k),
          f₂ = f₂_1 →
            ∀ (f₃ f₃_1 : k ⟶ l),
              f₃ = f₃_1 →
                ∀ (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1) (n₁ n₁_1 : ℤ) (e_n₁ : n₁ = n₁_1) (n₂ n₂_1 : ℤ) (e_n₂ : n₂ = n₂_1)
                  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
                  X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ = X_1.shortComplex f₁_1 f₂_1 f₃_1 n₀_1 n₁_1 n₂_1 ⋯ ⋯
-- Mathlib.RingTheory.Ideal.Over
/-- If `P` lies over `p`, then canonically `B ⧸ P` is a `A ⧸ p`-algebra.  -/
Ideal.Quotient.algebraOfLiesOver : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] → (P : Ideal B) → (p : Ideal A) → [P.LiesOver p] → Algebra (A ⧸ p) (B ⧸ P)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] (X : C) (X_1 : D),
  ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso
                  F).hom.app
            X).unmop.app
      X_1 =
    CategoryTheory.CategoryStruct.id ((F.obj X).unmop.obj X_1)
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHom_apply : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) (x : α), (a.ofPermHom τ) x = a.ofPermHomFun τ x
-- Mathlib.NumberTheory.SmoothNumbers
Nat.mem_factoredNumbers : ∀ {s : Finset ℕ} {m : ℕ}, m ∈ Nat.factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
-- Mathlib.Algebra.Polynomial.Sequence
/-- `S i` has strictly monotone natural degree.  -/
Polynomial.Sequence.natDegree_strictMono : ∀ {R : Type u_1} [inst : Semiring R] (S : Polynomial.Sequence R), StrictMono (Polynomial.natDegree ∘ ↑S)
-- Mathlib.GroupTheory.Congruence.Defs
/-- Multiplicative congruence relations preserve integer powers.  -/
Con.zpow : ∀ {M : Type u_1} [inst : Group M] (c : Con M) (n : ℤ) {w x : M}, c w x → c (w ^ n) (x ^ n)
-- Init.Data.UInt.Lemmas
UInt64.toNat_toUInt16 : ∀ (x : UInt64), x.toUInt16.toNat = x.toNat % 2 ^ 16
-- Mathlib.Util.MemoFix
_private.Mathlib.Util.MemoFix.0.memoFixImpl : {α β : Type} → [Nonempty β] → ((α → β) → α → β) → α → β
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b),
  CategoryTheory.CategoryStruct.comp (d.inj i) ((E.sigmaOfIsColimit hc hd).p₂ r) =
    CategoryTheory.CategoryStruct.comp (E.p₂ i.snd) (c.inj i.fst.2)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.pow : ∀ {𝕜 : 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] {z : M} {F' : Type u_21} [inst_6 : NormedRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'}, MDiffAt p z → ∀ (n : ℕ), MDiffAt (p ^ n) z
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.neg_comp : ∀ {M : Type u_2} {N : Type u_3} {G : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommGroup G] (φ : N →+ G) (ψ : M →+ N), (-φ).comp ψ = -φ.comp ψ
-- Init.Omega.LinearCombo
/-- Check if a linear combination is an atom, i.e. the constant term is zero and there is exactly one nonzero coefficient, which is one.  -/
Lean.Omega.LinearCombo.isAtom : Lean.Omega.LinearCombo → Bool
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).i =
    CategoryTheory.CategoryStruct.comp h.i (CategoryTheory.inv φ.τ₂)
-- Mathlib.Analysis.Convex.Slope
StrictConvexOn.secant_strict_mono_aux1 : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (z - x) * f y < (z - y) * f x + (y - x) * f z
-- Init.Data.Array.OfFn
_private.Init.Data.Array.OfFn.0.Array.ofFn.go.eq_1 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (i_1 : ℕ) (h : i_1 + 1 ≤ n),
  Array.ofFn.go✝ f acc i_1.succ h = Array.ofFn.go✝ f (acc.push (f ⟨n - i_1 - 1, ⋯⟩)) i_1 ⋯
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.pop.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} {a : σ → Option (Γ k) → σ}
  {a_1 : Turing.TM2.Stmt Γ Λ σ} {k_1 : K} {a_2 : σ → Option (Γ k_1) → σ} {a_3 : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2.Stmt.pop k a a_1 = Turing.TM2.Stmt.pop k_1 a_2 a_3 → k = k_1 ∧ a ≍ a_2 ∧ a_1 = a_3
-- Init.System.ST
instMonadFinallyST : {σ : Type} → MonadFinally (ST σ)
-- Mathlib.Control.Fold
Traversable.foldr.eq_1 : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] (f : α → β → β) (x : β) (xs : t α),
  Traversable.foldr f x xs = (Traversable.foldMap (Monoid.Foldr.mk ∘ f) xs).get x
-- Mathlib.Data.Sym.Card
/-- Type **stars and bars** for the case `n = 2`.  -/
Sym2.card : ∀ {α : Type u_2} [inst : Fintype α], Fintype.card (Sym2 α) = (Fintype.card α + 1).choose 2
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_prod_X_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (d : σ →₀ ℕ) (x : σ → ℕ) (s : Finset σ),
  MvPolynomial.coeff d (∏ y ∈ s, MvPolynomial.X y ^ x y) = if d = Finsupp.indicator s fun i x_1 => x i then 1 else 0
-- Mathlib.Order.Hom.Lattice
instCoeTCInfHomOfInfHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Min α] [inst_2 : Min β]
  [inst_3 : InfHomClass F α β], instCoeTCInfHomOfInfHomClass = { coe := fun f => { toFun := ⇑f, map_inf' := ⋯ } }
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.instProdIsBoundedSMul : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] [inst_2 : SeminormedRing 𝕜] [inst_3 : Module 𝕜 α] [inst_4 : Module 𝕜 β]
  [IsBoundedSMul 𝕜 α] [IsBoundedSMul 𝕜 β], IsBoundedSMul 𝕜 (WithLp p (α × β))
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.instQuasiIsoNatFromNormalizedChainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C],
  QuasiIso (X.fromNormalizedChainComplex R)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.openPartialHomeomorph_apply : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u : ↥(unitary A)), ↑Unitary.openPartialHomeomorph u = Unitary.argSelfAdjoint u
-- Mathlib.Algebra.Ring.Prod
/-- Product of two commutative semirings is a commutative semiring.  -/
Prod.instCommSemiring : {R : Type u_1} → {S : Type u_3} → [CommSemiring R] → [CommSemiring S] → CommSemiring (R × S)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.core : Lean.Expr → Lean.Expr → Lean.Grind.AC.Expr → Lean.Grind.AC.Expr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.Computability.Ackermann
ack_zero : ∀ (n : ℕ), ack 0 n = n + 1
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S T : J.Cover X}, S = T ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X), (↑S).arrows f ↔ (↑T).arrows f
-- Lean.Data.KVMap
Lean.DataValue.ofSyntax.injEq : ∀ (v v_1 : Lean.Syntax), (Lean.DataValue.ofSyntax v = Lean.DataValue.ofSyntax v_1) = (v = v_1)
-- Lean.Meta.Transform
/-- Visit expression (which should be different from current expression) instead.
The new expression `e` is passed to `pre` again.
 -/
Lean.TransformStep.visit : Lean.Expr → Lean.TransformStep
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  MeasureTheory.IsFiniteMeasure μ ↔ μ Set.univ < ⊤
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- **Alias** of `FunLike.coeAddMonoidHom`. -/
ContDiffMapSupportedIn.coeHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  (Std.DHashMap.filterMap f m).size = m.size ↔ ∀ (a : α) (h : a ∈ m), (f a (m.get a h)).isSome = true
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformContinuous_precomp : ∀ {ι : Type u_1} {ι' : Type u_2} {β : Type u_3} [inst : UniformSpace β] (φ : ι' → ι), UniformContinuous fun x => x ∘ φ