mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Util.LibraryNote
/-- Entry for library notes in the environment extension.

We only store the name, and look up the constant's docstring to find its contents.
 -/
Batteries.Util.LibraryNote.LibraryNoteEntry : Type
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongrₗ_refl : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (S : Type u_12) [inst_5 : Semiring S]
  [inst_6 : Module S N] [inst_7 : SMulCommClass R S N],
  AlternatingMap.domDomCongrₗ S (Equiv.refl ι) = LinearEquiv.refl S (M [⋀^ι]→ₗ[R] N)
-- Lean.Elab.Tactic.Basic
/-- The tactic monad, which extends the term elaboration monad `TermElabM` with state that contains the
current goals (`Lean.Elab.Tactic.State`, accessible via `MonadStateOf`) and local information about
the current tactic's name and whether error recovery is enabled (`Lean.Elab.Tactic.Context`,
accessible via `MonadReaderOf`).
 -/
Lean.Elab.Tactic.TacticM : Type → Type
-- Mathlib.Order.RelClasses
/-- **Alias** of `isTrans_le`. -/
transitive_le : ∀ {α : Type u} [inst : Preorder α], IsTrans α LE.le
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {v : β},
      List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = some (k', v) ↔ t.getKey? k = some k' ∧ t[k]? = some v
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.Exact ↔ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
-- Mathlib.Analysis.Normed.Group.Completeness
/-- In a complete normed additive group, every absolutely convergent series converges in the
space.  -/
NormedAddCommGroup.summable_imp_tendsto_of_complete : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [CompleteSpace E] (u : ℕ → E),
  (Summable fun x => ‖u x‖) → ∃ a, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, u i) Filter.atTop (nhds a)
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.filteredClosure.below.coeq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsFiltered.filteredClosure f a → Prop} {j j' : C}
  (a : CategoryTheory.IsFiltered.filteredClosure f j) (a_1 : CategoryTheory.IsFiltered.filteredClosure f j')
  (f_1 f' : j ⟶ j'),
  CategoryTheory.IsFiltered.filteredClosure.below a →
    motive j a →
      CategoryTheory.IsFiltered.filteredClosure.below a_1 →
        motive j' a_1 → CategoryTheory.IsFiltered.filteredClosure.below ⋯
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.unpair₂ : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ}, Nat.Primrec' f → Nat.Primrec' fun v => (Nat.unpair (f v)).2
-- Init.Data.List.ToArray
/-- Variant of `foldrM_toArray` with a side condition for the `start` argument.  -/
List.foldrM_toArray' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : ℕ} [inst : Monad m] (f : α → β → m β) (init : β)
  (l : List α), start = l.toArray.size → Array.foldrM f init l.toArray start = List.foldrM f init l
-- Mathlib.Data.List.Rotate
List.rotate_replicate : ∀ {α : Type u} (a : α) (n k : ℕ), (List.replicate n a).rotate k = List.replicate n a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_not_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  ¬P ≈ Q → W'.add P Q = W'.addXYZ P Q
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln_bound : ∀ {k : ℕ} {c : Nat.Partrec.Code} {n x : ℕ}, x ∈ Nat.Partrec.Code.evaln k c n → n < k
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.isIso_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.IsIso f.unop ↔ CategoryTheory.IsIso f
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mem_equivPair_tail_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i j : ι} {w : Monoid.CoprodI.Word M} (m : M i),
  ⟨i, m⟩ ∈ ((Monoid.CoprodI.Word.equivPair j) w).tail.toList ↔
    ⟨i, m⟩ ∈ w.toList.tail ∨ i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩
-- Mathlib.Topology.Order.OrderClosed
IsGLB.range_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {f : β → α} {a : α}
  {F : Filter β} [F.NeBot], (∀ (i : β), a ≤ f i) → Filter.Tendsto f F (nhds a) → IsGLB (Set.range f) a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceLT : Lean.Meta.Simp.Simproc
-- Init.Data.UInt.Lemmas
USize.lt_iff_toBitVec_lt : ∀ {a b : USize}, a < b ↔ a.toBitVec < b.toBitVec
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.sub_eq' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : SubtractionCommMonoid α] [inst_1 : Neg β],
  Function.Antiperiodic f c → f (c - x) = -f (-x)
