mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Slice
String.Slice.Pattern.Internal.memcmpSlice.congr_simp : ∀ (lhs lhs_1 : String.Slice) (e_lhs : lhs = lhs_1) (rhs rhs_1 : String.Slice) (e_rhs : rhs = rhs_1)
  (lstart lstart_1 : String.Pos.Raw) (e_lstart : lstart = lstart_1) (rstart rstart_1 : String.Pos.Raw)
  (e_rstart : rstart = rstart_1) (len len_1 : String.Pos.Raw) (e_len : len = len_1)
  (h1 : len.offsetBy lstart ≤ lhs.rawEndPos) (h2 : len.offsetBy rstart ≤ rhs.rawEndPos),
  String.Slice.Pattern.Internal.memcmpSlice lhs rhs lstart rstart len h1 h2 =
    String.Slice.Pattern.Internal.memcmpSlice lhs_1 rhs_1 lstart_1 rstart_1 len_1 ⋯ ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.homeomorphOfImageSubsetSource_apply_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a : ↑s),
  ↑((e.homeomorphOfImageSubsetSource hs ht) a) = ↑e ↑a
-- Mathlib.Algebra.Star.MonoidHom
/-- Construct a `StarMonoidHom` from a morphism in some type which preserves `1`, `*` and `star`.  -/
StarMonoidHom.ofClass : {F : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Monoid A] →
        [inst_1 : Star A] →
          [inst_2 : Monoid B] →
            [inst_3 : Star B] → [inst_4 : FunLike F A B] → [MonoidHomClass F A B] → [StarHomClass F A B] → F → A →⋆* B
-- Lean.AddDecl
_private.Lean.AddDecl.0.Lean.Environment.addDeclAux : Lean.Environment →
  Lean.Options →
    Lean.Declaration → optParam (Option IO.CancelToken) none → Except Lean.Kernel.Exception Lean.Environment
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instDistribMulAction : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {R : Type u_5} →
        [inst_1 : Monoid R] → [inst_2 : AddMonoid Y] → [DistribMulAction R Y] → DistribMulAction R (LocallyConstant X Y)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprConnection : Repr Std.Http.Header.Connection
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
  ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)) ⁻¹'
      ↑(PrimeSpectrum.basicOpen (HomogeneousLocalization.mk z)) =
    Subtype.val ⁻¹' ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑z.num)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.mk : ∀ {G : Type u_1} [inst : Add G],
  (∀ {A B : Finset G}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueAdd A B a0 b0) → UniqueSums G
-- Mathlib.Order.PiLex
Pi.instPartialOrderColexForallOfLinearOrder : {ι : Type u_1} →
  {β : ι → Type u_2} → [LinearOrder ι] → [(a : ι) → PartialOrder (β a)] → PartialOrder (Colex ((i : ι) → β i))
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.ext : ∀ {α α₂ β : Type w} {m : Type w → Type u_1} {x y : Std.Iterators.Types.Flatten α α₂ β m},
  x.it₁ = y.it₁ → x.it₂ = y.it₂ → x = y
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.congr_right : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β}, g =ᶠ[l] h → (f =ᶠ[l] g ↔ f =ᶠ[l] h)
-- Mathlib.Topology.Algebra.Group.Basic
/-- Eta-expanded form of `Continuous.zpow` -/
Continuous.fun_zpow : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G}, Continuous f → ∀ (z : ℤ), Continuous fun i => f i ^ z
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- Let `v` be an indexed family of `n` orthogonal vectors in an oriented `n`-dimensional
real inner product space `E`. The output of the volume form of `E` when evaluated on `v` is, up to
sign, the product of the norms of the vectors `v i`.  -/
Orientation.abs_volumeForm_apply_of_pairwise_orthogonal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) {v : Fin n → E},
  (Pairwise fun i j => inner ℝ (v i) (v j) = 0) → |o.volumeForm v| = ∏ i, ‖v i‖
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightUnitor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : C × CategoryTheory.Discrete PUnit.{w + 1}} (f : X ⟶ Y),
  (CategoryTheory.prod.rightUnitor C).map f = f.1
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongr_mul : ∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] {ι₁ : Type u_1} (σ₁ σ₂ : Equiv.Perm ι₁)
  (m : MultilinearMap R (fun x => M₂) M₃),
  MultilinearMap.domDomCongr (σ₂ * σ₁) m = MultilinearMap.domDomCongr σ₂ (MultilinearMap.domDomCongr σ₁ m)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_erase_le_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → (cmp (t.erase k).maxKey! t.maxKey!).isLE = true
