mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φQ : ∀ {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} {h₂ : S₂.LeftHomologyData}
  (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂), ψ.unop.φQ = ψ.φK.unop
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addEmpty.injEq : ∀ {β : Type u} {α : Type v} (id : ℕ) (rupHints : Array ℕ) (id_1 : ℕ) (rupHints_1 : Array ℕ),
  (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints = Std.Tactic.BVDecide.LRAT.Action.addEmpty id_1 rupHints_1) =
    (id = id_1 ∧ rupHints = rupHints_1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → BitVec w → aig.RefVec w
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.sum.match_1.splitter : {α : Type u_2} →
  (motive : (x : ℕ) → (Fin x → α) → Sort u_1) →
    (x : ℕ) →
      (x_1 : Fin x → α) →
        ((x : Fin 0 → α) → motive 0 x) →
          ((v : Fin 1 → α) → motive 1 v) → ((n : ℕ) → (v : Fin (n + 2) → α) → motive n.succ.succ v) → motive x x_1
-- Mathlib.FieldTheory.PerfectClosure
/-- Given a ring `K` of characteristic `p` and a perfect ring `L` of the same characteristic,
any homomorphism `K →+* L` can be lifted to `PerfectClosure K p`.  -/
PerfectClosure.lift : (K : Type u) →
  [inst : CommRing K] →
    (p : ℕ) →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : CharP K p] →
          (L : Type v) →
            [inst_3 : CommSemiring L] → [CharP L p] → [PerfectRing L p] → (K →+* L) ≃ (PerfectClosure K p →+* L)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t).inv = 0
-- Lean.Meta.ArgsPacker
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Unary.curryType.go : Lean.Expr → Lean.Expr → Lean.Expr → Array Lean.Expr → List Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (c c' : C) (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
          (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c' d)))
-- Init.SimpLemmas
and_imp : ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
-- Mathlib.Algebra.Category.FGModuleCat.Basic
LinearMap.id_fgModuleCat_comp : ∀ {R : Type u_1} [inst : Ring R] {G : Type v} [inst_1 : AddCommGroup G] [inst_2 : Module R G] {H : FGModuleCat R}
  (f : G →ₗ[R] ↑H), ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id H).hom ∘ₗ f = f
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.instCoeSortType : CoeSort CommSemiRingCat (Type u)
-- Batteries.Recycling.RBTree.Alter
/-- The root of the tree is `c₀, n₀`-balanced by assumption.  -/
RBTree.RBNode.Path.Balanced.root : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1}, RBTree.RBNode.Path.Balanced c₀ n₀ RBTree.RBNode.Path.root c₀ n₀
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.HasProductsOfShapeAux.inverts : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type)
  [inst_3 : CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J],
  (W.functorCategory (CategoryTheory.Discrete J)).IsInvertedBy (CategoryTheory.Limits.lim.comp L)
-- Std.Data.ExtHashSet.Basic
/-- Inserts multiple mappings into the hash set by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the first occurrence takes precedence.

Note: this precedence behavior is true for `ExtHashSet` and `ExtHashSet.Raw`. The `insertMany` function on
`ExtHashMap`, `DExtHashMap`, `ExtHashMap.Raw` and `DExtHashMap.Raw` behaves differently: it will prefer the last
appearance.
 -/
