mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Config.mk.inj : ∀ {maxSteps maxDischargeDepth maxSteps_1 maxDischargeDepth_1 : ℕ},
  { maxSteps := maxSteps, maxDischargeDepth := maxDischargeDepth } =
      { maxSteps := maxSteps_1, maxDischargeDepth := maxDischargeDepth_1 } →
    maxSteps = maxSteps_1 ∧ maxDischargeDepth = maxDischargeDepth_1
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The proposed colimit cocone is a colimit in `AddGroup`.  -/
AddGrpCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddGrpCat) →
        CategoryTheory.Limits.IsColimit (AddGrpCat.FilteredColimits.colimitCocone F)
-- Mathlib.MeasureTheory.Order.UpperLower
Set.OrdConnected.null_frontier : ∀ {ι : Type u_1} [inst : Fintype ι] {s : Set (ι → ℝ)}, s.OrdConnected → MeasureTheory.volume (frontier s) = 0
-- Mathlib.RingTheory.Polynomial.Hermite.Gaussian
/-- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a Gaussian.  -/
Polynomial.deriv_gaussian_eq_hermite_mul_gaussian : ∀ (n : ℕ) (x : ℝ),
  deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ n * (Polynomial.aeval x) (Polynomial.hermite n) * Real.exp (-(x ^ 2 / 2))
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- For `c, d ∈ ℝ` with `1 ≤ d ^ 2`, we have `r1 z ≤ |c * z + d| ^ 2`.  -/
EisensteinSeries.r1_aux_bound : ∀ (z : UpperHalfPlane) (c : ℝ) {d : ℝ}, 1 ≤ d ^ 2 → EisensteinSeries.r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2
-- Mathlib.Algebra.Opposites
AddOpposite.unop_zero : ∀ {α : Type u_1} [inst : Zero α], AddOpposite.unop 0 = 0
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
/-- Reinterpret an element of a type of completely positive maps as a completely positive linear
map.  -/
CompletelyPositiveMapClass.toCompletelyPositiveLinearMap : {F : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      [inst : NonUnitalCStarAlgebra A₁] →
        [inst_1 : NonUnitalCStarAlgebra A₂] →
          [inst_2 : PartialOrder A₁] →
            [inst_3 : PartialOrder A₂] →
              [inst_4 : StarOrderedRing A₁] →
                [inst_5 : StarOrderedRing A₂] →
                  [inst_6 : FunLike F A₁ A₂] →
                    [LinearMapClass F ℂ A₁ A₂] → [CompletelyPositiveMapClass F A₁ A₂] → F → CompletelyPositiveMap A₁ A₂
-- Mathlib.Tactic.Qify
Mathlib.Tactic.Qify.intCast_ne : ∀ (a b : ℤ), a ≠ b ↔ ↑a ≠ ↑b
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.fiberBundle_trivializationAt' : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (x : B),
  FiberBundle.trivializationAt' x = Bundle.Trivial.trivialization B F
-- Mathlib.Order.Heyting.Hom
HeytingHom.toFun_eq_coe_aux : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] {f : HeytingHom α β},
  ⇑f.toLatticeHom = ⇑f
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `‖f a‖ ≤ B a`;
* `f` and `B` have right derivatives `f'` and `B'` respectively at every point of `[a, b)`;
* we have `‖f' x‖ ≤ B x` everywhere on `[a, b)`.

