mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)) (n : α),
  ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).X.X n = (K.X n).X
-- Batteries.Classes.Order
Std.LawfulLECmp.toOrientedCmp : ∀ {α : Type u_1} {inst : LE α} {cmp : α → α → Ordering} [self : Std.LawfulLECmp cmp], Std.OrientedCmp cmp
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- The standard basis of `σ → P.ring`.  -/
Algebra.PreSubmersivePresentation.basis : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (P : Algebra.PreSubmersivePresentation R S ι σ) → [Finite σ] → Module.Basis σ P.Ring (σ → P.Ring)
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The `finrank` of a finite product is the sum of the `finrank`s.  -/
Module.finrank_pi_fintype : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι] {M : ι → Type w}
  [inst_3 : (i : ι) → AddCommMonoid (M i)] [inst_4 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)]
  [∀ (i : ι), Module.Finite R (M i)], Module.finrank R ((i : ι) → M i) = ∑ i, Module.finrank R (M i)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.iUnion.eq_1 : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f : α → ZFSet.{u}), ZFSet.iUnion f = (ZFSet.range f).sUnion
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.merge.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Sort u_2)
  (h_1 : Unit → motive Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil)
  (h_2 :
    (a₂ : α) →
      (c₂ sibling : Batteries.PairingHeapImp.Heap α) →
        motive Batteries.PairingHeapImp.Heap.nil (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling))
  (h_3 :
    (a₁ : α) →
      (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
        motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling) Batteries.PairingHeapImp.Heap.nil)
  (h_4 :
    (a₁ : α) →
      (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
        (a₂ : α) →
          (c₂ sibling_1 : Batteries.PairingHeapImp.Heap α) →
            motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling)
              (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1)),
  (match Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.nil with
    | Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.nil => h_1 ()
    | Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling => h_2 a₂ c₂ sibling
    | Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.nil => h_3 a₁ c₁ sibling
    | Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1 =>
      h_4 a₁ c₁ sibling a₂ c₂ sibling_1) =
    h_1 ()
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instT5Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T5Space M], T5Space Mᵈᵐᵃ
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos_assoc : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] (m n : ℕ) (h : n < m) {Z : C}
  (h_1 : (if x : n < m then M n else N n) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.SequentialProduct.cone f).π.app (Opposite.op m))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => if x : i < m then M i else N i) n)
        h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π M n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h_1)
-- Mathlib.Topology.Sheaves.Functors
TopCat.Sheaf.pushforward_obj_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Sheaf C X),
  ((TopCat.Sheaf.pushforward C f).obj F).obj = (TopCat.Presheaf.pushforward C f).obj F.obj
-- Mathlib.Order.GaloisConnection.Basic
isGLB_image2_of_isLUB_isLUB : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {s : Set α}
  {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β},
  (∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) →
    (∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) →
      IsLUB s a₀ → IsLUB t b₀ → IsGLB (Set.image2 u s t) (u a₀ b₀)