Std.ExtHashSet.insertMany : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      [EquivBEq α] → [LawfulHashable α] → {ρ : Type v} → [ForIn Id ρ α] → Std.ExtHashSet α → ρ → Std.ExtHashSet α
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionObj : ∀ (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]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᴹᵒᵖ D] (d : D) (c : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj { unmop := c } d
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
signHom.congr_simp : ∀ {α : Type u} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α], signHom = signHom
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.rotateL_lemma₄ : ∀ {a b : ℕ}, 2 * b ≤ 9 * a + 3 → 3 * b ≤ 16 * a + 9
-- Std.Do.SPred.SPred
Std.Do.SPred.conjunction_apply : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {env : List (Std.Do.SPred (σ :: σs))},
  Std.Do.SPred.conjunction env s = Std.Do.SPred.conjunction (List.map (fun x => x s) env)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.below.nil : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive : (a a_1 : s.Pos) → String.Slice.Pattern.Model.IsLongestMatchAtChain pat a a_1 → Prop} (p : s.Pos),
  String.Slice.Pattern.Model.IsLongestMatchAtChain.below ⋯
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.tr_respects : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] {σ : Type u_3} [inst_1 : Inhabited σ]
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst_2 : Inhabited Γ],
  StateTransition.Respects (Turing.TM1.step M) (Turing.TM0.step (Turing.TM1to0.tr M)) fun c₁ c₂ =>
    Turing.TM1to0.trCfg M c₁ = c₂
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (X : CategoryTheory.Arrow C),
  CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor X =
    CategoryTheory.Arrow.isoMk
      {
        hom :=
          CategoryTheory.Limits.pushout.desc
            ((CategoryTheory.Limits.initialIsInitial.ofIso
                  (CategoryTheory.zeroMul CategoryTheory.Limits.initialIsInitial).symm).to
              X.left)
            (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).hom ⋯,
        inv :=
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).inv
            (CategoryTheory.Limits.pushout.inr
              (((CategoryTheory.MonoidalCategory.curriedTensor C).map X.hom).app
                (CategoryTheory.Arrow.mk
                    (CategoryTheory.Limits.initial.to (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).left)
              (((CategoryTheory.MonoidalCategory.curriedTensor C).obj X.left).map
                (CategoryTheory.Arrow.mk
                    (CategoryTheory.Limits.initial.to (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).hom)),
        hom_inv_id := ⋯, inv_hom_id := ⋯ }
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right) ⋯
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- `R` is integrally closed if all integral elements of `Frac(R)` are also elements of `R`.

This definition uses `FractionRing R` to denote `Frac(R)`. See `isIntegrallyClosed_iff`
if you want to choose another field of fractions for `R`.
 -/
IsIntegrallyClosed : (R : Type u_1) → [CommRing R] → Prop
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasHomology_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasHomology], S₂.HasHomology
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.multisetProd : ∀ {α : Type u_1} {l : Filter α} {ι : Type u_17} {R : Type u_18} {𝕜 : Type u_19} [inst : SeminormedCommRing R]
  [inst_1 : NormedField 𝕜] {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜},
  (∀ i ∈ s, f i =O[l] g i) →
    (∃ i ∈ s, f i =o[l] g i) →
      (fun x => (Multiset.map (fun x_1 => f x_1 x) s).prod) =o[l] fun x => (Multiset.map (fun x_1 => g x_1 x) s).prod
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms
of the Schur complement.  -/
Matrix.det_fromBlocks₂₂ : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
  (D : Matrix n n α) [inst_5 : Invertible D], (Matrix.fromBlocks A B C D).det = D.det * (A - B * ⅟D * C).det
-- Init.Data.Array.Subarray
/-- Applies a monadic Boolean predicate to each element in a subarray in reverse order, stopping at the
first element that satisfies the predicate. The element that satisfies the predicate is returned, or
`none` if no element satisfies it.

Example:
```lean example
#eval #["red", "green", "blue"].toSubarray.findRevM? fun x => do
  IO.println x
  return (x.length = 5)
```
```output
blue
green
```
```output
some 5
```
 -/
Subarray.findRevM? : {α : Type} → {m : Type → Type w} → [Monad m] → Subarray α → (α → m Bool) → m (Option α)
-- Init.Data.Int.Order
Int.le_max_left : ∀ (a b : ℤ), a ≤ max a b
-- Lean.Syntax
Lean.Syntax.TopDown.mk.injEq : ∀ (firstChoiceOnly : Bool) (stx : Lean.Syntax) (firstChoiceOnly_1 : Bool) (stx_1 : Lean.Syntax),
  ({ firstChoiceOnly := firstChoiceOnly, stx := stx } = { firstChoiceOnly := firstChoiceOnly_1, stx := stx_1 }) =
    (firstChoiceOnly = firstChoiceOnly_1 ∧ stx = stx_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- Transfinite induction construction of the sigma-algebra generated by a set of sets `s`. At each
step, we add all elements of `s`, the empty set, the complements of already constructed sets, and
countable unions of already constructed sets.

We index this construction by an arbitrary ordinal for simplicity, but by `ω₁` we will have
generated all the sets in the sigma-algebra.

This construction is very similar to that of the Borel hierarchy.  -/
MeasurableSpace.generateMeasurableRec : {α : Type u} → Set (Set α) → Ordinal.{u_1} → Set (Set α)
-- Mathlib.Algebra.Group.Action.Option
Option.instIsScalarTowerOfSMul : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [inst_2 : SMul M N]
  [IsScalarTower M N α], IsScalarTower M N (Option α)
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} {n : ℕ} {Z : C}
  (a : X.obj (Opposite.op { len := n + 1 }) ⟶ Z) (b : Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Z))
  (a_1 : X.obj (Opposite.op { len := n + 1 }) ⟶ Z) (b_1 : Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Z)),
  ({ a := a, b := b } = { a := a_1, b := b_1 }) = (a = a_1 ∧ b = b_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k : α} {v : β},
      (k, v) ∈ Std.DHashMap.Raw.Const.toList m ↔ m.getKey? k = some k ∧ Std.DHashMap.Raw.Const.get? m k = some v