-- Init.Data.Vector.Lemmas
/-- Variant of `map_const` using a lambda rather than `Function.const`.  -/
Vector.map_const' : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {b : β}, Vector.map (fun x => b) xs = Vector.replicate n b
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- The obvious equivalence `Pushout f g ≃ Pushout' f g`.  -/
CategoryTheory.Limits.Types.Pushout.equivPushout' : {S X₁ X₂ : Type u} →
  (f : S ⟶ X₁) → (g : S ⟶ X₂) → CategoryTheory.Limits.Types.Pushout f g ≃ CategoryTheory.Limits.Types.Pushout' f g
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.mapCoeffs_repr : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {R' : Type u_13} [inst_3 : Semiring R'] [inst_4 : Module R' M] (f : R ≃+* R')
  (h : ∀ (c : R) (x : M), f c • x = c • x),
  (b.mapCoeffs f h).repr =
    LinearEquiv.restrictScalars R' b.repr ≪≫ₗ Finsupp.mapRange.linearEquiv (Module.compHom.toLinearEquiv f.symm).symm
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.inhabited : {α : Type u} → Inhabited (WithZero α)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.coproducts_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.coproducts.{w, v, u} W f ↔ ∃ J, W.colimitsOfShape (CategoryTheory.Discrete J) f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termL₁_1 : Lean.ParserDescr
-- Batteries.Data.List.Lemmas
List.instNeZeroNatLengthCons : ∀ {α : Type u_1} {a : α} {l : List α}, NeZero (a :: l).length
-- Init.Data.List.Perm
List.Perm.nil_eq : ∀ {α : Type u_1} {l : List α}, [].Perm l → [] = l
-- Mathlib.Analysis.Normed.Order.UpperLower
upperClosure_interior_subset' : ∀ {α : Type u_1} [inst : NormedCommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] (s : Set α),
  ↑(upperClosure (interior s)) ⊆ interior ↑(upperClosure s)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.subgraphOfAdj : ∀ {V : Type u_1} {G : SimpleGraph V} {v w : V} (h : G.Adj v w), (G.subgraphOfAdj h).IsMatching
-- Init.Data.String.Basic
/-- Returns the byte at the position `pos` of a string.
 -/
String.Pos.byte : {s : String} → (pos : s.Pos) → pos ≠ s.endPos → UInt8
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.fixingSubgroupEquivFixingSubgroup.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M} (hg : g • t = s),
  SubMulAction.fixingSubgroupEquivFixingSubgroup hg =
    (MulEquiv.subgroupMap (MulAut.conj g) (fixingSubgroup M t)).trans (MulEquiv.subgroupCongr ⋯)
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.coe_inf' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SemilatticeInf β]
  [inst_3 : ContinuousInf β] {ι : Type u_3} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)),
  ⇑(s.inf' H f) = s.inf' H fun i => ⇑(f i)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_one_right_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, x ∣ y → IsRelPrime x (y + 1)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
/-- The following should not be a `FunLike` instance because then the coercion `⇑` would get
unfolded to `FunLike.coe` instead of `WithCStarModule.equiv`.  -/
WithCStarModule.instCoeFunForall : {A : Type u_1} → {ι : Type u_2} → (E : ι → Type u_3) → CoeFun (WithCStarModule A ((i : ι) → E i)) fun x => (i : ι) → E i
-- Mathlib.Algebra.Algebra.Unitization
/-- This prevents `mk x` being printed as `{ toProd := x }` by `delabStructureInstance`.  -/
Unitization.delabMk : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.eq_1 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s : AffineSubspace R P) (x y : P), s.SSameSide x y = (s.WSameSide x y ∧ x ∉ s ∧ y ∉ s)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_eq_sign_of_equiv : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (f : Equiv.Perm α) (g : Equiv.Perm β) (e : α ≃ β),
  (∀ (x : α), e (f x) = g (e x)) → Equiv.Perm.sign f = Equiv.Perm.sign g
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h.homologyIso.hom h.rightHomologyIso.inv = S.rightHomologyIso.inv
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.mk : (toAddGrp : AddGrpCat) → [isFinite : Finite ↑toAddGrp] → FiniteAddGrp.{u}
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.getExtension? : Lean.Name → Lean.CoreM (Option Lean.Meta.Grind.Extension)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumElim_inl_inr : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language},
  FirstOrder.Language.LHom.sumInl.sumElim FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.id (L.sum L')
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.antisymm : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ L₁ → L₁ = L₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
deriv_csinh : ∀ {f : ℂ → ℂ} {x : ℂ}, DifferentiableAt ℂ f x → deriv (fun x => Complex.sinh (f x)) x = Complex.cosh (f x) * deriv f x
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE Int64
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair F] (A : adj.toComonad.Coalgebra),
  CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F
