mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ResidueField
/-- Degree of `f` at a point `x` is defined to be the degree of the associated field extension
from `κ(f x)` to `κ(x)`. We return a default value of zero when this degree is infinite.
 -/
AlgebraicGeometry.Scheme.Hom.residueDegree : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → ↥X → ℕ
-- Mathlib.Topology.Compactness.Compact
/-- If `s : Set X` belongs to `𝓝 x ⊓ l` for all `x` from a compact set `K`,
then it belongs to `(𝓝ˢ K) ⊓ l`,
i.e., there exist an open `U ⊇ K` and `T ∈ l` such that `U ∩ T ⊆ s`.  -/
IsCompact.mem_nhdsSet_inf_of_forall : ∀ {X : Type u} [inst : TopologicalSpace X] {K : Set X} {l : Filter X} {s : Set X},
  IsCompact K → (∀ x ∈ K, s ∈ nhds x ⊓ l) → s ∈ nhdsSet K ⊓ l
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : Module.Basis ι R M) (v : ι' → M) (i : ι) (j : ι'), e.toMatrix v i j = (e.repr (v j)) i
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.divConst_empty_right : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A : Finset G), A.divConst ∅ = 0
-- Lean.Meta.Tactic.Grind.Types
/-- Case-splits that have been inserted at `candidates` at some point.  -/
Lean.Meta.Grind.Split.State.added : Lean.Meta.Grind.Split.State → Std.HashSet Lean.Meta.Grind.SplitInfo
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- The coercion from `M →SL[σ] M₂` to `M →ₛₗ[σ] M₂`, as a linear map.  -/
ContinuousLinearMap.coeLMₛₗ : {R : Type u_1} →
  {R₃ : Type u_3} →
    {S₃ : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : Semiring R₃] →
          [inst_2 : Semiring S₃] →
            {M : Type u_6} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : Module R M] →
                    {M₃ : Type u_8} →
                      [inst_6 : TopologicalSpace M₃] →
                        [inst_7 : AddCommMonoid M₃] →
                          [inst_8 : Module R₃ M₃] →
                            [inst_9 : Module S₃ M₃] →
                              [inst_10 : SMulCommClass R₃ S₃ M₃] →
                                [inst_11 : ContinuousConstSMul S₃ M₃] →
                                  (σ₁₃ : R →+* R₃) → [inst_12 : ContinuousAdd M₃] → (M →SL[σ₁₃] M₃) →ₗ[S₃] M →ₛₗ[σ₁₃] M₃
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sum_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {α : Type u_3} {s : Finset α}
  {f : α → MvPolynomial σ R}, m.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun x => m.toSyn (m.degree (f x))
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [inst_5 : Finite G] [inst_6 : IsGaloisGroup G K L]
  (F : IntermediateField K L),
  Subgroup.map (↑(IsGaloisGroup.mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) = F.fixingSubgroup
-- Init.Data.String.Decode
UInt8.utf8ByteSize.congr_simp : ∀ (c c_1 : UInt8) (e_c : c = c_1) (_h : c.IsUTF8FirstByte), c.utf8ByteSize _h = c_1.utf8ByteSize ⋯
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.add_eq_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b : α}, a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Mathlib.Combinatorics.Matroid.Basic
/-- A Basis for a set `X ⊆ M.E` is a maximal independent subset of `X`
(Often in the literature, the word 'Basis' is used to refer to what we call a 'Base').  -/
Matroid.IsBasis : {α : Type u_1} → Matroid α → Set α → Set α → Prop
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.comap_jacobson_of_surjective : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ {K : Ideal S}, Ideal.comap f K.jacobson = (Ideal.comap f K).jacobson
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsCycles.reachable_deleteEdges : ∀ {V : Type u_1} {G : SimpleGraph V} {v w : V} [Finite V],
  G.Adj v w → G.IsCycles → (G.deleteEdges {s(v, w)}).Reachable v w