-- Mathlib.Algebra.Lie.TraceForm
/-- The upper and lower central series of `L` are orthogonal w.r.t. the trace form of any Lie module
`M`.  -/
LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {x y : L}
  (k : ℕ), x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((LieModule.traceForm R L M) x) y = 0
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- In a nonempty graph, if `k` is at most the degree of every vertex, it is at most the minimum
degree. Note the assumption that the graph is nonempty is necessary as long as `G.minDegree` is
defined to be a natural.  -/
SimpleGraph.le_minDegree_of_forall_le_degree : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Nonempty V] (k : ℕ),
  (∀ (v : V), k ≤ G.degree v) → k ≤ G.minDegree
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instModule : {α : Type u_1} →
  {R : Type u_6} →
    [inst : Semiring R] →
      [inst_1 : Module R ENNReal] →
        [IsScalarTower R ENNReal ENNReal] → {x : MeasurableSpace α} → Module R (MeasureTheory.Measure α)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.dirSupClosed_of_isClosed : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] {s : Set α} [Topology.IsScott α Set.univ],
  IsClosed s → DirSupClosed s
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.matchAt?_eq : ∀ {s : String.Slice} {pos : s.Pos} {p : Char → Bool},
  String.Slice.Pattern.Model.matchAt? p pos =
    if h₀ : ∃ (h : pos ≠ s.endPos), p (pos.get h) = true then some (pos.next ⋯) else none
-- Batteries.Data.List.Basic
List.product_eq_productTR : @List.product = @List.productTR
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  (CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).inv =
    (CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯
          (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) g) ⋯
          ⋯).desc
      (CategoryTheory.Limits.colimit.cocone
        (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0))
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.getUnusedNames.dummyLDecl : Lean.Name → Lean.LocalDecl
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_sub : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.qExpansion h (⇑f - ⇑g) = UpperHalfPlane.qExpansion h ⇑f - UpperHalfPlane.qExpansion h ⇑g
-- Mathlib.Order.UpperLower.Closure
upperClosure_min : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsUpperSet t → ↑(upperClosure s) ⊆ t
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_reindex : ∀ {m : Type u} {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] [inst_4 : CommRing α] (e : m ≃ n) (A : Matrix m m α) (b : n → α),
  ((Matrix.reindex e e) A).cramer b = A.cramer (b ∘ ⇑e) ∘ ⇑e.symm
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If Cᵒᵖ is cofiltered, then C is filtered.  -/
CategoryTheory.isFiltered_of_isCofiltered_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered Cᵒᵖ], CategoryTheory.IsFiltered C
-- Std.Time.Duration
/-- Subtracts one `Duration` from another.
 -/
Std.Time.Duration.sub : Std.Time.Duration → Std.Time.Duration → Std.Time.Duration
-- Mathlib.Data.Set.SMulAntidiagonal
Set.SMulAntidiagonal.finite_of_finite_fst : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} [inst : SMul G P] [IsLeftCancelSMul G P],
  s.Finite → ∀ (t : Set P) (p : P), (s.smulAntidiagonal t p).Finite