-- Mathlib.Topology.EMetricSpace.Defs
/-- EMetric space instance on the multiplicative opposite of an emetric space.  -/
instEMetricSpaceMulOpposite : {α : Type u_2} → [EMetricSpace α] → EMetricSpace αᵐᵒᵖ
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.applyCoe.go : FBinopElab.SRec → FBinopElab.Tree✝ → Option Lean.Expr → Lean.Elab.TermElabM FBinopElab.Tree✝
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filterMap_replicate.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.Do.WPMonad m ps]
  [inst_5 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {f : β → γ} {g : δ → γ → δ} {init : δ}
  {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄ Std.IterM.fold (fun d b => g d (f b)) init it ⦃Q⦄ → ⦃P⦄ Std.IterM.fold g init (Std.IterM.map f it) ⦃Q⦄
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- The linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M`.

This is the `LinearEquiv` version of `Finsupp.curryEquiv`.  -/
Finsupp.curryLinearEquiv : {α : Type u_9} →
  {β : Type u_10} →
    (R : Type u_11) →
      {M : Type u_12} →
        [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- A commutative monoid object internal to a monoidal category.
 -/
CategoryTheory.CommMon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → Type (max u₁ v₁)
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.mk.inj : ∀ {M : Type u_10} {N : Type u_11} {inst : Zero M} {inst_1 : Zero N} {toFun : M → N} {map_zero' : toFun 0 = 0}
  {toFun_1 : M → N} {map_zero'_1 : toFun_1 0 = 0},
  { toFun := toFun, map_zero' := map_zero' } = { toFun := toFun_1, map_zero' := map_zero'_1 } → toFun = toFun_1
-- Mathlib.Logic.Denumerable
Denumerable.int : Denumerable ℤ
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- An adjunction of braided functors lifts to an adjunction of their lifts to commutative group
objects.  -/
CategoryTheory.Adjunction.mapCommGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.CartesianMonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} →
                  {G : CategoryTheory.Functor D C} →
                    (F ⊣ G) → [inst_6 : F.Braided] → [inst_7 : G.Braided] → F.mapCommGrp ⊣ G.mapCommGrp
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mk : {R : Type u} →
  [inst : NonAssocRing R] →
    (toSubsemiring : Subsemiring R) → (∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier) → Subring R
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.noZeroDivisors : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [NoZeroDivisors A] [inst_3 : Algebra R A]
  (S : Subalgebra R A), NoZeroDivisors ↥S
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.edit : Lean.Lsp.TextDocumentEdit → Lean.Lsp.DocumentChange
-- Init.Data.String.Iter.Basic
/-- Convenience function for turning an iterator into an array of strings, provided the output of the
iterator implements `ToString`.
 -/
Std.Iter.toStringArray : {α β : Type} → [Std.Iterator α Id β] → [ToString β] → Std.Iter β → Array String
-- Mathlib.Order.Category.BddLat
BddLat.dualEquiv_functor : BddLat.dualEquiv.functor = BddLat.dual
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_mono : ∀ {R : Type u} [inst : Semiring R] {I J K L : Ideal R}, I ≤ K → J ≤ L → I * J ≤ K * L
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsInducedInv : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  [inst_2 : Φ.functor.IsEquivalence] [inst_3 : Φ.IsInduced] [inst_4 : W₂.RespectsIso], Φ.inv.IsInduced
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_neg_right_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- An operator `T` is normal iff `‖T v‖ = ‖(adjoint T) v‖` for all `v`.  -/
ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E], IsStarNormal T ↔ ∀ (v : E), ‖T v‖ = ‖(ContinuousLinearMap.adjoint T) v‖
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j k : D.J) {Z : C}
  (h : CategoryTheory.Limits.pullback (D.f i j) (D.f i k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (D.t' j k i) (CategoryTheory.CategoryStruct.comp (D.t' k i j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (D.f j k) (D.f j i)).hom
      (CategoryTheory.CategoryStruct.comp (D.t' j i k)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (D.f i k) (D.f i j)).hom h))
-- Mathlib.FieldTheory.Relrank
/-- If `A ≤ B`, then `IntermediateField.relrank A B` is `[B : A]`  -/
IntermediateField.relrank_eq_rank_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (h : A ≤ B), A.relrank B = Module.rank ↥A ↥(IntermediateField.extendScalars h)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalNormedCommRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalNormedCommRing β] → NonUnitalNormedCommRing (ZeroAtInftyContinuousMap α β)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
PartialOrder.mem_range_nerve_σ_iff : ∀ {X : Type u_1} [inst : PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n + 1 }))
  (i : Fin (n + 1)),
  s ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (CategoryTheory.nerve X) i)) ↔
    s.obj i.castSucc = s.obj i.succ
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_dvd_gcd_mul_left_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α), gcd m n ∣ gcd m (k * n)
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.beq.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (h_1 : Unit → motive Nat.zero Nat.zero) (h_2 : (n : ℕ) → motive Nat.zero n.succ)
  (h_3 : (n : ℕ) → motive n.succ Nat.zero) (h_4 : (n m : ℕ) → motive n.succ m.succ),
  (match Nat.zero, Nat.zero with
    | Nat.zero, Nat.zero => h_1 ()
    | Nat.zero, n.succ => h_2 n
    | n.succ, Nat.zero => h_3 n
    | n.succ, m.succ => h_4 n m) =
    h_1 ()
-- Lean.CoreM
Lean.MonadDeclNameGenerator : (Type → Type) → Type
-- Aesop.Script.StructureDynamic
Aesop.Script.structureDynamicCore : Lean.Meta.SavedState → Lean.MVarId → Aesop.Script.UScript → Lean.MetaM (Option (Aesop.Script.UScript × Bool))
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
/-- Bijection between `MulOpposite` of a subalgebra `S` and its opposite.  -/
Subalgebra.mopAlgEquivOp : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → (↥S)ᵐᵒᵖ ≃ₐ[R] ↥S.op
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` reflects isomorphisms, and we already know that the colimit exists in the source and `F`
preserves it, then `F` creates that colimit.  -/
CategoryTheory.createsColimitOfReflectsIsomorphismsOfPreserves : {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] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.ReflectsIsomorphisms] →
                  [CategoryTheory.Limits.HasColimit K] →
                    [CategoryTheory.Limits.PreservesColimit K F] → CategoryTheory.CreatesColimit K F
-- Mathlib.LinearAlgebra.LinearPMap
Submodule.toLinearPMap_range : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (g : Submodule R (E × F)),
  (∀ x ∈ g, x.1 = 0 → x.2 = 0) → g.toLinearPMap.toFun.range = Submodule.map (LinearMap.snd R E F) g
-- Mathlib.Topology.Order.WithTop
WithBot.continuousOn_unbotA : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : Nonempty ι],
  ContinuousOn WithBot.unbotA {a | a ≠ ⊥}
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.done.inj : ∀ {result result_1 : String},
  Std.Http.Internal.UnquoteState.done✝ result = Std.Http.Internal.UnquoteState.done✝ result_1 → result = result_1
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.Zoomed.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → Sort u_2) (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (x : α)
  (r : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.Path.root)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) → (x : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent x r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (x : α) → (parent : RBTree.RBNode.Path α) → motive (RBTree.RBNode.Path.right c l x parent)),
  (match RBTree.RBNode.Path.left c parent x r with
    | RBTree.RBNode.Path.root => h_1 ()
    | RBTree.RBNode.Path.left c parent x r => h_2 c parent x r
    | RBTree.RBNode.Path.right c l x parent => h_3 c l x parent) =
    h_2 c parent x r