-- Mathlib.Order.Filter.CardinalInter
/-- Infimum of two `CardinalInterFilter`s is a `CardinalInterFilter`. This is useful, e.g.,
to automatically get an instance for `residual α ⊓ 𝓟 s`.  -/
Filter.cardinalInterFilter_inf_eq : ∀ {α : Type u} {c : Cardinal.{u}} (l₁ l₂ : Filter α) [CardinalInterFilter l₁ c] [CardinalInterFilter l₂ c],
  CardinalInterFilter (l₁ ⊓ l₂) c
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
/-- **Alias** of `SimpleGraph.Walk.isSubwalk_nil_start`. -/
SimpleGraph.Walk.nil_isSubwalk : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (q : G.Walk u v), SimpleGraph.Walk.nil.IsSubwalk q
-- Mathlib.Algebra.Field.Defs
Field.mk : {K : Type u} →
  [toCommRing : CommRing K] →
    [toInv : Inv K] →
      [toDiv : Div K] →
        [toZPow : ZPow K] →
          autoParam (∀ (a b : K), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
            autoParam (∀ (a : K), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) DivInvMonoid.zpow_neg'._autoParam →
                  [toNontrivial : Nontrivial K] →
                    [toNNRatCast : NNRatCast K] →
                      [toRatCast : RatCast K] →
                        (∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                          0⁻¹ = 0 →
                            autoParam (∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den) DivisionRing.nnratCast_def._autoParam →
                              (nnqsmul : ℚ≥0 → K → K) →
                                autoParam (∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a)
                                    DivisionRing.nnqsmul_def._autoParam →
                                  autoParam (∀ (q : ℚ), ↑q = ↑q.num / ↑q.den) DivisionRing.ratCast_def._autoParam →
                                    (qsmul : ℚ → K → K) →
                                      autoParam (∀ (a : ℚ) (x : K), qsmul a x = ↑a * x)
                                          DivisionRing.qsmul_def._autoParam →
                                        Field K
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.intCast_mem : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A) (n : ℤ),
  ↑n ∈ S
-- Init.Data.UInt.BasicAux
/-- Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on
overflow.

This function is overridden at runtime with an efficient implementation.
 -/
USize.ofNat : ℕ → USize
-- Mathlib.Data.Set.Basic
Set.inter_assoc : ∀ {α : Type u} (a b c : Set α), a ∩ b ∩ c = a ∩ (b ∩ c)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, returning `none` if the map is empty.
 -/
Std.ExtDTreeMap.maxKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Option α
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.checkNoUnitMon : Lean.Grind.CommRing.Poly → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasInitial_op_of_hasTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.Limits.HasInitial Cᵒᵖ
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.map.go.eq_def : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a) (acc : Std.DHashMap.Internal.AssocList α γ)
  (a : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.map.go✝ f acc a =
    match a with
    | Std.DHashMap.Internal.AssocList.nil => acc
    | Std.DHashMap.Internal.AssocList.cons k v t =>
      Std.DHashMap.Internal.AssocList.map.go✝ f (Std.DHashMap.Internal.AssocList.cons k (f k v) acc) t
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hom_ext : ∀ {X Y : CommGrpCat} {f g : X ⟶ Y}, CommGrpCat.Hom.hom f = CommGrpCat.Hom.hom g → f = g
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.summable_f_int : ∀ (k : ℕ) (a : ℝ) {t : ℝ}, 0 < t → Summable (HurwitzKernelBounds.f_int k a t)
-- Mathlib.Computability.MyhillNerode
Language.leftQuotient_nil : ∀ {α : Type u} (L : Language α), L.leftQuotient [] = L
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.refl_toAlgHom : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  ↑AlgEquiv.refl = AlgHom.id R A₁
-- Init.Data.Array.Lemmas
Array.size_set! : ∀ {α : Type u_1} (xs : Array α) (i : ℕ) (x : α), (xs.set! i x).size = xs.size
-- Batteries.Data.Fin.Coding
Fin.decodeSubtype.eq_def : ∀ {n : ℕ} (P : Fin n → Prop) [inst : DecidablePred P] (k : Fin (Fin.countP fun x => decide (P x))),
  Fin.decodeSubtype P k =
    match n, P, inst, k with
    | 0, x, x_1, ⟨val, h⟩ => ⋯.elim
    | n.succ, P, inst, ⟨k, hk⟩ =>
      if h0 : P 0 then
        have this := ⋯;
        match k, hk with
        | 0, hk => ⟨0, h0⟩
        | k.succ, hk =>
          match Fin.decodeSubtype (fun i => P i.succ) ⟨k, ⋯⟩ with
          | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i + 1, ⋯⟩, hp⟩
      else
        have this := ⋯;
        match Fin.decodeSubtype (fun i => P i.succ) ⟨k, ⋯⟩ with
        | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i + 1, ⋯⟩, hp⟩
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toTopologicalSpace_iInf : ∀ {α : Type u} [inst : Group α] {ι : Sort u_1} (s : ι → GroupTopology α),
  (⨅ i, s i).toTopologicalSpace = ⨅ i, (s i).toTopologicalSpace
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.symm.injEq : ∀ {R : Type u} [inst : Rack R] {a b : Rack.PreEnvelGroup R} (hab hab_1 : Rack.PreEnvelGroupRel' R a b),
  (hab.symm = hab_1.symm) = (hab = hab_1)
-- Mathlib.RingTheory.RingHom.EssFiniteType
RingHom.EssFiniteType.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => RingHom.EssFiniteType
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.smul_mem_smul_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A} {s : R} {r : Rˣ},
  r • s ∈ spectrum R (r • a) ↔ s ∈ spectrum R a
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- **Gram-Schmidt Orthogonalisation**:
`gramSchmidt` produces an orthogonal system of vectors.  -/
InnerProductSpace.gramSchmidt_orthogonal : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  {a b : ι}, a ≠ b → inner 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f a) (InnerProductSpace.gramSchmidt 𝕜 f b) = 0
-- Batteries.Lean.Meta.Basic
/-- Check whether a metavariable is declared in the given `MetavarContext`.
 -/
