mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
/-- Standard Gaussian distribution on a finite-dimensional real inner product space `E`.
This is the random vector whose coordinates in an orthonormal basis are independent standard
Gaussian.

The definition uses `stdOrthonormalBasis ℝ E` but does not actually depend on the
basis, see `stdGaussian_eq_map_pi_orthonormalBasis`.  -/
ProbabilityTheory.stdGaussian : (E : Type u_2) →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → [FiniteDimensional ℝ E] → [inst : MeasurableSpace E] → MeasureTheory.Measure E
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_all_iff_nat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, (∀ (n : ℕ∞), ContDiffOn 𝕜 (↑n) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.basicOpen_eq_of_affine' : ∀ {R : CommRingCat} (f : ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤))),
  (AlgebraicGeometry.Spec R).basicOpen f =
    PrimeSpectrum.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso R).hom) f)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_mem_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∈ t.toArray → k ∈ t
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Flattening nested `iConvexComb`s.

See `iConvexComb_assoc'` and `iConvexComb_assoc` for non-dependent versions.  -/
Convexity.iConvexComb_assoc'' : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {J : I → Type u_9}
  (s : Convexity.StdSimplex R I) (f : (i : I) → Convexity.StdSimplex R (J i)) (g : (i : I) → J i → M),
  (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) (g i)) =
    Convexity.iConvexComb (Convexity.iConvexComb s fun i => Convexity.StdSimplex.map (fun x => ⟨i, x⟩) (f i))
      (Sigma.uncurry g)
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.mem_inv_pointwise_smul_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ (S : Subsemiring R) (x : R), x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.FieldTheory.RatFunc.Valuation
/-- The valuation at infinity is the nonarchimedean valuation on `F(t)` with uniformizer `1/t`.
Explicitly, if `f/g ∈ F(t)` is a nonzero quotient of polynomials, its valuation at infinity is
`exp (degree(f) - degree(g))`.  -/
RatFunc.inftyValuationDef : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → RatFunc F → WithZero (Multiplicative ℤ)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if the root of `e`s equivalence class is already attached to a term
of the given solver.
 -/
Lean.Meta.Grind.SolverExtension.hasTermAtRoot : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Init.Control.Lawful.Instances
StateT.seqRight_eq : ∀ {m : Type u_1 → Type u_2} {σ α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β),
  x *> y = Function.const α id <$> x <*> y
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.Qh_obj_singleFunctors_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ) (X : C),
  DerivedCategory.Qh.obj (((HomotopyCategory.singleFunctors C).functor n).obj X) =
    (DerivedCategory.singleFunctor C n).obj X
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lcongr.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ : R →+* R₂}
  {σ_inv : R₂ →+* R} [inst_6 : RingHomInvPair σ σ_inv] [inst_7 : RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10}
  (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N), Finsupp.lcongr e₁ e₂ = (Finsupp.domLCongr e₁).trans (Finsupp.mapRange.linearEquiv e₂)
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_inv_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)),
  ((CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C).inv.app P).f.f = P.p.f
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.pow : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {x : R}, IsSelfAdjoint x → ∀ (n : ℕ), IsSelfAdjoint (x ^ n)
-- Mathlib.Logic.Function.Defs
/-- Every point is a fixed point of `id`.  -/
Function.isFixedPt_id : ∀ {α : Type u₁} (x : α), Function.IsFixedPt id x
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ]
  (r : NNReal), (r • μ).toSignedMeasure = r • μ.toSignedMeasure
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by zero is the identity functor.  -/
CategoryTheory.shiftFunctorZero : (C : Type u) →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] → CategoryTheory.shiftFunctor C 0 ≅ CategoryTheory.Functor.id C
-- Init.Prelude
/-- Throws an exception, with the exception type specified explicitly. This is useful when a monad
supports throwing more than one type of exception.

Use `throw` for a version that expects the exception type to be inferred from `m`.
 -/
