mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.UniformMulAction
IsUniformInducing.uniformContinuousConstSMul : ∀ {M : Type v} {X : Type x} {Y : Type y} [inst : UniformSpace X] [inst_1 : UniformSpace Y] [inst_2 : SMul M X]
  [inst_3 : SMul M Y] [UniformContinuousConstSMul M Y] {f : X → Y},
  IsUniformInducing f → (∀ (c : M) (x : X), f (c • x) = c • f x) → UniformContinuousConstSMul M X
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.add_closedBall_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → s + Metric.closedBall 0 δ = Metric.cthickening δ s
-- Init.Data.Array.Lemmas
Array.set_pop : ∀ {α : Type u_1} {xs : Array α} {x : α} {i : ℕ} (h : i < xs.pop.size), xs.pop.set i x h = (xs.set i x ⋯).pop
-- Mathlib.CategoryTheory.Quotient
/-- A type synonym for `C`, thought of as the objects of the quotient category.  -/
CategoryTheory.Quotient : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → HomRel C → Type u_1
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset_eq_singleton_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g
-- Mathlib.Data.FP.Basic
FP.Float.isZero : [C : FP.FloatCfg] → FP.Float → Bool
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.of_compProd : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {𝓩 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨}
  {κ : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.SFinite P] [ProbabilityTheory.IsSFiniteKernel κ] {Z : Ω → 𝓩}
  {η : ProbabilityTheory.Kernel (𝓧 × 𝓨) 𝓩} [ProbabilityTheory.IsMarkovKernel η],
  ProbabilityTheory.HasCondDistrib (fun a => (Y a, Z a)) X (κ.compProd η) P →
    ProbabilityTheory.HasCondDistrib Z (fun a => (X a, Y a)) η P
-- Init.Data.BitVec.Lemmas
BitVec.intMin_le_iff_msb_eq_true : ∀ {w : ℕ} {x : BitVec w}, 0 < w → (BitVec.intMin w ≤ x ↔ x.msb = true)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instLE.eq_1 : ∀ {M : Type u_1} [inst : AddGroup M] [inst_1 : Lattice M],
  ArchimedeanOrder.instLE = { le := fun a b => ∃ n, |ArchimedeanOrder.val b| ≤ n • |ArchimedeanOrder.val a| }
-- Lean.Parser.Do
Lean.Parser.Term.doIfCond : Lean.Parser.Parser
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.ofRepr : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] → (E ≃ₗᵢ[𝕜] ↥(lp (fun x => 𝕜) 2)) → HilbertBasis ι 𝕜 E
-- Mathlib.Analysis.Convex.NNReal
NNReal.Icc_subset_segment : ∀ {x y : NNReal}, Set.Icc x y ⊆ segment NNReal x y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
  {v : β k} {h : Std.Internal.List.containsKey a (Std.Internal.List.insertEntryIfNew k v l) = true},
  Std.Internal.List.getKey a (Std.Internal.List.insertEntryIfNew k v l) h =
    if h' : (k == a) = true ∧ Std.Internal.List.containsKey k l = false then k else Std.Internal.List.getKey a l ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.neg_le_self`. -/