Then `‖f x‖ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
to make this theorem work for piecewise differentiable functions.
 -/
image_norm_le_of_norm_deriv_right_le_deriv_boundary' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      ∀ {B B' : ℝ → ℝ},
        ‖f a‖ ≤ B a →
          ContinuousOn B (Set.Icc a b) →
            (∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
              (∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.injective_noncommPiCoprod_of_iSupIndep : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → Group (H i)]
  (ϕ : (i : ι) → H i →* G) [inst_2 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)},
  (iSupIndep fun i => (ϕ i).range) →
    (∀ (i : ι), Function.Injective ⇑(ϕ i)) → Function.Injective ⇑(MonoidHom.noncommPiCoprod ϕ hcomm)
-- Init.Data.Vector.Count
Vector.boole_getElem_le_countP : ∀ {α : Type u_1} {n i : ℕ} {p : α → Bool} {xs : Vector α n} (h : i < n),
  (if p xs[i] = true then 1 else 0) ≤ Vector.countP p xs
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_symm_apply_coe : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (a : α),
  ↑((Ordinal.enum r).symm a) = (Ordinal.typein r).toRelEmbedding a
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeDomainAddMonoidHom_apply : ∀ {ι : Type u} (β : ι → Type v) [inst : (i : ι) → AddZeroClass (β i)] (p : ι → Prop) [inst_1 : DecidablePred p]
  (x : Π₀ (i : ι), β i), (DFinsupp.subtypeDomainAddMonoidHom β p) x = DFinsupp.subtypeDomain p x
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_inter_Ioo_of_left_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  b₁ < b₂ → Set.Ioc a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioc (max a₁ a₂) b₁
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.comap_coe_eq_uniformity : ∀ (α : Type u_1) [inst : UniformSpace α],
  Filter.comap (fun p => (↑p.1, ↑p.2)) (uniformity (UniformSpace.Completion α)) = uniformity α
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalUnknown : Lean.Elab.Tactic.Tactic
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.stabilizerHom.congr_simp : ∀ {A : Type u_3} {B : Type u_4} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p] (G : Type u_6) [inst_4 : Group G] [inst_5 : MulSemiringAction G B]
  [inst_6 : SMulCommClass G A B], Ideal.Quotient.stabilizerHom P p G = Ideal.Quotient.stabilizerHom P p G
-- Mathlib.GroupTheory.Transfer
/-- Auxiliary lemma in order to state `transfer_eq_pow`.  -/
MonoidHom.transfer_eq_pow_aux : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G),
  (∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k) → g ^ H.index ∈ H
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_smul`. -/
CuspForm.IsGLPos.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Topology.DiscreteSubset
/-- In a `T1Space`, every set is codiscrete within a subsingleton set.
 -/
Set.Subsingleton.mem_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s t : Set X}, t.Subsingleton → s ∈ Filter.codiscreteWithin t
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
_private.Mathlib.Combinatorics.Additive.PluenneckeRuzsa.0.Finset.card_mul_pow_le : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] {A B : Finset G},
  (∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card) →
    ∀ (n : ℕ), ↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.nnnorm_down : ∀ {E : Type u_2} [inst : NNNorm E] (x : ULift.{u_5, u_2} E), ‖x.down‖₊ = ‖x‖₊
-- Mathlib.RingTheory.Ideal.IsPrimary
Ideal.isPrime_radical : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, I.IsPrimary → I.radical.IsPrime
-- Mathlib.Order.WithBot
WithTop.toDual.eq_1 : ∀ {α : Type u_1}, WithTop.toDual = Equiv.refl (WithTop α)
-- Mathlib.Algebra.Polynomial.Smeval
/-- `Polynomial.smeval` as a linear map.  -/
Polynomial.smeval.linearMap : (R : Type u_1) →
  [inst : Semiring R] →
    {S : Type u_2} → [inst_1 : AddCommMonoid S] → [Pow S ℕ] → [inst_3 : Module R S] → S → Polynomial R →ₗ[R] S
-- Init.System.IO
/-- Returns the file name of the currently-running executable.
 -/