throwThe : (ε : Type u) → {m : Type v → Type w} → [MonadExceptOf ε m] → {α : Type v} → ε → m α
-- Mathlib.Data.Fintype.Option
/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`.  -/
Finite.induction_empty_option : ∀ {P : Type u → Prop},
  (∀ {α β : Type u} (a : α ≃ β), P α → P β) →
    P PEmpty.{u + 1} → (∀ {α : Type u} [Fintype α], P α → P (Option α)) → ∀ (α : Type u) [Finite α], P α
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.idealOfSet_ofIdeal_eq_closure : ∀ {X : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [inst_2 : CompactSpace X]
  [inst_3 : T2Space X] (I : Ideal C(X, 𝕜)), ContinuousMap.idealOfSet 𝕜 (ContinuousMap.setOfIdeal I) = I.closure
-- Lean.Language.Basic
/-- Applies the transformation to the given info tree; `none` if the tree is unchanged.  -/
Lean.Language.SnapshotTreeTransform.transformInfoTree? : Lean.Language.SnapshotTreeTransform → Lean.Elab.InfoTree → Option Lean.Elab.InfoTree
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instNeg.eq_1 : ∀ {α : Type u}, FreeAddGroup.instNeg = { neg := Quot.map FreeAddGroup.negRev ⋯ }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_snd' : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ⇑(ContinuousLinearMap.snd R M₁ M₂) = Prod.snd
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Matrix.discr_conj' : ∀ {R : Type u_1} {n : Type u_2} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (g : GL n R)
  (m : Matrix n n R), ((↑g)⁻¹ * m * ↑g).discr = m.discr
-- Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
/-- For any `c : List ℕ` whose sum is at most `Fintype.card α`,
we can find `o : List (List α)` whose members have no duplicate,
whose lengths given by `c`, and which are pairwise disjoint  -/
List.exists_pw_disjoint_with_card : ∀ {α : Type u_2} [inst : Fintype α] {c : List ℕ},
  c.sum ≤ Fintype.card α → ∃ o, List.map List.length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ List.Pairwise List.Disjoint o
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_left : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u') [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y : CategoryTheory.Functor C D} (η : X ⟶ Y) (A : CategoryTheory.SimplicialObject.Augmented C),
  (((CategoryTheory.SimplicialObject.Augmented.whiskering C D).map η).app A).left =
    CategoryTheory.Functor.whiskerLeft (CategoryTheory.SimplicialObject.Augmented.drop.obj A) η
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.smul_nonpos : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m0} {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : PartialOrder F]
  [IsOrderedAddMonoid F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] [IsOrderedModule ℝ F] {f : ι → Ω → F} {c : ℝ},
  c ≤ 0 → MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Supermartingale (c • f) ℱ μ
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.maxValueSealed : ISize
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_eq_single_of_mem : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → M},
  ∀ a ∈ s, (∀ b ∈ s, b ≠ a → f b = 0) → ∑ x ∈ s, f x = f a
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_smul_eq_top_of_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {z₀ : 𝕜} {f : 𝕜 → 𝕜}, analyticOrderAt f z₀ = ⊤ → analyticOrderAt (f • g) z₀ = ⊤
-- Mathlib.Topology.EMetricSpace.Weak
instWeakPseudoEMetricSpaceWithBot.eq_1 : ∀ {α : Type u} [t : TopologicalSpace α] [inst : LinearOrder α] [inst_1 : OrderTopology α]
  [m : WeakPseudoEMetricSpace α],
  instWeakPseudoEMetricSpaceWithBot =
    { toEDist := instEDistWithBot, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, topology_le := ⋯,
      topology_eq_on_restrict := ⋯ }
-- Init.Data.UInt.Lemmas
UInt32.add_right_inj : ∀ {a b : UInt32} (c : UInt32), c + a = c + b ↔ a = b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R}, P ≈ Q → W'.neg P ≈ W'.neg Q
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteSpanningSetsIn.mk.sizeOf_spec : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} [inst : SizeOf α]
  [inst_1 : (a : Set α) → SizeOf (C a)] (set : ℕ → Set α) (set_mem : ∀ (i : ℕ), set i ∈ C)
  (finite : ∀ (i : ℕ), μ (set i) < ⊤) (spanning : ⋃ i, set i = Set.univ),
  sizeOf { set := set, set_mem := set_mem, finite := finite, spanning := spanning } = 1 + sizeOf spanning
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_neg_Iic : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : PartialOrder G] [inst_3 : AddCommGroup G] [IsOrderedAddMonoid G] [MeasurableNeg G] [μ.IsNegInvariant]
  {c : G} {f : G → F},
  MeasureTheory.IntegrableOn f (Set.Ici (-c)) μ → MeasureTheory.IntegrableOn (fun x => f (-x)) (Set.Iic c) μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_nonneg_iff_sign_nonneg : ∀ {θ : Real.Angle}, 0 ≤ θ.toReal ↔ 0 ≤ θ.sign
-- Batteries.Data.UInt
UInt64.toUInt32_toNat : ∀ (x : UInt64), x.toUInt32.toNat = x.toNat % 2 ^ 32
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V},
  Disjoint s t → ∀ (f : ↑s ≃ ↑t), (∀ (v : ↑s), G.Adj ↑v ↑(f v)) → ∃ M, M.verts = s ∪ t ∧ M.IsMatching
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  (o : CategoryTheory.HomOrthogonal s) {α β : Type} [inst_3 : Finite α] [inst_4 : Finite β] {f : α → ι} {g : β → ι}
  (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (i : ι) (j : ↑(g ⁻¹' {i})) (k : ↑(f ⁻¹' {i})),
  o.matrixDecompositionAddEquiv z i j k =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j)
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
LinearIsometryEquiv.ofBounds.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗ[σ₁₂] E₂) (h₁ : ∀ (x : E), ‖e x‖ ≤ ‖x‖) (h₂ : ∀ (y : E₂), ‖e.symm y‖ ≤ ‖y‖),
  LinearIsometryEquiv.ofBounds e h₁ h₂ = { toLinearEquiv := e, norm_map' := ⋯ }
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_sub_sinh : ∀ (x : ℝ), Real.cosh x - Real.sinh x = Real.exp (-x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_diff_eq_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_isPrefix_aig : ∀ {expr : Std.Tactic.BVDecide.BVLogicalExpr} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit}
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Sat.AIG.IsPrefix aig.decls (↑(Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).result).aig.decls
-- Mathlib.Order.WithBot
WithBot.LT.coe_lt_coe : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a < b → (↑a).LT ↑b
-- Mathlib.RepresentationTheory.Basic
Representation.dual_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρV : Representation k G V) (g : G), ρV.dual g = Module.Dual.transpose (ρV g⁻¹)
-- Mathlib.NumberTheory.Height.MvPolynomial
Height.logHeight_sym2_ge : ∀ (K : Type u_4) [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K],
  ∃ C,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 →
          C + Height.logHeight ![a, b] + Height.logHeight ![c, d] ≤ Height.logHeight ![a * c, a * d + b * c, b * d]
-- Std.Time.Time.Unit.Basic
/-- Converts a `Millisecond.Offset` to a `Minute.Offset`.
 -/
Std.Time.Millisecond.Offset.toMinutes : Std.Time.Millisecond.Offset → Std.Time.Minute.Offset
-- Std.Time.DateTime
/-- Subtract `Second.Offset` from a `DateTime`.
 -/
Std.Time.DateTime.subSeconds : Std.Time.DateTime → Std.Time.Second.Offset → Std.Time.DateTime
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_zero_sub_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), Metric.ball 0 δ - {x} = Metric.ball (-x) δ
-- Mathlib.Topology.NhdsKer
subset_nhdsKer : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, s ⊆ nhdsKer s
-- Mathlib.Topology.Algebra.Group.Basic
topologicalGroup_of_indiscreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Group H] [IndiscreteTopology H], IsTopologicalGroup H
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PreDiscrTree.modifyAt : {α : Type} →
  Lean.Meta.LazyDiscrTree.PreDiscrTree α →
    Lean.Meta.LazyDiscrTree.Key →
      (Array (Lean.Meta.LazyDiscrTree.LazyEntry α) → Array (Lean.Meta.LazyDiscrTree.LazyEntry α)) →
        Lean.Meta.LazyDiscrTree.PreDiscrTree α
-- Mathlib.Order.PFilter
Order.PFilter.mem_of_mem_of_le : ∀ {P : Type u_1} [inst : Preorder P] {x : P} {F G : Order.PFilter P}, x ∈ F → F ≤ G → x ∈ G
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_union_le_size_add_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Init.Data.String.Basic
String.Pos.offset_ofCopy : ∀ {s : String.Slice} {pos : s.copy.Pos}, pos.ofCopy.offset = pos.offset
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.liftUnique.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x)
  (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F)
  (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z)
  (hh :
    ∀ (x : C),
      CategoryTheory.CategoryStruct.comp
          (G.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj x))) hG.hom =
        CategoryTheory.CategoryStruct.comp (h.hom.app x) (M x)),
  CategoryTheory.WithTerminal.liftUnique F M hM G h hG hh =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        match X with
        | CategoryTheory.WithTerminal.of x => h.app x
        | CategoryTheory.WithTerminal.star => hG)
      ⋯
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.top_σ : ∀ {α : Type u_1}, Filter.Realizer.top.σ = Unit
-- Mathlib.Order.Lattice
/-- A type with a commutative, associative and idempotent binary `sup` operation has the structure of a
join-semilattice.

The partial order is defined so that `a ≤ b` unfolds to `a ⊔ b = b`; cf. `sup_eq_right`.
 -/
SemilatticeSup.mk' : {α : Type u_1} →
  [inst : Max α] →
    (∀ (a b : α), a ⊔ b = b ⊔ a) → (∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) → (∀ (a : α), a ⊔ a = a) → SemilatticeSup α
-- Init.Data.SInt.Lemmas
Int16.neg_mul_comm : ∀ (a b : Int16), -a * b = a * -b
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_mul_relfinrank_eq_inf_relfinrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E)
  {B C : IntermediateField F E}, B ≤ C → A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C
-- Mathlib.CategoryTheory.WithTerminal.FinCategory
CategoryTheory.WithTerminal.instFinCategory : (C : Type u) →
  [inst : CategoryTheory.SmallCategory C] →
    [CategoryTheory.FinCategory C] → CategoryTheory.FinCategory (CategoryTheory.WithTerminal C)
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.sInf_mem : ∀ {α : Type u_2} {s : Set α} [inst : CompleteLattice α],
  CountableInfClosed s → ∀ {A : Set α}, A.Countable → A.Nonempty → (∀ a ∈ A, a ∈ s) → sInf A ∈ s
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.set_smul_mono_left : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (N : Submodule R M) {s t : Set S}, s ⊆ t → s • N ≤ t • N
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Raised.add_right : ∀ (k : ℕ) {n m : ℕ}, Ordnode.Raised n m → Ordnode.Raised (n + k) (m + k)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.LaxMonoidalFunctor.laxMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (self : CategoryTheory.LaxMonoidalFunctor C D) → self.LaxMonoidal
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdxTR.go.eq_def : ∀ {α : Type u_1} (l a : List α) (a_1 : ℕ) (a_2 : Array α),
  List.eraseIdxTR.go✝ l a a_1 a_2 =
    match a, a_1, a_2 with
    | [], x, x_1 => l
    | head :: as, 0, acc => acc.toListAppend as
    | a :: as, n.succ, acc => List.eraseIdxTR.go✝ l as n (acc.push a)
-- Mathlib.AlgebraicTopology.SimplicialCategory.Basic
/-- The bifunctor `Cᵒᵖ ⥤ C ⥤ SSet.{v}` which sends `K : Cᵒᵖ` and `L : C` to `sHom K.unop L`.  -/
CategoryTheory.SimplicialCategory.sHomFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.SimplicialCategory C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C SSet)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.mk : Bool → Bool → ℕ → Array Lean.MVarId → Array Lean.MVarId → Lean.Meta.Sym.DefEqM.Context✝
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd_assoc : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp T.SpecTensorTo
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr)
      (CategoryTheory.CategoryStruct.comp (Y.fromSpecResidueField T.y) h)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_filter_lt_of_lt_right : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => x < c], b < c → {x ∈ Finset.Icc a b | x < c} = Finset.Icc a b
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
/-- If a family `x` is algebraically independent, then any of its element is transcendental.  -/
AlgebraicIndependent.transcendental : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A], AlgebraicIndependent R x → ∀ (i : ι), Transcendental R (x i)
-- Mathlib.Algebra.Homology.Embedding.TruncLE
ComplexShape.Embedding.truncLE'ToRestrictionNatTrans_app : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncLE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c'),
  (e.truncLE'ToRestrictionNatTrans C).app K = K.truncLE'ToRestriction e
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α}, ∅.contains a = false
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.smul_measure : ∀ {α : Type u_2} {β : Type u_3} {R : Type u_6} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [inst_1 : SMul R ENNReal] [inst_2 : IsScalarTower R ENNReal ENNReal],
  AEMeasurable f μ → ∀ (c : R), AEMeasurable f (c • μ)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote.match_1.congr_eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (p : Int.Internal.Linear.Poly)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add k v p))
  (k : ℤ),
  p = Int.Internal.Linear.Poly.num k →
    (match p with
      | Int.Internal.Linear.Poly.num k => h_1 k
      | Int.Internal.Linear.Poly.add k v p => h_2 k v p) ≍
      h_1 k
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.pointwise_smul_toAddSubmonoid : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M)
  (S : Subsemiring R), (m • S).toAddSubmonoid = m • S.toAddSubmonoid
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.instBEqKey.beq : Lean.Meta.DiscrTree.Key → Lean.Meta.DiscrTree.Key → Bool
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.decidableMemCommonNeighbors : {V : Type u} → (G : SimpleGraph V) → [DecidableRel G.Adj] → (v w : V) → DecidablePred fun x => x ∈ G.commonNeighbors v w