-- Batteries.Data.Char.Basic
Char.instDecidableForallOfDecidablePred_batteries : (P : Char → Prop) → [DecidablePred P] → Decidable (∀ (c : Char), P c)
-- Mathlib.FieldTheory.Finite.Basic
Int.prime_dvd_pow_sub_one : ∀ {p : ℕ}, Nat.Prime p → ∀ {n : ℤ}, IsCoprime n ↑p → ↑p ∣ n ^ (p - 1) - 1
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.IsLeftAdjoint.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {left : CategoryTheory.Functor C D}, (∃ right, Nonempty (left ⊣ right)) → left.IsLeftAdjoint
-- Init.Data.Nat.MinMax
Nat.le_min : ∀ {a b c : ℕ}, a ≤ min b c ↔ a ≤ b ∧ a ≤ c
-- Mathlib.Algebra.Colimit.Module
/-- **Alias** of `DirectedSystem.map_map'`. -/
Module.DirectedSystem.map_map : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] ⦃i j k : ι⦄ (hij : i ≤ j) (hjk : j ≤ k) (x : F i),
  (f j k hjk) ((f i j hij) x) = (f i k ⋯) x
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype_injective : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p], Function.Injective ⇑Equiv.Perm.ofSubtype
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_symm_toLinearEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ⇑(↑e).symm = ⇑e.symm
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The underlying function of a `ContinuousHom` is continuous, i.e. it preserves `ωSup`  -/
OmegaCompletePartialOrder.ContinuousHom.map_ωSup' : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (self : α →𝒄 β) (c : OmegaCompletePartialOrder.Chain α),
  self.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map self.toOrderHom)
-- Mathlib.Analysis.CStarAlgebra.Fuglede
_private.Mathlib.Analysis.CStarAlgebra.Fuglede.0.expMulMulExp.eq_1 : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a b x : A) (z : ℂ),
  expMulMulExp✝ a b x z = NormedSpace.exp (z • star b) * x * NormedSpace.exp (z • star (-a))
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The support of a set of TM2 states in the TM2 emulator.  -/
Turing.TM2to1.trSupp : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} → {σ : Type u_4} → (Λ → Turing.TM2.Stmt Γ Λ σ) → Finset Λ → Finset (Turing.TM2to1.Λ' K Γ Λ σ)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.LeftUnitorBimod.hom_left_act_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  CategoryTheory.CategoryStruct.comp ((Bimod.regular R).tensorBimod P).actLeft (Bimod.LeftUnitorBimod.hom P) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.LeftUnitorBimod.hom P)) P.actLeft
-- Mathlib.Control.Traversable.Equiv
Equiv.traverse_eq_map_id : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t] {α β : Type u}
  (f : α → β) (x : t' α), Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.hasForgetToSemigroup : CategoryTheory.HasForget₂ MonCat Semigrp
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_mono : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ : Subgroup G} (H₃ : Subgroup G), H₁ ≤ H₂ → H₁.subgroupOf H₃ ≤ H₂.subgroupOf H₃
-- Init.Core
instDecidableEqSigma : {α : Type u} → {β : α → Type v} → [h₁ : DecidableEq α] → [h₂ : (a : α) → DecidableEq (β a)] → DecidableEq (Sigma β)
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- The standard basis for a monoid algebra.  -/
MonoidAlgebra.basis : (R : Type u_7) → (k : Type u_8) → [inst : Semiring k] → Module.Basis R k (MonoidAlgebra k R)
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.map₂_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (a : CategoryTheory.ThinSkeleton C),
  (CategoryTheory.ThinSkeleton.map₂ F).obj a = CategoryTheory.ThinSkeleton.map₂Functor F a