IO.appPath : IO System.FilePath
-- Mathlib.Algebra.Ring.ULift
ULift.nonUnitalNonAssocSemiring : {R : Type u} → [NonUnitalNonAssocSemiring R] → NonUnitalNonAssocSemiring (ULift.{u_1, u} R)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The underlying modification of oplax transformations.  -/
CategoryTheory.Lax.OplaxTrans.Hom.as : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Lax.OplaxTrans.Hom η θ → CategoryTheory.Lax.OplaxTrans.Modification η θ
-- Mathlib.Probability.Martingale.OptionalSampling
MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m}
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {i n : ι},
  MeasureTheory.Martingale f ℱ μ →
    ∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
      i ≤ n → μ[f n | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] f i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  [inst_2 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDTreeMap.ofList l cmp).get? k = none
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_ofList_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → ∀ {h' : k' ∈ Std.HashMap.Raw.ofList l}, (Std.HashMap.Raw.ofList l).getKey k' h' = k
-- Mathlib.Data.PNat.Factors
/-- The product map gives a homomorphism from the additive monoid
of multisets to the multiplicative monoid ℕ+.  -/
PrimeMultiset.prod_zero : PrimeMultiset.prod 0 = 1
-- Mathlib.MeasureTheory.Group.Pointwise
MeasurableSet.const_smul_of_ne_zero : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MulAction G₀ α] [inst_2 : MeasurableSpace α]
  [MeasurableConstSMul G₀ α] {s : Set α}, MeasurableSet s → ∀ {a : G₀}, a ≠ 0 → MeasurableSet (a • s)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The negation of a projective point class on a Weierstrass curve `W`.

If `P` is a projective point representative on `W`, then `W.negMap ⟦P⟧` is definitionally equivalent
to `W.neg P`.  -/
WeierstrassCurve.Projective.negMap : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Projective R → WeierstrassCurve.Projective.PointClass R → WeierstrassCurve.Projective.PointClass R
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertEntry.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.insertEntry k v l =
    bif Std.Internal.List.containsKey k l then Std.Internal.List.replaceEntry k v l else ⟨k, v⟩ :: l
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_π_ne : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {j j' : J},
  j ≠ j' →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
        (CategoryTheory.Limits.biproduct.π f j') =
      0
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.cons₁ : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Cont'
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.toSSetObj₁Equiv_apply_zero : ∀ {X : TopCat} (s : (TopCat.toSSet.obj X).obj (Opposite.op { len := 1 })),
  (CategoryTheory.ConcreteCategory.hom (TopCat.toSSetObj₁Equiv s)) 0 =
    TopCat.toSSetObj₀Equiv
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) 1)) s)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
/-- `zarankiewicz m n s t` is greater than `x` if and only if there
exists a `completeBipartiteGraph α β`-free bipartite graph `G` with more than `x` edges.  -/
SimpleGraph.lt_zarankiewicz_iff : ∀ {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : Fintype α] [inst_3 : Fintype β],
  Fintype.card V = m →
    Fintype.card W = n →
      Fintype.card α = s →
        Fintype.card β = t →
          ∀ (x : ℕ),
            x < SimpleGraph.zarankiewicz m n s t ↔
              ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < G.edgeFinset.card
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.map_taylorEquiv_degreeLT : ∀ {R : Type u_1} [inst : CommRing R] {r : R} {n : ℕ},
  Submodule.map (↑↑(Polynomial.taylorEquiv r)) (Polynomial.degreeLT R n) = Polynomial.degreeLT R n
-- Mathlib.Algebra.Order.Sub.Defs
tsub_nonpos : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  a - b ≤ 0 ↔ a ≤ b
-- Mathlib.Data.Finset.Image
Finset.image_inter : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} [inst_1 : DecidableEq α] (s₁ s₂ : Finset α),
  Function.Injective f → Finset.image f (s₁ ∩ s₂) = Finset.image f s₁ ∩ Finset.image f s₂
-- Batteries.Data.Fin.Lemmas
Fin.eq_false_of_findRev?_eq_some_of_lt : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, Fin.findRev? p = some i → ∀ (j : Fin n), i < j → p j = false
-- Mathlib.Order.Defs.Unbundled
Std.Asymm.decide : ∀ {α : Sort u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Asymm r], Std.Asymm fun a b => decide (r a b) = true
-- Lean.Compiler.Options
Lean.Compiler.compiler.check : Lean.Option Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true → t.minKey? = none
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).fst = X.base
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- Post-composing an additive character to `ℂ` with complex conjugation gives the inverse
character.  -/
AddChar.starComp_eq_inv : ∀ {R : Type u_1} [inst : CommRing R], 0 < ringChar R → ∀ {φ : AddChar R ℂ}, (↑(starRingEnd ℂ)).compAddChar φ = φ⁻¹
-- Mathlib.LinearAlgebra.CrossProduct
/-- **Jacobi identity**: For a cross product of three vectors,
their sum over the three even permutations is equal to the zero vector.  -/
jacobi_cross : ∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
  (crossProduct u) ((crossProduct v) w) + (crossProduct v) ((crossProduct w) u) +
      (crossProduct w) ((crossProduct u) v) =
    0