neg_le_self : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftMono α] {a : α}, 0 ≤ a → -a ≤ a
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- **Alias** of the reverse direction of `Matrix.nonsingular_submatrix_equiv_iff`. -/
Matrix.Nonsingular.submatrix_equiv : ∀ {n : Type u_1} {m : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommSemiring R] {A : Matrix n n R} {e₁ e₂ : m ≃ n},
  A.Nonsingular → (A.submatrix ⇑e₁ ⇑e₂).Nonsingular
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.div₀` -/
TendstoLocallyUniformlyOn.fun_div₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X] {s : Set X}
  {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      ContinuousOn f s →
        ContinuousOn g s →
          (∀ x ∈ s, g x ≠ 0) → TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 / G i i_1) (fun i => f i / g i) l s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.maxKey? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Data.Matrix.Basic
RingEquiv.mapMatrix_trans : ∀ {m : Type u_2} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonAssocSemiring α] [inst_3 : NonAssocSemiring β] [inst_4 : NonAssocSemiring γ] (f : α ≃+* β) (g : β ≃+* γ),
  f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- If `X` is a finite-rank set, and `Y` is a superset of `X` of rank no larger than that of `X`,
then `X` and `Y` have the same closure.  -/
Matroid.IsRkFinite.closure_eq_closure_of_subset_of_eRk_ge_eRk : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → X ⊆ Y → M.eRk Y ≤ M.eRk X → M.closure X = M.closure Y
-- Mathlib.Algebra.Category.CoalgCat.Basic
/-- A type alias for `CoalgHom` to avoid confusion between the categorical and
algebraic spellings of composition.  -/
CoalgCat.Hom : {R : Type u} → [inst : CommRing R] → CoalgCat R → CoalgCat R → Type v
-- Init.System.IO
/-- The read/write cursor's position in the buffer.  -/
IO.FS.Stream.Buffer.pos : IO.FS.Stream.Buffer → ℕ
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ≅ y) (z : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.inv z)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.hom z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y z)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Auxiliary definition for `add`  -/
ONote.addAux : ONote → ℕ+ → ONote → ONote
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.mk : IO.CancelToken → IO.CancelToken → IO.Promise Unit → IO.Promise Unit → Lean.Server.RequestCancellationToken
-- Mathlib.GroupTheory.Congruence.Defs
/-- Given binary relations `r, s` with `r` contained in `s`, the
smallest additive congruence relation containing `s` contains the smallest additive congruence
relation containing `r`.  -/
AddCon.addConGen_mono : ∀ {M : Type u_1} [inst : Add M] {r s : M → M → Prop}, (∀ (x y : M), r x y → s x y) → addConGen r ≤ addConGen s
-- Init.Data.BitVec.Bootstrap
BitVec.eq_of_getElem_eq : ∀ {n : ℕ} {x y : BitVec n}, (∀ (i : ℕ) (hi : i < n), x[i] = y[i]) → x = y
-- Lean.Parser.Basic
/-- Parses `#` characters immediately after a `"`.
The `closingNum` variable counts the number of `#`s seen after the `"`.
Note: `num > 0` since the `num = 0` case is entirely handled by `normalState`.
 -/
_private.Lean.Parser.Basic.0.Lean.Parser.rawStrLitFnAux.closingState : String.Pos.Raw → ℕ → ℕ → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.map_add_left_Ico : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  [ExistsAddOfLE α] [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Finset.map (addLeftEmbedding c) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_finsetSum : ∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_5} {s : Finset ι} {f : ι → α → E},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → ∀ (m : MeasurableSpace α), μ[∑ i ∈ s, f i | m] =ᵐ[μ] ∑ i ∈ s, μ[f i | m]
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
/-- The endomorphism `QInfty : K[X] ⟶ K[X]` obtained from the `Q q` by passing to the limit.  -/
AlgebraicTopology.DoldKan.QInfty : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X
-- Qq.SortLocalDecls
Qq.SortLocalDecls.visitExpr : Lean.Expr → Qq.SortLocalDecls.M Unit
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_empty' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, nhdsSetWithin ∅ s = ⊥
-- Init.Data.Vector.Basic
Vector.tail_eq_cast_extract : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), xs.tail = Vector.cast ⋯ (xs.extract 1)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The lifted cone on `Over X` is a limit cone if the original cone was limiting
and `J` is nonempty.  -/
CategoryTheory.Over.isLimitLiftCone : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        [Nonempty J] →
          (D : CategoryTheory.Functor J T) →
            {X : T} →
              (s : D ⟶ (CategoryTheory.Functor.const J).obj X) →
                (c : CategoryTheory.Limits.Cone D) →
                  (p : c.pt ⟶ X) →
                    (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.π.app j) (s.app j) = p) →
                      CategoryTheory.Limits.IsLimit c →
                        CategoryTheory.Limits.IsLimit (CategoryTheory.Over.liftCone D s c p hp)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofHom_hom : ∀ {A B : ProfiniteAddGrp.{u}} (f : A ⟶ B), ProfiniteAddGrp.ofHom (ProfiniteAddGrp.Hom.hom f) = f