-- Mathlib.Algebra.Star.StarProjection
isStarProjection_iff : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] (p : R), IsStarProjection p ↔ IsIdempotentElem p ∧ IsSelfAdjoint p
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.prevAux.go.match_1.eq_2 : ∀ {s : String.Slice}
  (motive :
    (off : ℕ) →
      (h₁ : off < s.utf8ByteSize) → ¬(s.getUTF8Byte { byteIdx := off } h₁).IsUTF8FirstByte → 0 ≠ off → Sort u_1)
  (off : ℕ) (h₁ : off + 1 < s.utf8ByteSize) (hbyte : ¬(s.getUTF8Byte { byteIdx := off + 1 } h₁).IsUTF8FirstByte)
  (this : 0 ≠ off + 1)
  (h_1 :
    (h₁ : 0 < s.utf8ByteSize) →
      (hbyte : ¬(s.getUTF8Byte { } h₁).IsUTF8FirstByte) → (this : 0 ≠ 0) → motive 0 h₁ hbyte this)
  (h_2 :
    (off : ℕ) →
      (h₁ : off + 1 < s.utf8ByteSize) →
        (hbyte : ¬(s.getUTF8Byte { byteIdx := off + 1 } h₁).IsUTF8FirstByte) →
          (this : 0 ≠ off + 1) → motive off.succ h₁ hbyte this),
  (match off.succ, h₁, hbyte, this with
    | 0, h₁, hbyte, this => h_1 h₁ hbyte this
    | off.succ, h₁, hbyte, this => h_2 off h₁ hbyte this) =
    h_2 off h₁ hbyte this
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSliceData.range : {α : Type u} → {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RccSliceData α β → Std.Rcc α
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.mk.injEq : ∀ (inner inner_1 : Int16), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Init.System.IO
IO.FS.Mode.noConfusionType : Sort v✝ → IO.FS.Mode → IO.FS.Mode → Sort v✝
-- Mathlib.Data.Nat.Factorial.NatCast
IsUnit.natCast_factorial_of_isNilpotent : ∀ {A : Type u_1} [inst : CommRing A] {n p : ℕ}, IsNilpotent ↑p → ∀ [Fact (Nat.Prime p)], n < p → IsUnit ↑n.factorial
-- Mathlib.Algebra.Ring.Ext
_private.Mathlib.Algebra.Ring.Ext.0.«termLocal_hMul[_,_]» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- When `h : F.IsEventuallyConstantFrom i₀`, the colimit of `F` exists and is `F.obj i₀`.  -/
CategoryTheory.Functor.IsEventuallyConstantFrom.isColimitCocone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} →
            (h : F.IsEventuallyConstantFrom i₀) →
              [inst_2 : CategoryTheory.IsFiltered J] → CategoryTheory.Limits.IsColimit h.cocone
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Prop-valued mixin for a monoid with zero to be equipped with a cancelling division.

The obvious use case is groups with zero, but this condition is also satisfied by `ℕ`, `ℤ` and, more
generally, any Euclidean domain.  -/
MulDivCancelClass : (M₀ : Type u_2) → [MonoidWithZero M₀] → [Div M₀] → Prop
-- Mathlib.Data.Sym.Sym2
Sym2.IsDiag.decidablePred : (α : Type u) → [DecidableEq α] → DecidablePred Sym2.IsDiag
-- Mathlib.Tactic.FunProp.Mor
/-- bundled morphism  -/
Mathlib.Meta.FunProp.Mor.App.fn : Mathlib.Meta.FunProp.Mor.App → Lean.Expr
-- Mathlib.RepresentationTheory.Rep.Res
Rep.resMap_hom_toLinearMap : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G)
  {M N : Rep.{u_1, u, v1} k G} (p : M ⟶ N), (Rep.Hom.hom (Rep.resMap f p)).toLinearMap = (Rep.Hom.hom p).toLinearMap
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ L₁ : CochainComplex C₁ ℤ} (f₁ : K₁ ⟶ L₁) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F]
  [inst_9 : L₁.HasMapBifunctor K₂ F] {Z : HomologicalComplex D (ComplexShape.up ℤ)}
  (h : (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).obj (L₁.mapBifunctor K₂ F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.mapBifunctorMap
        ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).map f₁)
        (CategoryTheory.CategoryStruct.id K₂) F (ComplexShape.up ℤ))
      (CategoryTheory.CategoryStruct.comp (L₁.mapBifunctorShift₁Iso K₂ F x).hom h) =
    CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₁Iso K₂ F x).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).map
          (HomologicalComplex.mapBifunctorMap f₁ (CategoryTheory.CategoryStruct.id K₂) F (ComplexShape.up ℤ)))
        h)
