mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.ext_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : CocompactMap α β},
  f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.mk_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g),
  (CategoryTheory.Limits.PullbackCone.mk fst snd eq).fst = fst
-- Mathlib.Tactic.FunProp.Types
/-- It is a constant defined in the environment.  -/
Mathlib.Meta.FunProp.Origin.decl : Lean.Name → Mathlib.Meta.FunProp.Origin
-- Mathlib.FieldTheory.NormalizedTrace
_private.Mathlib.FieldTheory.NormalizedTrace.0.Algebra.normalizedTraceAux_eq_of_finiteDimensional : ∀ (F : Type u_1) {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [CharZero F]
  [FiniteDimensional F K] (a : K), Algebra.normalizedTraceAux✝ F K a = (↑(Module.finrank F K))⁻¹ • (Algebra.trace F K) a
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionContext.mk.sizeOf_spec : ∀ (diagnostics : Array Lean.Lsp.Diagnostic) (only? : Option (Array Lean.Lsp.CodeActionKind))
  (triggerKind? : Option Lean.Lsp.CodeActionTriggerKind),
  sizeOf { diagnostics := diagnostics, only? := only?, triggerKind? := triggerKind? } =
    1 + sizeOf diagnostics + sizeOf only? + sizeOf triggerKind?
-- Init.System.IO
/-- Returns the operating system process id of the child process.  -/
IO.Process.Child.pid : {cfg : IO.Process.StdioConfig} → IO.Process.Child cfg → UInt32
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.surjectiveOnStalks_of_isLocalization : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S], (algebraMap R S).SurjectiveOnStalks
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mkIso'_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsMonHom e.hom], (CategoryTheory.Mon.mkIso' e).hom.hom = e.hom
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.rightCompReflexion_eq : CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion =
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.right
    CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion
-- Init.Data.UInt.Lemmas
UInt64.ofInt_mul : ∀ (x y : ℤ), UInt64.ofInt (x * y) = UInt64.ofInt x * UInt64.ofInt y
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_surjective_eq_zero_iff_lift : ∀ {α : Type u} {β' : Type v},
  Cardinal.mk ↑{f | Function.Surjective f} = 0 ↔
    Cardinal.lift.{v, u} (Cardinal.mk α) < Cardinal.lift.{u, v} (Cardinal.mk β') ∨
      Cardinal.mk α ≠ 0 ∧ Cardinal.mk β' = 0
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.coeff_single_zero_smul : ∀ {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ'] [inst_1 : AddCommMonoid V] {Γ : Type u_6}
  [inst_2 : AddCommMonoid Γ] [inst_3 : PartialOrder Γ] [inst_4 : AddAction Γ Γ'] [inst_5 : IsOrderedCancelVAdd Γ Γ']
  [inst_6 : MulZeroClass R] [inst_7 : SMulWithZero R V] {r : R} {x : HahnModule Γ' R V} {a : Γ'},
  ((HahnModule.of R).symm ((HahnSeries.single 0) r • x)).coeff a = r • ((HahnModule.of R).symm x).coeff a
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_containsKey_of_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getValueCast? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
        Std.Internal.List.getValueCast? k l₁
-- Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure
_private.Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure.0.MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply_eq_enorm : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.SignedMeasure X) {i j : Set X} (him : MeasurableSet i)
  (hi : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict μ i),
  MeasurableSet j → (μ.toMeasureOfZeroLE i him hi) j = ‖μ (i ∩ j)‖ₑ
-- Init.Data.SInt.Lemmas
Int8.toISize_ofInt : ∀ {n : ℤ}, Int8.minValue.toInt ≤ n → n ≤ Int8.maxValue.toInt → (Int8.ofInt n).toISize = ISize.ofInt n
-- Mathlib.LinearAlgebra.CrossProduct
cross_cross : ∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
  (crossProduct ((crossProduct u) v)) w = (crossProduct u) ((crossProduct v) w) - (crossProduct v) ((crossProduct u) w)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_32 : HSub Std.Time.Day.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.normal : {K : Type u_1} → {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Λ → Turing.TM2to1.Λ' K Γ Λ σ
-- Init.Omega.Logic
Lean.Omega.Decidable.or_not_not_of_not_and : ∀ {p q : Prop} [Decidable p] [Decidable q], ¬(p ∧ q) → ¬p ∨ ¬q
-- Mathlib.Data.Matrix.Basic
Matrix.transposeRingEquiv_apply : ∀ (m : Type u_2) (α : Type u_11) [inst : AddCommMonoid α] [inst_1 : CommMagma α] [inst_2 : Fintype m]
  (a : Matrix m m α), (Matrix.transposeRingEquiv m α) a = MulOpposite.op a.transpose
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow.
 -/
Std.Time.PlainDateTime.subNanoseconds : Std.Time.PlainDateTime → Std.Time.Nanosecond.Offset → Std.Time.PlainDateTime
-- Init.Data.SInt.Lemmas
Int32.toInt64_lt : ∀ {a b : Int32}, a.toInt64 < b.toInt64 ↔ a < b
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.ParseResult.success.inj : ∀ {α ι : Type} {pos : ι} {res : α} {pos_1 : ι} {res_1 : α},
  Std.Internal.Parsec.ParseResult.success pos res = Std.Internal.Parsec.ParseResult.success pos_1 res_1 →
    pos = pos_1 ∧ res = res_1
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_toUInt32 : ∀ (n : UInt64), n.toUInt32.toUInt16 = n.toUInt16
-- Lean.LocalContext
/-- The pretty-printable name of the variable.  -/
Lean.LocalDecl.userName : Lean.LocalDecl → Lean.Name
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∏ j ∈ s, f j) (f i) μ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] {X' Y' : C} (g : X' ⟶ Y')
  [inst_8 : CategoryTheory.Limits.HasCokernel g] [inst_9 : CategoryTheory.Limits.HasCokernel (G.map g)]
  [inst_10 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair g 0) G] (p : X ⟶ X')
  (q : Y ⟶ Y') (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G f).hom
      (CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq))
      (CategoryTheory.Limits.PreservesCokernel.iso G g).hom
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- The "set-theoretic-way" of constructing a two-sided ideal by providing:
- the underlying set `S`;
- a proof that `0 ∈ S`;
- a proof that `x + y ∈ S` if `x ∈ S` and `y ∈ S`;
- a proof that `-x ∈ S` if `x ∈ S`;
- a proof that `x * y ∈ S` if `y ∈ S`;
- a proof that `x * y ∈ S` if `x ∈ S`.
 -/
TwoSidedIdeal.mk' : {R : Type u_1} →
  [inst : NonUnitalNonAssocRing R] →
    (carrier : Set R) →
      0 ∈ carrier →
        (∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier) →
          (∀ {x : R}, x ∈ carrier → -x ∈ carrier) →
            (∀ {x y : R}, y ∈ carrier → x * y ∈ carrier) →
              (∀ {x y : R}, x ∈ carrier → x * y ∈ carrier) → TwoSidedIdeal R
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.Waiter.mk.inj : ∀ {α : Type} {finished : IO.Ref Bool} {promise : IO.Promise (Except IO.Error α)} {finished_1 : IO.Ref Bool}
  {promise_1 : IO.Promise (Except IO.Error α)},
  { finished := finished, promise := promise } = { finished := finished_1, promise := promise_1 } →
    finished = finished_1 ∧ promise = promise_1
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.centralizer.eq_1 : ∀ {M : Type u_1} (S : Set M) [inst : Monoid M],
  Submonoid.centralizer S = { carrier := S.centralizer, mul_mem' := ⋯, one_mem' := ⋯ }
-- Lean.Parser.Extension
Lean.Parser.getParserPriority : Lean.Syntax → Except String ℕ
-- Mathlib.Order.WithBot
WithTop.lt_iff_exists_coe_btwn' : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a b : WithTop α}, b < a ↔ ∃ x, ↑x < a ∧ b < ↑x
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.Functor.CommShift₂.precomp₁ : {C₁ : Type u_1} →
  {C₁' : Type u_2} →
    {C₂ : Type u_3} →
      {D : Type u_5} →
        [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} C₂] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D] →
                {M : Type u_6} →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : CategoryTheory.HasShift C₁ M] →
                      [inst_6 : CategoryTheory.HasShift C₁' M] →
                        [inst_7 : CategoryTheory.HasShift C₂ M] →
                          [inst_8 : CategoryTheory.HasShift D M] →
                            (F : CategoryTheory.Functor C₁' C₁) →
                              [F.CommShift M] →
                                (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  (h : CategoryTheory.CommShift₂Setup D M) → [G.CommShift₂ h] → (F.comp G).CommShift₂ h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constEntryAtIdx!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {i : ℕ},
  t₁.Equiv t₂ → Std.DTreeMap.Const.entryAtIdx! t₁ i = Std.DTreeMap.Const.entryAtIdx! t₂ i
-- Init.Data.Int.Order
Int.nonpos_of_neg_nonneg : ∀ {a : ℤ}, 0 ≤ -a → a ≤ 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.isoFromComma_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i : X.toComma ≅ Y.toComma),
  (CategoryTheory.MorphismProperty.Comma.isoFromComma i).hom =
    CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i.hom
-- Mathlib.Analysis.Calculus.Deriv.Pow
deriv_pow_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (n : ℕ), deriv (fun x => x ^ n) x = ↑n * x ^ (n - 1)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_comap : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) (f : G' →* G) (K : Subgroup G'),
  (Subgroup.comap f H).relIndex K = H.relIndex (Subgroup.map f K)
-- Mathlib.CategoryTheory.Presentable.Dense
CategoryTheory.IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalAccessibleCategory C κ] (X : C),
  CategoryTheory.IsCardinalFiltered (CategoryTheory.CostructuredArrow (CategoryTheory.isCardinalPresentable C κ).ι X) κ