-- Lean.Data.RArray
Lean.RArray.size.eq_2 : ∀ {α : Type u} (p : ℕ) (l r : Lean.RArray α), (Lean.RArray.branch p l r).size = l.size + r.size
-- Init.Data.List.Lemmas
/-- Variant of `append_inj_right` instead requiring equality of the lengths of the second lists.  -/
List.append_inj_right' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → t₁ = t₂
-- Mathlib.NumberTheory.Padics.RingHoms
_private.Mathlib.NumberTheory.Padics.RingHoms.0.Int.neg.match_1.splitter : (motive : ℤ → Sort u_1) → (n : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive n
-- Init.Data.UInt.Bitwise
USize.ofFin_shiftLeft_mod : ∀ (a b : Fin USize.size),
  USize.ofFin (a <<< (b % ⟨System.Platform.numBits, USize.ofFin_shiftLeft_mod._proof_1⟩)) =
    USize.ofFin a <<< USize.ofFin b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_maxKey?_of_isSome_maxKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t.erase k).maxKey?.isSome = true → t.maxKey?.isSome = true
-- Init.PropLemmas
decide_eq_true_iff : ∀ {p : Prop} [inst : Decidable p], decide p = true ↔ p
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.extend_one : ∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : One β] {f : α → β} [T2Space α'],
  HasCompactMulSupport f → ∀ {g : α → α'}, Continuous g → HasCompactMulSupport (Function.extend g f 1)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulBackwardPatternModel.skipSuffix?_sliceTo_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {p₀ : s.Pos},
  String.Slice.Pattern.BackwardPattern.skipSuffix? pat (s.sliceTo p₀) = none ↔
    ¬String.Slice.Pattern.Model.RevMatchesAt pat p₀
-- Init.Data.Ord.Basic
compareOfLessAndEq_eq_swap : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [inst_2 : DecidableLT α] [inst_3 : DecidableEq α],
  (∀ {x y : α}, x ≤ y → y ≤ x → x = y) →
    (∀ (x y : α), x ≤ y ∨ y ≤ x) →
      (∀ {x y : α}, ¬x ≤ y ↔ y < x) → ∀ {x y : α}, compareOfLessAndEq x y = (compareOfLessAndEq y x).swap
-- Mathlib.Analysis.Convex.Exposed
/-- A set `B` is exposed with respect to `A` iff it maximizes some functional over `A` (and contains
all points maximizing it). Written `IsExposed 𝕜 A B`.  -/
IsExposed : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [TopologicalSpace 𝕜] →
      [inst : Semiring 𝕜] →
        [Preorder 𝕜] → [inst_2 : AddCommMonoid E] → [TopologicalSpace E] → [Module 𝕜 E] → Set E → Set E → Prop
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : CategoryTheory.Functor C (Type (max w v₁))}
  (τ : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F),
  CategoryTheory.uliftCoyonedaEquiv τ =
    (CategoryTheory.ConcreteCategory.hom (τ.app (Opposite.unop X)))
      { down := CategoryTheory.CategoryStruct.id (Opposite.unop X) }
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.partialMatch : ∀ {pat s : String.Slice} {needlePos stackPos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos →
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat.copy.toByteArray s.copy.toByteArray
      needlePos.byteIdx stackPos.byteIdx
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_add_of_mutuallySingular : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν₁]
  [MeasureTheory.SigmaFinite ν₂] [MeasureTheory.SigmaFinite μ],
  ν₂.MutuallySingular μ → (ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) [QuasiIso φ],
  QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ)
-- Mathlib.Analysis.Normed.Group.Basic
preimage_add_sphere : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E) (r : ℝ),
  (fun x => b + x) ⁻¹' Metric.sphere a r = Metric.sphere (a - b) r