-- Mathlib.Topology.Constructions
Subtype.dense_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {t : Set ↑s}, Dense t ↔ s ⊆ closure (Subtype.val '' t)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.preservesColimits_forgetToSheafedSpace : CategoryTheory.Limits.PreservesColimits AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Mathlib.Data.List.Chain
List.IsChain.prefix : ∀ {α : Type u_1} {R : α → α → Prop} {l l₁ : List α}, List.IsChain R l → l₁ <+: l → List.IsChain R l₁
-- Mathlib.Analysis.Normed.Group.Basic
/-- The norm of a normed group as an additive group norm.  -/
normAddGroupNorm : (E : Type u_5) → [inst : NormedAddGroup E] → AddGroupNorm E
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_eq_of_semiconjBy : ∀ {f g₁ g₂ : CircleDeg1Lift}, SemiconjBy f g₁ g₂ → g₁.translationNumber = g₂.translationNumber
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.arrowMap.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] {j : J}
  (F F_1 : CategoryTheory.Functor (↑(Set.Iic j)) C),
  F = F_1 →
    ∀ (i₁ i₁_1 : J) (e_i₁ : i₁ = i₁_1) (i₂ i₂_1 : J) (e_i₂ : i₂ = i₂_1) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j),
      CategoryTheory.SmallObject.SuccStruct.arrowMap F i₁ i₂ h₁₂ h₂ =
        CategoryTheory.SmallObject.SuccStruct.arrowMap F_1 i₁_1 i₂_1 ⋯ ⋯
-- Lean.Language.Basic
Lean.Language.SnapshotTask.instInhabitedReportingRange.default : Lean.Language.SnapshotTask.ReportingRange
-- Lean.Elab.PreDefinition.WF.Preprocess
_private.Lean.Elab.PreDefinition.WF.Preprocess.0.Lean.Elab.WF.getSimpContext : Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_comm : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ →
    ∀ {g : α → ℝ}, MeasureTheory.Integrable (fun x => Real.exp (g x)) μ → (μ.tilted f).tilted g = (μ.tilted g).tilted f
-- Mathlib.Order.Filter.Partial
/-- Generic "limit of a relation" predicate. `RTendsto' r l₁ l₂` asserts that for every
`l₂`-neighborhood `a`, the `r`-preimage of `a` is an `l₁`-neighborhood. One generalization of
`Filter.Tendsto` to relations.  -/
Filter.RTendsto' : {α : Type u} → {β : Type v} → SetRel α β → Filter α → Filter β → Prop
-- Lean.Elab.InfoTree.Main
Lean.Elab.ChoiceInfo.format : Lean.Elab.ContextInfo → Lean.Elab.ChoiceInfo → Std.Format
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Remove the first `i` elements of the set, counted from the left.