-- Mathlib.Topology.Order
/-- This lemma characterizes discrete topological spaces as those whose singletons are
neighbourhoods.  -/
discreteTopology_iff_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α], DiscreteTopology α ↔ ∀ (x : α), nhds x = pure x
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.mk_smul_top_ofAlgEquiv_symm : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) [inst_1 : IsAdicComplete I S] (n : ℕ) (x : AdicCompletion I S),
  (Ideal.Quotient.mk (I ^ n • ⊤)) ((AdicCompletion.ofAlgEquiv I).symm x) = (AdicCompletion.eval I S n) x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).getKey? k = if k ∈ m₂ then none else m₁.getKey? k
-- Lean.Server.References
/-- Definition and usages of an identifier within a single module.  -/
Lean.Server.RefInfo : Type
-- Mathlib.GroupTheory.Rank
Group.rank_pos : ∀ (G : Type u_1) [inst : Group G] [Nontrivial G] [inst_2 : Group.FG G], 0 < Group.rank G
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.associator_def : ∀ (R : Type u) [inst : CommRing R] (X Y Z : BialgCat R),
  CategoryTheory.MonoidalCategoryStruct.associator X Y Z =
    (Bialgebra.TensorProduct.assoc R R X.carrier Y.carrier Z.carrier).toBialgIso
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso_hom_snd : ∀ {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} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom =
        CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w).hom.snd = eᵣ.hom
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_le_iff : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b c : G},
  |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instIsIsoFunctorCounitRestrictAdjunction : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Modules.restrictAdjunction f).counit
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieAlgebra.toModule : {R : Type u_1} →
  {inst : CommRing R} → {L : Type u_2} → {inst_1 : LeftPreLieRing L} → [self : LeftPreLieAlgebra R L] → Module R L
-- Mathlib.CategoryTheory.Subobject.Basic
/-- `exists f : Subobject X ⥤ Subobject Y` is
left adjoint to `pullback f : Subobject Y ⥤ Subobject X`.
 -/
CategoryTheory.Subobject.existsPullbackAdj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasImages C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
            CategoryTheory.Subobject.exists f ⊣ CategoryTheory.Subobject.pullback f
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_clear : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.clear p k q) =
    Turing.PartrecToTM2.pop' k
      (Turing.TM2.Stmt.branch (fun s => s.elim true p) (Turing.TM2.Stmt.goto fun x => q)
        (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.Λ'.clear p k q))
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coeFn_inj : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂}, ⇑e = ⇑e' ↔ e = e'
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- A face is a subset of another one iff its vertices are.  -/
Geometry.SimplicialComplex.face_subset_face_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s t : Finset E},
  s ∈ K.faces → t ∈ K.faces → ((convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t ↔ s ⊆ t)
-- Init.Data.BitVec.Bitblast
BitVec.mulRec_zero_eq : ∀ {w : ℕ} (x y : BitVec w), x.mulRec y 0 = if y.getLsbD 0 = true then x else 0
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.instReprSplitStatus.repr : Lean.Meta.Grind.SplitStatus → ℕ → Std.Format
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciSup_of_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {a : α} {f : ι → α},
  BddAbove (Set.range f) → ∀ (c : ι), a ≤ f c → a ≤ iSup f
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationData.mk.inj : ∀ {name : Lean.Name} {userName : String} {html : ProofWidgets.Html} {name_1 : Lean.Name} {userName_1 : String}
  {html_1 : ProofWidgets.Html},
  { name := name, userName := userName, html := html } = { name := name_1, userName := userName_1, html := html_1 } →
    name = name_1 ∧ userName = userName_1 ∧ html = html_1
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_left_inj : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {s t : σ →₀ ℕ} {r : R},
  r ≠ 0 → ((MvPolynomial.monomial s) r = (MvPolynomial.monomial t) r ↔ s = t)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.subtractionCommMonoid : {α : Type u} →
  [inst : AddCommGroup α] →
    [inst_1 : PartialOrder α] → [IsOrderedAddMonoid α] → SubtractionCommMonoid (NonemptyInterval α)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- **Alias** of `Irreducible.maximalIdeal_eq_setOfPred_le_v_coe`. -/
Irreducible.maximalIdeal_eq_setOf_le_v_coe : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)
  [inst_2 : IsDiscreteValuationRing ↥v.integer] {ϖ : ↥v.integer},
  Irreducible ϖ → ↑(IsLocalRing.maximalIdeal ↥v.integer) = {y | v ↑y ≤ v ↑ϖ}