Lean.MetavarContext.isExprMVarDeclared : Lean.MetavarContext → Lean.MVarId → Bool
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.gateToCNF.eq_1 : ∀ {α : Type u_1} (output lhs rhs : α) (linv rinv : Bool),
  Std.Sat.AIG.Decl.gateToCNF✝ output lhs rhs linv rinv =
    Std.Sat.CNF.add [(output, true), (lhs, linv), (rhs, rinv)]
      (Std.Sat.CNF.add [(output, false), (rhs, !rinv)]
        (Std.Sat.CNF.add [(output, false), (lhs, !linv)] Std.Sat.CNF.empty))
-- Lean.Expr
Lean.MData.empty : Lean.MData
-- Mathlib.Data.NNRat.Defs
NNRat.mul_def : ∀ (q r : ℚ≥0), q * r = NNRat.divNat (q.num * r.num) (q.den * r.den)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.isIntegral' : ∀ (F : Type u_1) {E : Type u_2} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (x : E), IsIntegral F x
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.monotone_stieltjesFunctionAux : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α],
  ProbabilityTheory.IsMeasurableRatCDF f →
    ∀ (a : α), Monotone (ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a)
-- Lean.Elab.ErrorUtils
/-- Give alternative forms of a string if the `count` is 1 or not.

- `(1).plural == ""`
- `(2).plural == "s"`
- `(1).plural "wug" == "wug"`
- `(2).plural "wug" == "wugs"`
- `(1).plural "it" "they" == "it"`
- `(2).plural "it" "they" == "they"`
 -/
_private.Lean.Elab.ErrorUtils.0.Nat.plural : {α : Sort u_1} →
  [inst : Lean.HasPluralDefaults✝ α] →
    ℕ →
      (singular : optParam α Lean.HasPluralDefaults.singular✝) →
        optParam α (Lean.HasPluralDefaults.plural✝ singular) → α
-- Mathlib.Order.Partition.Finpartition
Finpartition.default_eq_empty : ∀ (α : Type u_1) [inst : Lattice α] [inst_1 : OrderBot α], default = Finpartition.empty α
-- Mathlib.RingTheory.Morita.Matrix
MatrixModCat.toModuleCat_obj_carrier : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι)
  (M : ModuleCat (Matrix ι ι R)), ↑((MatrixModCat.toModuleCat R i).obj M) = ↥(MatrixModCat.toModuleCatObj R (↑M) i)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mul_go : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mul.go p₂ p₁ acc) =
    Lean.Grind.CommRing.Poly.denote ctx acc +
      Lean.Grind.CommRing.Poly.denote ctx p₁ * Lean.Grind.CommRing.Poly.denote ctx p₂