-- Mathlib.CategoryTheory.Join.Basic
/-- Identity morphisms in `C ⋆ D` are inherited from those in `C` and `D`.  -/
CategoryTheory.Join.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (X : CategoryTheory.Join C D) → X.Hom X
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by all the matrices either in `listTransvecCol M` and `listTransvecRow M` turns
the matrix in block-diagonal form.  -/
Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
    ((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod).IsTwoBlockDiagonal
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.powerBasis_gen : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), h.powerBasis.gen = h.root
-- Init.Data.Option.Lemmas
Option.isSome_merge : ∀ {α : Type u_1} {o o' : Option α} {f : α → α → α}, (Option.merge f o o').isSome = (o.isSome || o'.isSome)
-- Mathlib.NumberTheory.NumberField.Norm
RingOfIntegers.isUnit_norm_of_isGalois : ∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  [IsGalois K L] {x : NumberField.RingOfIntegers L}, IsUnit ((RingOfIntegers.norm K) x) ↔ IsUnit x
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.isExtTheorem : Lean.Meta.Grind.Extension → Lean.Name → Lean.CoreM Bool
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- One direction of `div_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative).  -/
div_le_of_le_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 ≤ b → 0 ≤ c → a ≤ c * b → a / b ≤ c
-- Init.Control.Lawful.Basic
/-- `seqRight` is equivalent to the default implementation.  -/
LawfulApplicative.seqRight_eq : ∀ {f : Type u → Type v} {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (x : f α) (y : f β),
  x *> y = Function.const α id <$> x <*> y
-- Mathlib.CategoryTheory.Action.Basic
Action.mkIso_inv_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M.V ≅ N.V)
  (comm :
    autoParam
      (∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g))
      Action.mkIso._auto_1),
  (Action.mkIso f comm).inv.hom = f.inv
-- Mathlib.CategoryTheory.Limits.Cones
/-- A map to the vertex of a cone naturally induces a cone by composition.  -/
CategoryTheory.Limits.Cone.extensions : {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.Cone F) → CategoryTheory.uliftYoneda.{u₁, v₃, u₃}.obj c.pt ⟶ F.cones
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_eq_getLast!_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.maxKey! = t.keys.getLast!
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_sub : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (D1 D2 : LieDerivation R L M), ⇑(D1 - D2) = ⇑D1 - ⇑D2
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- A subcomplex is the union of its closed cells and its base.  -/
Topology.RelCWComplex.Subcomplex.union_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C), D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n ↑j = ↑E
-- Mathlib.Analysis.Complex.Arg
Complex.norm_add_eq_iff : ∀ {x y : ℂ}, ‖x + y‖ = ‖x‖ + ‖y‖ ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
-- Mathlib.Algebra.Group.Action.Defs
inv_smul_eq_iff : ∀ {G : Type u_3} {α : Type u_5} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a b : α}, g⁻¹ • a = b ↔ a = g • b
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasDerivAt_exp_smul_const' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
  (x : 𝔸) (t : 𝕂), HasDerivAt (fun u => NormedSpace.exp (u • x)) (x * NormedSpace.exp (t • x)) t
-- Mathlib.Analysis.Complex.JensenFormula
/-- Reformulation of a finsum that appears in Jensen's formula and in the definition of the counting
function of Value Distribution Theory, as discussed in
`Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean`.
 -/
countingFunction_finsum_eq_finsum_add : ∀ {c : ℂ} {R : ℝ} {D : ℂ → ℤ},
  R ≠ 0 →
    Function.HasFiniteSupport D →
      ∑ᶠ (u : ℂ), ↑(D u) * (Real.log R - Real.log ‖c - u‖) =
        ∑ᶠ (u : ℂ), ↑(D u) * Real.log (R * ‖c - u‖⁻¹) + ↑(D c) * Real.log R
-- Aesop.Tree.AddRapp
Aesop.AddRapp.mk.sizeOf_spec : ∀ (toRuleApplication : Aesop.RuleApplication) (parent : Aesop.GoalRef) (appliedRule : Aesop.RegularRule)
  (successProbability : Aesop.Percent),
  sizeOf
      { toRuleApplication := toRuleApplication, parent := parent, appliedRule := appliedRule,
        successProbability := successProbability } =
    1 + sizeOf toRuleApplication + sizeOf parent + sizeOf appliedRule + sizeOf successProbability
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.opOp_symm_apply : ∀ (M : Type u_3) [inst : Mul M] (a : Mᵐᵒᵖᵐᵒᵖ), (MulEquiv.opOp M).symm a = MulOpposite.unop (MulOpposite.unop a)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.disjoint_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Injective ⇑f → ∀ {H K : AddSubgroup G}, Disjoint H K → Disjoint (AddSubgroup.map f H) (AddSubgroup.map f K)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStmts₁.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.load a q) = Turing.TM2to1.trStmts₁ q
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instMonoidalCategoryStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.AddGrp C)