```
drop 2 {a, b, c, d} = {c, d}
drop 5 {a, b, c, d} = ∅
```  -/
Ordnode.drop : {α : Type u_1} → ℕ → Ordnode α → Ordnode α
-- Init.Data.UInt.IntToBitVec
USize.lt_iff_toBitVec64_lt : ∀ {a b : USize} (h : System.Platform.numBits = 64), a < b ↔ a.toBitVec64 h < b.toBitVec64 h
-- Mathlib.Data.Nat.Factors
Nat.mem_primeFactorsList' : ∀ {n p : ℕ}, p ∈ n.primeFactorsList ↔ Nat.Prime p ∧ p ∣ n ∧ n ≠ 0
-- Init.Data.Array.Zip
Array.map_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : γ → δ → α} {cs : Array γ} {ds : Array δ},
  Array.map f (Array.zipWith g cs ds) = Array.zipWith (fun x y => f (g x y)) cs ds
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryLT!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {k : α}, t₁.Equiv t₂ → t₁.getEntryLT! k = t₂.getEntryLT! k
-- Mathlib.Analysis.CStarAlgebra.Basic
/-- A C⋆-ring is a normed star ring that satisfies the stronger condition `‖x‖ ^ 2 ≤ ‖x⋆ * x‖`
for every `x`. Note that this condition actually implies equality, as is shown in
`norm_star_mul_self` below.  -/
CStarRing : (E : Type u_4) → [inst : NonUnitalNormedRing E] → [StarRing E] → Prop
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
GaloisConnection.u_ciInf_set : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {s : Set γ} {f : γ → β}, BddBelow (f '' s) → s.Nonempty → u (⨅ i, f ↑i) = ⨅ i, u (f ↑i)
-- Mathlib.Analysis.MellinInversion
mellin_eq_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) {s : ℂ},
  mellin f s = FourierTransform.fourier (fun u => Real.exp (-s.re * u) • f (Real.exp (-u))) (s.im / (2 * Real.pi))
-- Mathlib.Order.Filter.CardinalInter
Filter.EventuallyEq.cardinal_bUnion : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι},
  Cardinal.mk ↑S < c →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) → ⋃ i, ⋃ (h : i ∈ S), s i h =ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.instInhabitedMachine : (Γ : Type u_1) → (Λ : Type u_2) → [inst : Inhabited Λ] → Inhabited (Turing.TM0.Machine Γ Λ)
-- Mathlib.Algebra.GradedMonoid
SetLike.gOne : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : SetLike S R] →
        [inst_1 : One R] → [inst_2 : Zero ι] → (A : ι → S) → [SetLike.GradedOne A] → GradedMonoid.GOne fun i => ↥(A i)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pullbacks_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {A B X Y : C}
  {f : A ⟶ X} {q : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}, CategoryTheory.IsPullback f q p g → P p → P.pullbacks q
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 7 ≤ n → n < 2 ^ 7 → (Int8.ofInt n).toNatClampNeg = n.toNat
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f g : 𝕜 → F},
  Set.EqOn f g s → Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
CommRingCat.KaehlerDifferential.ext : ∀ {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} {α β : CommRingCat.KaehlerDifferential f ⟶ M},
  (∀ (b : ↑B),
      (CategoryTheory.ConcreteCategory.hom α) (CommRingCat.KaehlerDifferential.d b) =
        (CategoryTheory.ConcreteCategory.hom β) (CommRingCat.KaehlerDifferential.d b)) →
    α = β
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.linearMap.eq_1 : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂), b₁.linearMap b₂ = (Matrix.stdBasis R ι₂ ι₁).map (LinearMap.toMatrix b₁ b₂).symm
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveCodeProps.mk.injEq : ∀ (fmt fmt_1 : Lean.Widget.CodeWithInfos), ({ fmt := fmt } = { fmt := fmt_1 }) = (fmt = fmt_1)
-- Mathlib.Algebra.Notation.Prod
Prod.instVAdd : {E : Type u_8} → {α : Type u_9} → {β : Type u_10} → [VAdd E α] → [VAdd E β] → VAdd E (α × β)
-- Mathlib.ModelTheory.Order
/-- The type of relations for the language of orders, consisting of a single binary relation `le`.
 -/
FirstOrder.Language.orderRel : ℕ → Type
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.Over.mapId.eq_1 : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (Y : T),
  CategoryTheory.Over.mapId Y =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Over.isoMk
          (CategoryTheory.Iso.refl ((CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id Y)).obj x).left) ⋯)
      ⋯
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instIsIsoMonHomGrp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.CommGrp C} {f : G ⟶ H} [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.hom.hom