-- Mathlib.Algebra.Module.ULift
ULift.mulDistribMulAction' : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] → [inst_1 : Monoid M] → [MulDistribMulAction R M] → MulDistribMulAction R (ULift.{u_1, v} M)
-- Mathlib.Data.EReal.Basic
EReal.coe_one : ↑1 = 1
-- Mathlib.Analysis.Convex.StdSimplex
/-- The standard one-dimensional simplex in `Fin 2 → 𝕜` is equivalent to the unit interval.
This bijection sends the zeroth vertex `Pi.single 0 1` to `0` and
the first vertex `Pi.single 1 1` to `1`.  -/
stdSimplexEquivIcc : (𝕜 : Type u_1) →
  [inst : Ring 𝕜] → [inst_1 : PartialOrder 𝕜] → [IsOrderedRing 𝕜] → ↑(stdSimplex 𝕜 (Fin 2)) ≃ ↑(Set.Icc 0 1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback
-- Init.Data.Int.Pow
Int.pow_add : ∀ (a : ℤ) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.eulerChar_prod : ∀ (𝕜 : Type u_2) {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : PartialOrder β]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : LocallyFiniteOrder β] [inst_5 : DecidableEq α] [inst_6 : DecidableEq β]
  [inst_7 : DecidableLE α] [inst_8 : DecidableLE β] [inst_9 : BoundedOrder α] [inst_10 : BoundedOrder β],
  IncidenceAlgebra.eulerChar 𝕜 (α × β) = IncidenceAlgebra.eulerChar 𝕜 α * IncidenceAlgebra.eulerChar 𝕜 β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_succ_right_eq_append_map : ∀ {m n : ℤ}, m < n → (m<...n + 1).toArray = #[m + 1] ++ Array.map (fun x => x + 1) (m<...n).toArray
-- Mathlib.Order.Completion
DedekindCut.instLinearOrder : {α : Type u_1} → [inst : LinearOrder α] → LinearOrder (DedekindCut α)
-- Lean.DocString.Extension
Lean.VersoModuleDocs.instInhabitedSnippet : Inhabited Lean.VersoModuleDocs.Snippet
-- Mathlib.Data.ENNReal.Operations
ENNReal.exists_add_lt_of_add_lt : ∀ {x y z : ENNReal}, y + z < x → ∃ y' > y, ∃ z' > z, y' + z' < x
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.collectArraySizes : Lean.Meta.Match.Problem → Array ℕ
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instPartialOrder : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → PartialOrder (ClosedSubmodule R M)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.isClique : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, G.IsNClique n s → G.IsClique ↑s
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.weightedTotalDegree_rename_of_injective : ∀ {R : Type u_3} [inst : CommSemiring R] {σ : Type u_5} {τ : Type u_6} {e : σ → τ} {w : τ → ℕ} {P : MvPolynomial σ R},
  Function.Injective e →
    MvPolynomial.weightedTotalDegree w ((MvPolynomial.rename e) P) = MvPolynomial.weightedTotalDegree (w ∘ e) P
-- Qq.Simp
/-- For `pre` procedures, continue transformation by visiting subexpressions, and then
executing `post` procedures.

For `post` procedures, this is equivalent to returning `visit`.
 -/
Lean.Meta.Simp.StepQ.continue : {u : Lean.Level} →
  {α : Q(Sort u)} → {e : Q(«$α»)} → optParam (Option (Lean.Meta.Simp.ResultQ e)) none → Lean.Meta.Simp.StepQ e