-- Init.Data.Dyadic.Basic
Dyadic.instHShiftLeftNat : HShiftLeft Dyadic ℕ Dyadic
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derivedε.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [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.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj adj_1 : G ⊣ F),
  adj = adj_1 →
    ∀ {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
      (W₂ W₂_1 : CategoryTheory.MorphismProperty C₂) (e_W₂ : W₂ = W₂_1) [inst_4 : L₂.IsLocalization W₂]
      {G' : CategoryTheory.Functor D₁ D₂} {F' : CategoryTheory.Functor D₂ D₁} (α α_1 : L₁.comp G' ⟶ G.comp L₂),
      α = α_1 →
        ∀ (β β_1 : F.comp L₁ ⟶ L₂.comp F') (e_β : β = β_1)
          [inst_5 :
            (F'.comp G').IsRightDerivedFunctor
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G') (L₂.associator F' G').hom)
              W₂],
          adj.derivedε W₂ α β = adj_1.derivedε W₂_1 α_1 β_1
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.ofHom_apply : ∀ {R : Type u} [inst : Ring R] {M N : Type v} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N] [inst_3 : Module R M]
  [inst_4 : Module R N] (f : M →ₗ[R] N) (x : M), (CategoryTheory.ConcreteCategory.hom (ModuleCat.ofHom f)) x = f x
-- Mathlib.Algebra.Order.Archimedean.Real.Hom
ringHom_monotone : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedAddMonoid R] [inst_3 : Ring S]
  [inst_4 : LinearOrder S] [IsOrderedAddMonoid S] [PosMulMono S],
  (∀ (r : R), 0 ≤ r → IsSquare r) → ∀ (f : R →+* S), Monotone ⇑f
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.hexagon_reverse : ∀ {R : Type u} [inst : CommSemiring R] (X Y Z : SemimoduleCat R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).braiding Z).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (Y.braiding Z).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.braiding Z).hom Y))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.ExprPair.mk.injEq : ∀ {w : ℕ} (lhs rhs : Std.Tactic.BVDecide.BVExpr w) (w_1 : ℕ) (lhs_1 rhs_1 : Std.Tactic.BVDecide.BVExpr w_1),
  ({ w := w, lhs := lhs, rhs := rhs } = { w := w_1, lhs := lhs_1, rhs := rhs_1 }) =
    (w = w_1 ∧ lhs ≍ lhs_1 ∧ rhs ≍ rhs_1)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `smul_apply`. -/
MultilinearMap.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.FieldTheory.Finite.Basic
/-- A unit `a` of a finite field `F` of odd characteristic is a square
if and only if `a ^ (#F / 2) = 1`.  -/
FiniteField.unit_isSquare_iff : ∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F],
  ringChar F ≠ 2 → ∀ (a : Fˣ), IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_of_fintype : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : Decidable s.Nontrivial] [inst_2 : Fintype ↑s],
  s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (Function.uncurry dist) else 0
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- The non-unital ⋆-homomorphism/⋆-representation of `A` into the algebra of bounded operators on
a Hilbert space that is constructed from a positive linear functional `f` on a possibly non-unital
C⋆-algebra.
 -/
PositiveLinearMap.gnsNonUnitalStarAlgHom : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → [inst_2 : StarOrderedRing A] → A →⋆ₙₐ[ℂ] f.GNS →L[ℂ] f.GNS
-- Init.Meta.Defs
/-- Whenever `Int.natAbs a` is found, register the disjunction
`0 ≤ a ∧ Int.natAbs a = a ∨ a < 0 ∧ Int.natAbs a = - a` for later splitting.
 -/
Lean.Meta.Omega.OmegaConfig.splitNatAbs : Lean.Meta.Omega.OmegaConfig → Bool
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.triangleOfDegreewiseSplit_mor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting),
  (CochainComplex.triangleOfDegreewiseSplit S σ).mor₂ = S.g