-- Mathlib.Data.List.Sort
List.sortedLT_iff_pairwise : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLT ↔ List.Pairwise (fun x1 x2 => x1 < x2) l
-- Mathlib.Topology.Category.TopCat.Opens
/-- The inclusion `U ⊓ V ⟶ V` as a morphism in the category of open sets.
 -/
TopologicalSpace.Opens.infLERight : {X : TopCat} → (U V : TopologicalSpace.Opens ↑X) → U ⊓ V ⟶ V
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorUSize : LawfulXor USize
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Mathlib.Data.Sum.Interval
Sum.Iic_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : LocallyFiniteOrderBot β] (b : β), Finset.Iic (Sum.inr b) = Finset.map Function.Embedding.inr (Finset.Iic b)
-- Mathlib.Analysis.Complex.Order
Complex.sq_nonneg_iff : ∀ {z : ℂ}, 0 ≤ z ^ 2 ↔ z.im = 0
-- Batteries.Data.Vector.Lemmas
Vector.scanl_empty : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β}, Vector.scanl f init #v[] = #v[init]
-- Mathlib.InformationTheory.Hamming
/-- The Hamming distance function to the naturals.  -/
hammingDist : {ι : Type u_2} →
  {β : ι → Type u_3} → [Fintype ι] → [(i : ι) → DecidableEq (β i)] → ((i : ι) → β i) → ((i : ι) → β i) → ℕ
-- Mathlib.Topology.Separation.Basic
instR0SpaceOfT1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], R0Space X
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.nth_succ : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ) (n : ℕ), l.nth (n + 1) = l.tail.nth n
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph isomorphism is a bijective map on vertex sets that respects adjacency relations.

The notation `G ≃g G'` represents the type of graph isomorphisms.
 -/
SimpleGraph.Iso : {V : Type u_1} → {W : Type u_2} → SimpleGraph V → SimpleGraph W → Type (max u_1 u_2)
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioo_Ioi_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ioo (Filter.principal (Set.Ioi a)) (Filter.principal (Set.Ioi a))
-- Mathlib.Algebra.Module.BigOperators
List.sum_smul : ∀ {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {l : List R}
  {x : M}, l.sum • x = (List.map (fun r => r • x) l).sum
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.toOplax_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F.StrongTrans G) (a : B), η.toOplax.app a = η.app a
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.centralizer.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (s s_1 : Set A),
  s = s_1 → NonUnitalSubalgebra.centralizer R s = NonUnitalSubalgebra.centralizer R s_1