-- Init.Data.OfScientific
Float32.ofScientific : ℕ → Bool → ℕ → Float32
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.model_iff_subset_completeTheory : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T : L.Theory}, M ⊨ T ↔ T ⊆ L.completeTheory M
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- Let `C` be a Grothendieck abelian category. Assume that `G : C` is a generator
of `C`. Then, any morphism in `C` is a transfinite composition of pushouts
of monomorphisms in the family `generatingMonomorphisms G` which consists
of the inclusions of the subobjects of `G`.  -/
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_transfiniteCompositionOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.IsSeparator G →
    ∀ {X : C} [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {A : C} (f : A ⟶ X) [CategoryTheory.Mono f],
      ∃ J x x_1 x_2,
        ∃ (x_3 : WellFoundedLT J),
          Nonempty
            ((CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J
              f)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Numerator of an element in `HomogeneousLocalization x`.  -/
HomogeneousLocalization.num : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] → [inst_1 : SetLike σ A] → {𝒜 : ι → σ} → {x : Submonoid A} → HomogeneousLocalization 𝒜 x → A
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesColimit.toReflectsColimit : ∀ {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} [self : CategoryTheory.CreatesColimit K F], CategoryTheory.Limits.ReflectsColimit K F
-- Aesop.Tree.Data
Aesop.instInhabitedGoalId : Inhabited Aesop.GoalId
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigitsTerm.eq_1 : ∀ {b : ℕ} (digits : ℕ → Fin b) (i : ℕ), Real.ofDigitsTerm digits i = ↑↑(digits i) * (↑b ^ (i + 1))⁻¹
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.mk'.injEq : ∀ {α : Type u} {β : α → Type v} {cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap._auto_1}
  (inner inner_1 : Quotient (Std.DTreeMap.isSetoid α β cmp)),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
min_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] [AddRightMono α] (a b c : α), min a b + c = min (a + c) (b + c)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_squareRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A'']
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B''] [inst_8 : CategoryTheory.Category.{v₉, u₉} C'']
  {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''),
  (ψ.comp ψ').squareRight = ψ.squareRight.vComp' ψ'.squareRight
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {Z : Cᵒᵖ} (h : Opposite.op S.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.opcyclesOpIso.hom (CategoryTheory.CategoryStruct.comp S.toCycles.op h) =
    CategoryTheory.CategoryStruct.comp S.op.fromOpcycles h
-- Mathlib.Algebra.Quandle
Quandle.oppositeQuandle : {Q : Type u_1} → [Quandle Q] → Quandle Qᵐᵒᵖ
-- Mathlib.Algebra.Module.ZMod
AddSubgroup.coe_toZModSubmodule : ∀ (n : ℕ) {M : Type u_1} [inst : AddCommGroup M] [inst_1 : Module (ZMod n) M] (S : AddSubgroup M),
  ↑((AddSubgroup.toZModSubmodule n) S) = ↑S
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftRight_add : ∀ (m n k : ℕ), m >>> (n + k) = m >>> n >>> k
-- Mathlib.Algebra.Star.StarAlgHom
/-- By definition, a ⋆-algebra homomorphism preserves the `star` operation.  -/
StarAlgHom.map_star' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (self : A →⋆ₐ[R] B) (x : A),
  (↑↑(↑self).toRingHom).toFun (star x) = star ((↑↑(↑self).toRingHom).toFun x)
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le' : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.le_of_le_cert p₁ p₂ = true →
    ∀ (k : ℤ), Int.Internal.Linear.Poly.denote' ctx p₁ ≤ k → Int.Internal.Linear.Poly.denote' ctx p₂ ≤ k
-- Mathlib.Algebra.Group.ULift
ULift.commGroup.eq_1 : ∀ {α : Type u} [inst : CommGroup α], ULift.commGroup = Function.Injective.commGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Finsupp.Basic
Finsupp.domCongr_refl : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M], Finsupp.domCongr (Equiv.refl α) = AddEquiv.refl (α →₀ M)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_centralizer_iff : ∀ {R : Type u_1} [inst : NonUnitalRing R] {s : Set R} {z : R},
  z ∈ NonUnitalSubring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
-- Lean.Util.PPExt
Lean.instInhabitedPPFns : Inhabited Lean.PPFns
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.ord_mk_lt_type : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {s : Set α},
  s.Finite → sᶜ.Nonempty → (Cardinal.mk ↑s).ord < Ordinal.type r
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.baseChange_eq_span : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (p : Submodule R M),
  Submodule.baseChange A p = Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) p)