-- Init.Internal.Order.Basic
Lean.Order.implication_order_monotone_and : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] (f₁ f₂ : α → Lean.Order.ImplicationOrder),
  Lean.Order.monotone f₁ → Lean.Order.monotone f₂ → Lean.Order.monotone fun x => f₁ x ∧ f₂ x
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
AlternatingMap.alternatizeUncurryFin_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} {S : Type u_6} [inst_5 : Monoid S] [inst_6 : DistribMulAction S N]
  [inst_7 : SMulCommClass R S N] (c : S) (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N),
  AlternatingMap.alternatizeUncurryFin (c • f) = c • AlternatingMap.alternatizeUncurryFin f
-- Init.Data.SInt.Lemmas
Int32.sub_zero : ∀ (a : Int32), a - 0 = a
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The elements of `A.nonunits` are those of the maximal ideal of `A` after coercion to `K`.

See also `mem_nonunits_iff_exists_mem_maximalIdeal`, which gets rid of the coercion to `K`,
at the expense of a more complicated right-hand side.
 -/
ValuationSubring.coe_mem_nonunits_iff : ∀ {K : Type u} [inst : Field K] {A : ValuationSubring K} {a : ↥A}, ↑a ∈ A.nonunits ↔ a ∈ IsLocalRing.maximalIdeal ↥A
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.equivBaseChange_apply : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V)
  (a : CliffordAlgebra (QuadraticForm.baseChange A Q)),
  (CliffordAlgebra.equivBaseChange A Q) a = (CliffordAlgebra.toBaseChange A Q) a
-- Std.Data.HashMap.Lemmas
Std.HashMap.distinct_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  List.Pairwise (fun a b => (a == b) = false) m.keys
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeriesStep.congr_simp : ∀ {G : Type u_1} [inst : AddGroup G] (N N_1 : AddSubgroup G) (e_N : N = N_1) [inst_1 : N.Normal],
  N.upperCentralSeriesStep = N_1.upperCentralSeriesStep
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousWithinAt_iff_forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} {x : α}
  [inst_1 : TopologicalSpace β],
  UpperHemicontinuousWithinAt f s x ↔ ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an
equivalence between cocones over `F` and cocones over `F ⋙ e.functor`.
 -/
CategoryTheory.Limits.Cocone.functorialityEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor J C) →
              (e : C ≌ D) → CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone (F.comp e.functor)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ ν : MeasureTheory.Measure α},
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ → Pairwise fun g₁ g₂ => MeasureTheory.AEDisjoint ν (g₁ +ᵥ s) (g₂ +ᵥ s)
-- Mathlib.Order.BoundedOrder.Basic
Subtype.mk_top : ∀ {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : OrderTop (Subtype p)]
  (htop : p ⊤), ⟨⊤, htop⟩ = ⊤
-- Mathlib.LinearAlgebra.Basis.Exact
LinearIndependent.linearIndependent_of_exact_of_retraction : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
  s ∘ₗ f = LinearMap.id →
    Function.Exact ⇑f ⇑g →
      ∀ {ι : Type u_5} {κ : Type u_6} {v : ι → M} {a : κ → ι},
        Function.Injective a → (∀ (i : κ), s (v (a i)) = 0) → LinearIndependent R v → LinearIndependent R (⇑g ∘ v ∘ a)
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- A function is called of temperate growth if it is smooth and all iterated derivatives are
polynomially bounded.  -/
Function.HasTemperateGrowth : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (E → F) → Prop
-- Init.Tactics
/-- `admit` is a synonym for `sorry`.  -/
Lean.Parser.Tactic.tacticAdmit : Lean.ParserDescr
-- Mathlib.Data.NNReal.Defs
Real.coe_toNNReal' : ∀ (r : ℝ), ↑r.toNNReal = max r 0
-- Std.Do.Triple.Basic
Std.Do.Triple.iff_conseq : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Std.Do.WP m ps] {α : Type u} {x : m α} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond α ps},
  ⦃P⦄ x ⦃Q⦄ ↔
    ∀ ⦃P' : Std.Do.SPred ps.args⦄ ⦃Q' : Std.Do.PostCond α ps⦄, (P' ⊢ₛ P) → Q.entails Q' → P' ⊢ₛ (Std.Do.wp x).apply Q'
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instSMulPosReflectLE : ∀ {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [inst : Semiring α] [inst_1 : Preorder α]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] [inst_3 : (i : ι) → Preorder (β i)] [inst_4 : (i : ι) → Module α (β i)]
  [∀ (i : ι), SMulPosReflectLE α (β i)], SMulPosReflectLE α (Π₀ (i : ι), β i)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.coe_star_mul_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(pinGroup Q)), star ↑x * ↑x = 1