-- Lean.Meta.Tactic.UnifyEq
_private.Lean.Meta.Tactic.UnifyEq.0.Lean.Meta.unifyEq?.substEq : Lean.MVarId →
  Lean.FVarId →
    Lean.Meta.FVarSubst →
      (Lean.MVarId → Lean.Expr → Lean.MetaM Bool) →
        Lean.LocalDecl → Lean.Expr → Lean.Expr → Bool → Lean.MetaM (Option Lean.Meta.UnifyEqResult)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_think : ∀ {α : Type u} (s : Stream'.WSeq α), s.think.destruct = s.destruct.think
-- Mathlib.Topology.MetricSpace.Thickening
Bornology.IsBounded.cthickening : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {δ : ℝ} {E : Set α},
  Bornology.IsBounded E → Bornology.IsBounded (Metric.cthickening δ E)
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app app_1 : (X : C) → F.obj X ⟶ G.obj X) (e_app : app = app_1)
  (naturality :
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (G.map f)),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_one : ∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p], iterateFrobenius R p 1 = frobenius R p
-- Mathlib.SetTheory.Ordinal.Basic
WellOrder.mk : (α : Type u) → (r : α → α → Prop) → IsWellOrder α r → WellOrder
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.tsum_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  [CompleteSpace α] [T0Space α] {f : β × γ → α}, Summable f → ∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul_k.eq_1 : ∀ (p : Int.Internal.Linear.Poly) (k : ℤ),
  p.mul_k k =
    Bool.rec
      (Int.Internal.Linear.Poly.rec (fun k' => Int.Internal.Linear.Poly.num (k.mul k'))
        (fun k' v x ih => Int.Internal.Linear.Poly.add (k.mul k') v ih) p)
      (Int.Internal.Linear.Poly.num 0) (k.beq' 0)
-- Mathlib.Data.LawfulXor.Basic
instCommutativeXor_mathlib : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α], Std.Commutative XorOp.xor
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.toListRev.eq_1 : ∀ {α : Type u_1} (xs : Array α), xs.toListRev = Array.foldl (fun l t => t :: l) [] xs
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_of_pow_lt_pow_left₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀]
  (n : ℕ), 0 ≤ b → a ^ n < b ^ n → a < b
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular epimorphism in `C` induces a regular monomorphism in `Cᵒᵖ`.  -/
CategoryTheory.RegularEpi.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.RegularEpi f → CategoryTheory.RegularMono f.op
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.mk''.inj : ∀ {callerName : Lean.Name} {decrTactic? : Option Lean.Elab.DecreasingBy}
  {callerMeasures calleeMeasures : Array Lean.Elab.WF.GuessLex.BasicMeasure}
  {rcc : Lean.Elab.WF.GuessLex.RecCallWithContext}
  {cache : IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel)))} {callerName_1 : Lean.Name}
  {decrTactic?_1 : Option Lean.Elab.DecreasingBy}
  {callerMeasures_1 calleeMeasures_1 : Array Lean.Elab.WF.GuessLex.BasicMeasure}
  {rcc_1 : Lean.Elab.WF.GuessLex.RecCallWithContext}
  {cache_1 : IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel)))},
  { callerName := callerName, decrTactic? := decrTactic?, callerMeasures := callerMeasures,
        calleeMeasures := calleeMeasures, rcc := rcc, cache := cache } =
      { callerName := callerName_1, decrTactic? := decrTactic?_1, callerMeasures := callerMeasures_1,
        calleeMeasures := calleeMeasures_1, rcc := rcc_1, cache := cache_1 } →
    callerName = callerName_1 ∧
      decrTactic? = decrTactic?_1 ∧
        callerMeasures = callerMeasures_1 ∧ calleeMeasures = calleeMeasures_1 ∧ rcc = rcc_1 ∧ cache = cache_1
-- Mathlib.Algebra.Star.StarAlgHom
/-- Transitivity of `StarAlgEquiv`.  -/
StarAlgEquiv.trans : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      {C : Type u_5} →
        [inst : Add A] →
          [inst_1 : Add B] →
            [inst_2 : Mul A] →
              [inst_3 : Mul B] →
                [inst_4 : SMul R A] →
                  [inst_5 : SMul R B] →
                    [inst_6 : Star A] →
                      [inst_7 : Star B] →
                        [inst_8 : Add C] →
                          [inst_9 : Mul C] →
                            [inst_10 : SMul R C] → [inst_11 : Star C] → (A ≃⋆ₐ[R] B) → (B ≃⋆ₐ[R] C) → A ≃⋆ₐ[R] C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert! k v t).get k ⋯ = v
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_lt_zero : ∀ {α : Type u} [inst : Zero α] [inst_1 : LT α] {a : α}, ↑a < 0 ↔ a < 0
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceFrom.eq_1 : ∀ (s : String.Slice) (pos : s.Pos),
  s.sliceFrom pos =
    { str := s.str, startInclusive := pos.str, endExclusive := s.endExclusive, startInclusive_le_endExclusive := ⋯ }
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.isoOfEq_hom_ι_assoc : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U = V) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom (CategoryTheory.CategoryStruct.comp V.ι h) =
    CategoryTheory.CategoryStruct.comp U.ι h
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.transAssocReparamAux.eq_1 : ∀ (t : ↑unitInterval),
  Path.Homotopy.transAssocReparamAux t =
    if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.smartUnfoldingReduce?.goMatch : Lean.Expr → OptionT Lean.MetaM Lean.Expr