-- Init.Data.List.Sublist
List.mem_of_mem_take : ∀ {α : Type u_1} {i : ℕ} {a : α} {l : List α}, a ∈ List.take i l → a ∈ l
-- Lean.Meta.Tactic.Grind.Extension
/-- Instantiates the theorem only if less than `n` instances have been generated for this theorem.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts : ℕ → Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- Given `L₁ : E' × E' → ℝ` and `L₂ : F' × F' → ℝ` two continuous bilinear forms,
`diagonalStrongDualProd L₁ L₂` is the continuous bilinear form over `(E × F)'`
which maps `(x, y) : (E × F)' × (E × F)'` to
`L₁ (fun (a, b) ↦ x a) (fun (a, b) ↦ y a) + L₂ (fun (a, b) ↦ x b) (fun (a, b) ↦ y b)`.

This is an implementation detail used in `IndepFun.hasGaussianLaw`.  -/
_private.Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence.0.ContinuousLinearMap.diagonalStrongDualProd : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            (StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) →
              (StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ) → StrongDual ℝ (E × F) →L[ℝ] StrongDual ℝ (E × F) →L[ℝ] ℝ
-- Mathlib.Algebra.Group.Units.Defs
Units.mkOfMulEqOne.eq_1 : ∀ {α : Type u} [inst : Monoid α] [inst_1 : IsDedekindFiniteMonoid α] (a b : α) (hab : a * b = 1),
  Units.mkOfMulEqOne a b hab = { val := a, inv := b, val_inv := hab, inv_val := ⋯ }
-- Mathlib.Computability.RegularExpressions
RegularExpression.instZero : {α : Type u_1} → Zero (RegularExpression α)
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- In a unital algebra, elements of the character space are algebra homomorphisms.  -/
WeakDual.CharacterSpace.instAlgHomClass : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommRing 𝕜] [NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : ContinuousAdd 𝕜] [inst_4 : ContinuousConstSMul 𝕜 𝕜] [inst_5 : TopologicalSpace A] [inst_6 : Semiring A]
  [inst_7 : Algebra 𝕜 A], AlgHomClass (↑(WeakDual.characterSpace 𝕜 A)) 𝕜 A 𝕜