-- Mathlib.Topology.Order.WithTop
TopologicalSpace.instWithTopOfOrderTopology : {ι : Type u_1} → [inst : Preorder ι] → [inst_1 : TopologicalSpace ι] → [OrderTopology ι] → TopologicalSpace (WithTop ι)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.ext : ∀ {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 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  {e e' : P₁ ≃ᴬ[k] P₂}, (∀ (x : P₁), e x = e' x) → e = e'
-- Mathlib.Topology.Sheaves.Stalks
/-- **Alias** of `TopCat.Presheaf.exists_germ_eq`.

---

For presheaves valued in a concrete category whose forgetful functor preserves filtered colimits,
every element of the stalk is the germ of a section.
 -/
TopCat.Presheaf.germ_exist : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (F : TopCat.Presheaf C X) {x : ↑X}
  (t : CategoryTheory.ToType (F.stalk x)),
  ∃ U, ∃ (m : x ∈ U), ∃ s, (CategoryTheory.ConcreteCategory.hom (F.germ U x m)) s = t
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.tensorFunc_obj_map : ∀ (C : Type u) (Z : CategoryTheory.FreeMonoidalCategory C)
  {n n' : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C} (f : n ⟶ n'),
  ((CategoryTheory.FreeMonoidalCategory.tensorFunc C).obj Z).map f =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.FreeMonoidalCategory.inclusion.map f) Z
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_le_iff_le_comap : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M}
  {N' : LieSubmodule R L M'}, LieSubmodule.map f N ≤ N' ↔ N ≤ LieSubmodule.comap f N'
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.integrable_indicator_iff : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {s : Set X},
  MeasurableSet s → (μ.Integrable (s.indicator f) ↔ μ.IntegrableOn f s)
-- Mathlib.Data.Sym.Basic
Sym.sigma_sub_ext : ∀ {α : Type u_1} {n : ℕ} {m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)}, ↑m₁.snd = ↑m₂.snd → m₁ = m₂
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.inv_val : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A : ↥(Matrix.unitaryGroup n α)), ↑A⁻¹ = star ↑A
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.zero : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}, IntervalIntegrable 0 μ a b
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_assoc_coeff₁'.eq_1 : ∀ (s t : ↑unitInterval),
  Set.Icc.convexComb_assoc_coeff₁' s t =
    unitInterval.symm (Set.Icc.convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s))
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded : ∀ {ι : Type u_1} {E : Type u_2} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [inst : NormedAddCommGroup E]
  {a b : ι → ℝ} {f : ℝ → E} {I a₀ b₀ : ℝ},
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) MeasureTheory.volume) →
    Filter.Tendsto a l (nhds a₀) →
      Filter.Tendsto b l (nhds b₀) →
        (∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Set.Ioc (a i) (b i), ‖f x‖ ≤ I) →
          MeasureTheory.IntegrableOn f (Set.Ioc a₀ b₀) MeasureTheory.volume
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_mapDomain_index : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {f : α → β} {s : α →₀ M} {h : β → M → N},
  (∀ (b : β), h b 0 = 0) →
    (∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) →
      (Finsupp.mapDomain f s).sum h = s.sum fun a m => h (f a) m