-- Mathlib.Order.CompleteLattice.Basic
iInf_eq_top : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {s : ι → α}, iInf s = ⊤ ↔ ∀ (i : ι), s i = ⊤
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.mapAlgEquiv`.

---

The algebra isomorphism of monoid algebras induced by an isomorphism of the base algebras.  -/
MonoidAlgebra.mapRangeAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    {B : Type u_5} →
      (M : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] → [inst_5 : Monoid M] → (A ≃ₐ[R] B) → MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra B M
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.coeff_truncateFun : ∀ {p n : ℕ} {R : Type u_1} (x : WittVector p R) (i : Fin n),
  TruncatedWittVector.coeff i (WittVector.truncateFun n x) = x.coeff ↑i
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedHurwitzZetaEven₀.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.completedHurwitzZetaEven₀ a s = (HurwitzZeta.hurwitzEvenFEPair a).Λ₀ (s / 2) / 2
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.apply_lineMap : ∀ {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 : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k),
  e ((AffineMap.lineMap a b) c) = (AffineMap.lineMap (e a) (e b)) c
-- Mathlib.Data.List.AList
AList.insert_empty : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a), AList.insert a b ∅ = AList.singleton a b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α},
  k ∉ t → l.contains k = false → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKey? k = none
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.State.mk.sizeOf_spec : ∀ (cache : Std.HashSet (Option Lean.Expr × Lean.Expr × Bool)) (progress : Mathlib.Tactic.GRewrite.Progress✝),
  sizeOf { cache := cache, progress := progress } = 1 + sizeOf cache + sizeOf progress
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey?_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k' (Std.Internal.List.Const.alterKey k f l) =
      if (k == k') = true then if (f (Std.Internal.List.getValue? k l)).isSome = true then some k else none
      else Std.Internal.List.getKey? k' l
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prod.eq_1 : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂),
  LieAlgebra.Basis.prod✝ eι b₁ b₂ =
    LieSubalgebra.lieSpan R (L₁ × L₂)
      ({x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪
        {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x})
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.rayleigh_smul : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (x : E) {c : 𝕜}, c ≠ 0 → T.rayleighQuotient (c • x) = T.rayleighQuotient x
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr : ∀ {X Y : AlgebraicGeometry.Scheme} {f g : X ⟶ Y} (e : f = g) (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.residueFieldMap f x =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom
      (AlgebraicGeometry.Scheme.Hom.residueFieldMap g x)
-- Init.Data.Array.Lex.Lemmas
Array.lt_asymm : ∀ {α : Type u_1} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] {xs ys : Array α}, xs < ys → ¬ys < xs
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instNonUnitalNonAssocRing : {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalNonAssocRing β] → NonUnitalNonAssocRing (α →₀ β)
-- Init.Data.Array.Lemmas
Array.foldl_flip_append_eq_append : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {ys : Array β},
  Array.foldl (fun acc y => f y ++ acc) ys xs = (Array.map f xs).reverse.flatten ++ ys
-- Mathlib.Algebra.Ring.Shrink
Shrink.instSemiring : {α : Type u_1} → [inst : Small.{v, u_1} α] → [Semiring α] → Semiring (Shrink.{v, u_1} α)
-- Mathlib.Order.Heyting.Hom
instCoeTCBiheytingHomOfBiheytingHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : BiheytingAlgebra α] →
          [inst_2 : BiheytingAlgebra β] → [BiheytingHomClass F α β] → CoeTC F (BiheytingHom α β)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Size.  -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.Literal.n : BitVec.Literal✝ → ℕ
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.mk_apply_coe : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : AdicCompletion.AdicCauchySequence I M) (n : ℕ), ↑((AdicCompletion.mk I M) f) n = (I ^ n • ⊤).mkQ (↑f n)
-- Mathlib.CategoryTheory.Sites.InducedTopology
CategoryTheory.Functor.instIsContinuousInducedTopology : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D}, F.IsContinuous (F.inducedTopology K) K
-- Init.Data.SInt.Basic
instInhabitedInt64 : Inhabited Int64
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.LaxTrans F G) {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g))
              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).inv))))
-- Std.Http.Data.Status
Std.Http.Status.notImplemented.sizeOf_spec : sizeOf Std.Http.Status.notImplemented = 1
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` is absolutely continuous on `uIcc a b`, then `f` is uniformly continuous on `uIcc a b`.
 -/