-- Init.WFComputable
_private.Init.WFComputable.0.Acc.recC.eq_1 : ∀ {α : Sort u_1} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort v}
  (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (hr : r y x) → motive y ⋯) → motive x ⋯) {a : α}
  (t : Acc r a), Acc.recC intro t = intro a ⋯ fun x hr => Acc.recC intro ⋯
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.mono : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop}
  [inst_1 : OrderBot ι] [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E],
  (∀ (X : ι → Ω → E), p X → q X) → ProbabilityTheory.Locally p 𝓕 X P → ProbabilityTheory.Locally q 𝓕 X P
-- Mathlib.Order.SupClosed
/-- A join-semilattice where every sup-closed set has a least upper bound is automatically complete.
 -/
SemilatticeSup.toCompleteSemilatticeSup : {α : Type u_3} →
  [inst : SemilatticeSup α] →
    (sSup : Set α → α) → (∀ (s : Set α), SupClosed s → IsLUB s (sSup s)) → CompleteSemilatticeSup α
-- Lean.Meta.Tactic.Grind.Theorems
/-- A local hypothesis.  -/
Lean.Meta.Grind.Origin.fvar : Lean.FVarId → Lean.Meta.Grind.Origin
-- Mathlib.Analysis.Convex.Side
Function.Injective.wSameSide_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [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] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'},
  Function.Injective ⇑f → ((AffineSubspace.map f s).WSameSide (f x) (f y) ↔ s.WSameSide x y)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instAddAction.eq_1 : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : AddMonoid K] [inst_1 : AddAction K V],
  WithLp.instAddAction p K V = { toVAdd := WithLp.instVAdd p K V, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialObject.II
/-- Auxiliary definition for `map'`. Given `f : Fin (n + 1) →o Fin (m + 1)` and
`x : Fin (m + 2)`, `map' f x` shall be the smallest element in
this `finset f x : Finset (Fin (n + 2))`.  -/
SimplexCategory.II.finset : {n m : ℕ} → (Fin (n + 1) →o Fin (m + 1)) → Fin (m + 2) → Finset (Fin (n + 2))
-- Mathlib.GroupTheory.Transfer
MonoidHom.not_dvd_card_ker_transferSylow : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P)
  [Fact (Nat.Prime p)] [Finite (Sylow p G)] [inst_3 : (↑P).FiniteIndex],
  ¬p ∣ Nat.card ↥(MonoidHom.transferSylow P hP).ker
-- Mathlib.Order.RelSeries
RelSeries.cons.congr_simp : ∀ {α : Type u_1} {r : SetRel α α} (p p_1 : RelSeries r) (e_p : p = p_1) (newHead newHead_1 : α)
  (e_newHead : newHead = newHead_1) (rel : (newHead, p.head) ∈ r), p.cons newHead rel = p_1.cons newHead_1 ⋯