-- Lean.Elab.Match
Lean.Elab.Term.instInhabitedDiscr : Inhabited Lean.Elab.Term.Discr
-- Mathlib.Geometry.Manifold.HasGroupoid
Topology.IsOpenEmbedding.singletonChartedSpace_chartAt_eq : ∀ {H : Type u} [inst : TopologicalSpace H] {α : Type u_5} [inst_1 : TopologicalSpace α] [inst_2 : Nonempty α]
  {f : α → H} (h : Topology.IsOpenEmbedding f) {x : α}, ↑(chartAt H x) = f
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.mk.inj : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {inst : Monoid G} {inst_1 : Ring R}
  {inst_2 : AddCommGroup V} {inst_3 : TopologicalSpace V} {inst_4 : IsTopologicalAddGroup V} {inst_5 : Module R V}
  {inst_6 : AddCommGroup W} {inst_7 : TopologicalSpace W} {inst_8 : IsTopologicalAddGroup W} {inst_9 : Module R W}
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {toContinuousLinearMap : V →L[R] W}
  {isIntertwining' : ∀ (g : G), toContinuousLinearMap ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap}
  {toContinuousLinearMap_1 : V →L[R] W}
  {isIntertwining'_1 : ∀ (g : G), toContinuousLinearMap_1 ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap_1},
  { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' } =
      { toContinuousLinearMap := toContinuousLinearMap_1, isIntertwining' := isIntertwining'_1 } →
    toContinuousLinearMap = toContinuousLinearMap_1
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.map_ofFintype : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → ENNReal) (h : ∑ a, f a = 1)
  (g : α → β), PMF.map g (PMF.ofFintype f h) = PMF.ofFintype (fun b => ∑ a with g a = b, f a) ⋯
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.push : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} → {σ : Type u_4} → (k : K) → (σ → Γ k) → Turing.TM2.Stmt Γ Λ σ → Turing.TM2.Stmt Γ Λ σ
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_natCast_p_sub_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ‖↑(p - 1)‖ = 1
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result : Type
-- Init.Data.Vector.Attach
Vector.toList_attach : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.attach.toList = xs.toList.attachWith (fun x => x ∈ xs) ⋯
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsPrimitiveRoot.adjoin_isCyclotomicExtension : ∀ (A : Type u) {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {ζ : B} {n : ℕ} [NeZero n],
  IsPrimitiveRoot ζ n → IsCyclotomicExtension {n} A ↥A[ζ]
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.mk_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E} {r : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.ball x r) →
    ContinuousOn f (Metric.closedBall x r) → InnerProductSpace.HarmonicContOnCl f (Metric.ball x r)
-- Mathlib.Order.Grade
GradeBoundedOrder.toGradeMaxOrder : {𝕆 : Type u_5} →
  {α : Type u_6} → [inst : Preorder 𝕆] → [inst_1 : Preorder α] → [self : GradeBoundedOrder 𝕆 α] → GradeMaxOrder 𝕆 α
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GOne.mk : {ι : Type u_1} → {A : ι → Type u_2} → [inst : Zero ι] → A 0 → GradedMonoid.GOne A
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntry?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α),
  Std.DHashMap.Internal.AssocList.getEntry? a Std.DHashMap.Internal.AssocList.nil = none
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- `MonoidAlgebra.map` of a surjective function is surjective.  -/
MonoidAlgebra.map_surjective : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S),
  Function.Surjective ⇑f → Function.Surjective (MonoidAlgebra.map f)