AbsolutelyContinuousOnInterval.uniformContinuousOn : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F},
  AbsolutelyContinuousOnInterval f a b → UniformContinuousOn f (Set.uIcc a b)
-- Mathlib.Data.Countable.Basic
Function.Embedding.uncountable : ∀ {α : Sort u} {β : Sort v} [Uncountable α] (f : α ↪ β), Uncountable β
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.eq_2 : ∀ {β : Type u_3} {γ : Type u_1} {init : γ} (PlausibleForInStep : β → γ → ForInStep γ → Prop) (out : β)
  (motive : Subtype (PlausibleForInStep out init) → Sort u_2) (c : γ)
  (property : PlausibleForInStep out init (ForInStep.done c))
  (h_1 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩)
  (h_2 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩),
  (match ⟨ForInStep.done c, property⟩ with
    | ⟨ForInStep.yield c, property⟩ => h_1 c property
    | ⟨ForInStep.done c, property⟩ => h_2 c property) =
    h_2 c property
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.basisKaehlerOfIsCompl.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) {κ : Type u_5} {f : κ → ι}
  (hf : Function.Injective f) (hcompl : IsCompl (Set.range f) (Set.range P.map)),
  P.basisKaehlerOfIsCompl hf hcompl = Module.Basis.ofSplitExact ⋯ ⋯ ⋯ P.cotangentSpaceBasis hf ⋯ ⋯ ⋯
-- Mathlib.Topology.Maps.Strict.Group
ContinuousMulEquiv.quotientKerEquivRange.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {f : G →* H} [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H] (hf : Topology.IsStrictMap ⇑f),
  ContinuousMulEquiv.quotientKerEquivRange hf =
    { toMulEquiv := QuotientGroup.quotientKerEquivRange f, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.self_mem_periodicOrbit : ∀ {α : Type u_1} {f : α → α} {x : α}, x ∈ Function.periodicPts f → x ∈ Function.periodicOrbit f x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `StructuredArrow d T ⥤ StructuredArrow e (T ⋙ S)` that `u : e ⟶ S.obj d`
induces via `StructuredArrow.map₂` can be expressed up to isomorphism by
`StructuredArrow.preEquivalence` and `StructuredArrow.proj`.  -/
CategoryTheory.StructuredArrow.map₂IsoPreEquivalenceInverseCompProj : {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] →
            {T : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Functor D E} →
                {T' : CategoryTheory.Functor C E} →
                  (d : D) →
                    (e : E) →
                      (u : e ⟶ S.obj d) →
                        (α : T.comp S ⟶ T') →
                          CategoryTheory.StructuredArrow.map₂ u α ≅
                            (CategoryTheory.StructuredArrow.preEquivalence T
                                    (CategoryTheory.StructuredArrow.mk u)).inverse.comp
                              ((CategoryTheory.StructuredArrow.proj (CategoryTheory.StructuredArrow.mk u)
                                    (CategoryTheory.StructuredArrow.pre e T S)).comp
                                (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id e) α))
-- Aesop.Script.UScriptToSScript
Aesop.Script.sortDedupArrays : {α : Type u_1} → [Ord α] → Array (Array α) → Array α
-- Mathlib.Data.Finite.Defs
Finite.of_equiv : ∀ {β : Sort u_2} (α : Sort u_3) [h : Finite α] (f : α ≃ β), Finite β