mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToLimit.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cone (K.comp F)} {t : CategoryTheory.Limits.IsLimit c}
  {toLiftableCone : CategoryTheory.LiftableCone K F c}
  {makesLimit : CategoryTheory.Limits.IsLimit toLiftableCone.liftedCone}
  {toLiftableCone_1 : CategoryTheory.LiftableCone K F c}
  {makesLimit_1 : CategoryTheory.Limits.IsLimit toLiftableCone_1.liftedCone},
  { toLiftableCone := toLiftableCone, makesLimit := makesLimit } =
      { toLiftableCone := toLiftableCone_1, makesLimit := makesLimit_1 } →
    toLiftableCone = toLiftableCone_1 ∧ makesLimit ≍ makesLimit_1
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go.match_13.eq_1 : ∀ (motive : Std.Sat.AIG.Decl ℕ → Sort u_1)
  (h_1 : Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : ℕ) → Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match heq : Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 heq
    | Std.Sat.AIG.Decl.atom idx => h_2 idx heq
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs heq) =
    h_1 ⋯
-- Mathlib.RepresentationTheory.Rep.Basic
/-- There is a `k`-linear isomorphism between the sets of representation morphisms `Hom(A ⊗ B, C)`
and `Hom(A, Homₖ(B, C))`.  -/
Rep.MonoidalClosed.linearHomEquivComm : {k : Type u} →
  [inst : CommRing k] →
    {G : Type v} →
      [inst_1 : Group G] →
        (A B C : Rep.{u, u, v} k G) → (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ₗ[k] A ⟶ B ⟹ C
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_union : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (s₁ s₂ : Multiset α),
  (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.finrank_R : ∀ (σ K : Type u) [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ],
  Module.finrank K (MvPolynomial.R σ K) = Fintype.card (σ → K)
-- Mathlib.Topology.UniformSpace.Ultra.Completion
CauchyFilter.isTrans_gen : ∀ {X : Type u_1} [inst : UniformSpace X] {s : SetRel X X} [s.IsTrans], (CauchyFilter.gen s).IsTrans
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToColimit.toLiftableCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                  {t : CategoryTheory.Limits.IsColimit c} →
                    CategoryTheory.LiftsToColimit K F c t → CategoryTheory.LiftableCocone K F c
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {f : α → Bool} {k : α},
  t.WF → (Std.TreeMap.Raw.filter (fun k x => f k) t).getKey! k = (Option.filter f (t.getKey? k)).get!
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofMulDistribMulAction_ρ_apply_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : Monoid M] [inst_1 : CommGroup G] [inst_2 : MulDistribMulAction M G] (g : M)
  (a : Additive G), ((Rep.ofMulDistribMulAction M G).ρ g) a = Additive.ofMul (g • Additive.toMul a)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited γ] {f : α → β → Option γ}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValue! k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
          ((Std.Internal.List.getValue? k l).bind fun x => f k' x).get!
-- Mathlib.MeasureTheory.Category.MeasCat
/-- The underlying measurable space.  -/
MeasCat.carrier : MeasCat → Type u
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_hom_comp_biproduct_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom
      (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X
-- Init.Data.Vector.Monadic
Vector.foldrM_map : ∀ {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m]
  {f : β₁ → β₂} {g : β₂ → α → m α} {xs : Vector β₁ n} {init : α},
  Vector.foldrM g init (Vector.map f xs) = Vector.foldrM (fun x y => g (f x) y) init xs
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keysArray.size = m.size
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_alter_eq_add_one : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∉ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size + 1
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Presieve.FamilyOfElements.map.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (p : CategoryTheory.Presieve.FamilyOfElements P R) (φ : P ⟶ Q) (x : C) (f : x ⟶ X)
  (hf : R f), p.map φ f hf = (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op x))) (p f hf)
-- Init.Data.Ord.UInt
UInt64.instTransOrd : Std.TransOrd UInt64
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication.  -/
AddAction.automorphize_smul_left : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [T2Space M]
  {R : Type u_12} [inst_3 : DivisionRing R] [inst_4 : Module R M] [ContinuousConstSMul R M] [inst_6 : AddGroup α]
  [inst_7 : AddAction α β] (f : β → M) (g : Quotient (AddAction.orbitRel α β) → R),
  AddAction.automorphize (g ∘ Quotient.mk' • f) = g • AddAction.automorphize f
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.mop_inv_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C), (β_ X Y).inv.mop = (β_ { unmop := Y } { unmop := X }).inv
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.map_polynomialY : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] (f : R →+* S),
  (W'.map f).polynomialY = (MvPolynomial.map f) W'.polynomialY
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.ofHom_hom_hom : ∀ {X Y : FinPartOrd} (f : X ⟶ Y), FinPartOrd.ofHom (PartOrd.Hom.hom f.hom) = f
-- Init.Prelude
/-- Exception monads provide the ability to throw errors and handle errors.

In this class, `ε` is a `semiOutParam`, which means that it can influence the choice of instance.
`MonadExcept ε` provides the same operations, but requires that `ε` be inferable from `m`.

`tryCatchThe`, which takes an explicit exception type, is used to desugar `try ... catch ...` steps
inside `do`-blocks when the handlers have type annotations.
 -/
MonadExceptOf : semiOutParam (Type u) → (Type v → Type w) → Type (max (max u (v + 1)) w)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {a : R}, SkewPolynomial.C a = 0 ↔ a = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.erase k).getKey? a = if cmp k a = Ordering.eq then none else t.getKey? a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil.destruct = none
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_of_subsingleton_codomain : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [Subsingleton β] (f : α → β),
  Measurable f
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.measurable_ofReal : Measurable ENNReal.ofReal
-- Lean.Server.Completion.CompletionUtils
/-- Get type names for resolving `id` in `s.id x₁ ... xₙ` notation.  -/
Lean.Server.Completion.getDotCompletionTypeNames : Lean.Expr → Lean.MetaM (Array Lean.Name)
-- Mathlib.Data.EReal.Basic
/-- The type of extended real numbers `[-∞, ∞]`, constructed as `WithBot (WithTop ℝ)`.  -/
EReal : Type
-- Mathlib.Algebra.Quandle
Rack.self_invAct_act_eq : ∀ {R : Type u_1} [inst : Rack R] {x y : R}, Shelf.act (Rack.invAct x x) y = Shelf.act x y
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddEquiv.subsemigroupMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (S : AddSubsemigroup M),
  e.subsemigroupMap S =
    { toFun := fun x => ⟨e ↑x, ⋯⟩, invFun := fun x => ⟨e.symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Init.Data.Rat.Lemmas
Rat.mul_eq_zero : ∀ {a b : ℚ}, a * b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
vectorSpan_vadd : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P) (v : V), vectorSpan k (v +ᵥ s) = vectorSpan k s
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.endSection.injEq : ∀ (stx : Lean.Syntax) (id? : Option Lean.Name) (danglingDot : Bool) (scopeNames : List String) (stx_1 : Lean.Syntax)
  (id?_1 : Option Lean.Name) (danglingDot_1 : Bool) (scopeNames_1 : List String),
  (Lean.Elab.CompletionInfo.endSection stx id? danglingDot scopeNames =
      Lean.Elab.CompletionInfo.endSection stx_1 id?_1 danglingDot_1 scopeNames_1) =
    (stx = stx_1 ∧ id? = id?_1 ∧ danglingDot = danglingDot_1 ∧ scopeNames = scopeNames_1)
-- Mathlib.Tactic.Ring.Basic
/-- The output value `b` is equal to the lift of `a`. This can be supplied by the default
instance which sets `b := lift a`, but `ring` will treat this as an atom so it is more useful
when there are other instances which distribute addition or multiplication.  -/
Mathlib.Tactic.Ring.CSLiftVal.eq : ∀ {α : Type u} {β : outParam (Type u)} {inst : Mathlib.Tactic.Ring.CSLift α β} {a : α} {b : outParam β}
  [self : Mathlib.Tactic.Ring.CSLiftVal a b], b = Mathlib.Tactic.Ring.CSLift.lift a
-- Mathlib.Topology.CompactOpen
ContinuousMap.uncurry_apply : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : LocallyCompactSpace Y] (f : C(X, C(Y, Z))) (a : X × Y),
  f.uncurry a = Function.uncurry (fun x y => (f x) y) a
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_bool : ∀ {α : Type u_1} [inst : AddCommMonoid α] (f : Bool → α), ∑ b, f b = f true + f false
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
GromovHausdorff.HD.eq_1 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : GromovHausdorff.Cb✝ X Y),
  GromovHausdorff.HD f = max (⨆ x, ⨅ y, f (Sum.inl x, Sum.inr y)) (⨆ y, ⨅ x, f (Sum.inl x, Sum.inr y))
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instSub.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddGroup γ] [inst_3 : IsTopologicalAddGroup γ],
  MeasureTheory.AEEqFun.instSub = { sub := MeasureTheory.AEEqFun.comp₂ Sub.sub ⋯ }
-- Mathlib.Order.Irreducible
supPrime_ofDual : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : αᵒᵈ}, SupPrime (OrderDual.ofDual a) ↔ InfPrime a
-- Mathlib.Analysis.Analytic.Composition
/-- For `n ≠ 1`, the `n`-th coefficient of `id 𝕜 E` is zero, by definition.  -/
FormalMultilinearSeries.id_apply_of_one_lt : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E) {n : ℕ}, 1 < n → FormalMultilinearSeries.id 𝕜 E x n = 0
-- Mathlib.Data.Finset.Max
Finset.min_empty : ∀ {α : Type u_2} [inst : LinearOrder α], ∅.min = ⊤
-- Init.Grind.Ring.Field
/-- Zero is not equal to one: fields are non trivial. -/
Lean.Grind.Field.zero_ne_one : ∀ {α : Type u} [self : Lean.Grind.Field α], 0 ≠ 1
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfPair.mk : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R},
  Function.Bijective ⇑p → Function.Bijective ⇑p.flip → p.IsPerfPair
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_mul_relIndex : ∀ {G : Type u_1} [inst : Group G] (H K L : Subgroup G), H ≤ K → K ≤ L → H.relIndex K * K.relIndex L = H.relIndex L
-- Init.Data.UInt.BasicAux
/-- Converts 32-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.toUInt64 : UInt32 → UInt64
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instCoeFunForallNat : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] → [inst_3 : Ring β] → {abv : β → α} → CoeFun (CauSeq β abv) fun x => ℕ → β
-- Lean.Meta.Tactic.Replace
/-- Replaces the type of `fvarId` at `mvarId` with `typeNew`.
Remark: this method assumes that `typeNew` is definitionally equal to the current type of `fvarId`,
and that `typeNew` is well-formed at this position.

If `typeNew` is equal to current type of `fvarId`, then returns `mvarId` unchanged.
Uses `Expr.equal` for the comparison so that it is possible to update binder names, etc., which are user-visible.
 -/
Lean.MVarId.replaceLocalDeclDefEq : Lean.MVarId → Lean.FVarId → Lean.Expr → Lean.MetaM Lean.MVarId
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
/-- The class of isomorphisms modulo a Serre class: given a
Serre class `P : ObjectProperty C`, this is the class of morphisms `f`
such that `kernel f` and `cokernel f` satisfy `P`.  -/
CategoryTheory.ObjectProperty.isoModSerre : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (P : CategoryTheory.ObjectProperty C) → [P.IsSerreClass] → CategoryTheory.MorphismProperty C
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_zero_or_pos_or_neg : ∀ {f : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially f →
    (∀ᶠ (x : ℝ) in Filter.atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in Filter.atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in Filter.atTop, f x < 0
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.instPatternModel : {pat : String.Slice} → String.Slice.Pattern.Model.PatternModel pat
-- Init.Core
/-- `Asymm r` means that the binary relation `r` is asymmetric, that is, `r a b → ¬ r b a`.  -/
Std.Asymm : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
/-- Constructor for cocycles to a single complex.  -/
CochainComplex.HomComplex.Cocycle.toSingleMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X : C} →
          {K : CochainComplex C ℤ} →
            {p q : ℤ} →
              (f : K.X p ⟶ X) →
                {n : ℤ} →
                  p + n = q →
                    (p' : ℤ) →
                      p' + 1 = p →
                        CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0 →
                          CochainComplex.HomComplex.Cocycle K ((CochainComplex.singleFunctor C q).obj X) n
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.card_le_preAleph : ∀ (o : Ordinal.{u_1}), o.card ≤ Cardinal.preAleph o
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.subtypeEmb.eq_1 : ∀ {β : Type u_2} [inst : TopologicalSpace β] {α : Type u_5} (p : α → Prop) (e : α → β) (x : { x // p x }),
  IsDenseEmbedding.subtypeEmb p e x = ⟨e ↑x, ⋯⟩
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_of_le_bot : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel P Lean.Order.bot → Lean.Order.PartialOrder.rel P Q
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.ker_filter : ∀ {α : Type u_1} (F : FilterBasis α), F.filter.ker = ⋂₀ F.sets
-- Mathlib.RingTheory.Perfection
Perfection.pthRoot_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  (Perfection.pthRoot R p).comp (frobenius (Perfection R p) p) = RingHom.id (Perfection R p)
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAt_const_add_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasDerivAt (fun x => c + f x) f' x ↔ HasDerivAt f f' x
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.mk.inj : ∀ {mvar key : Lean.Expr} {mctx : Lean.MetavarContext} {instances : Array Lean.Meta.SynthInstance.Instance}
  {currInstanceIdx : ℕ} {typeHasMVars : Bool} {mvar_1 key_1 : Lean.Expr} {mctx_1 : Lean.MetavarContext}
  {instances_1 : Array Lean.Meta.SynthInstance.Instance} {currInstanceIdx_1 : ℕ} {typeHasMVars_1 : Bool},
  { mvar := mvar, key := key, mctx := mctx, instances := instances, currInstanceIdx := currInstanceIdx,
        typeHasMVars := typeHasMVars } =
      { mvar := mvar_1, key := key_1, mctx := mctx_1, instances := instances_1, currInstanceIdx := currInstanceIdx_1,
        typeHasMVars := typeHasMVars_1 } →
    mvar = mvar_1 ∧
      key = key_1 ∧
        mctx = mctx_1 ∧ instances = instances_1 ∧ currInstanceIdx = currInstanceIdx_1 ∧ typeHasMVars = typeHasMVars_1
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Given a continuous `R`-alternating map `f` taking values in `R`, `f.smulRight z` is the
continuous alternating map sending `m` to `f m • z`.  -/
ContinuousAlternatingMap.smulRight : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : Module R M] →
                [inst_4 : Module R N] →
                  [inst_5 : TopologicalSpace R] →
                    [inst_6 : TopologicalSpace M] →
                      [inst_7 : TopologicalSpace N] → [ContinuousSMul R N] → M [⋀^ι]→L[R] R → N → M [⋀^ι]→L[R] N
-- Mathlib.Algebra.Group.Basic
pow_boole : ∀ {M : Type u_4} [inst : Monoid M] (P : Prop) [inst_1 : Decidable P] (a : M),
  (a ^ if P then 1 else 0) = if P then a else 1
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.coe_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (K : TopologicalSpace.PositiveCompacts α) (L : TopologicalSpace.PositiveCompacts β), ↑(K ×ˢ L) = ↑K ×ˢ ↑L
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_singleton_zero : ∀ (R : Type uR) (A : Type uA) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], R[0] = ⊥
-- Batteries.Data.List.Matcher
/-- Returns the start and end positions of the first infix sublist of `l` that matches `pattern`,
or `none` if there is no such sublist.
 -/
List.findInfix? : {α : Type u_1} → [BEq α] → List α → List α → Option (ℕ × ℕ)
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.find?_prop_eq_some_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String} {pos : s.Pos},
  s.find? p = some pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), ¬p (pos'.get ⋯)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.instFunLike : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} → {N : Type u_2} → [inst_1 : AddCommMonoid N] → FunLike (S.LocalizationMap N) M N
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.of.inj : ∀ {R : Type u} {inst : CommRing R} {X : Type v} {commRing : CommRing X} {hopfAlgebra : HopfAlgebra R X} {X_1 : Type v}
  {commRing_1 : CommRing X_1} {hopfAlgebra_1 : HopfAlgebra R X_1},
  { X := X, commRing := commRing, hopfAlgebra := hopfAlgebra } =
      { X := X_1, commRing := commRing_1, hopfAlgebra := hopfAlgebra_1 } →
    X = X_1 ∧ commRing ≍ commRing_1 ∧ hopfAlgebra ≍ hopfAlgebra_1
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.Raw.toListRev_iter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.iter.toListRev = m.toList.reverse
-- Mathlib.Tactic.NormNum.Basic
_private.Mathlib.Tactic.NormNum.Basic.0.Mathlib.Meta.NormNum.Result.mul.ratArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a b : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result q(«$a») →
        Mathlib.Meta.NormNum.Result q(«$b») →
          (inst : Q(Semiring «$α»)) → Q(DivisionRing «$α») → Option (Mathlib.Meta.NormNum.Result q(«$a» * «$b»))
-- Lean.Message
Lean.instInhabitedMessageData.default : Lean.MessageData
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme} [Finite ↥X] [DiscreteTopology ↥X], AlgebraicGeometry.IsAffine X
-- Init.Data.SInt.Lemmas
Int16.toISize_ofNat : ∀ {n : ℕ}, n ≤ 32767 → (OfNat.ofNat n).toISize = OfNat.ofNat n
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
BoundarylessManifold.mk : ∀ {𝕜 : Type u_5} [inst : NontriviallyNormedField 𝕜] {E : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_8}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M], (∀ (x : M), I.IsInteriorPoint x) → BoundarylessManifold I M
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceSemanticTokensRangeParams : Lean.Lsp.FileSource Lean.Lsp.SemanticTokensRangeParams
-- Mathlib.Algebra.Order.Hom.Basic
/-- `SubadditiveHomClass F α β` states that `F` is a type of subadditive morphisms.  -/
SubadditiveHomClass : (F : Type u_7) →
  (α : outParam (Type u_8)) → (β : outParam (Type u_9)) → [Add α] → [Add β] → [LE β] → [FunLike F α β] → Prop
-- Aesop.Builder.Basic
Aesop.PhaseSpec.safe.sizeOf_spec : ∀ (info : Aesop.SafeRuleInfo), sizeOf (Aesop.PhaseSpec.safe info) = 1 + sizeOf info
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Limit.w_apply' : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F' : CategoryTheory.Functor J (Type v)} {j j' : J}
  {x : CategoryTheory.Limits.limit F'} (f : j ⟶ j'),
  (CategoryTheory.ConcreteCategory.hom (F'.map f))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j')) x
-- Aesop.Frontend.Extension
Aesop.Frontend.getGlobalRuleSetFromData : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      Aesop.RuleSetExtension → Lean.Meta.SimpExtension → Lean.Meta.Simp.SimprocExtension → m Aesop.GlobalRuleSet
-- Mathlib.Data.Set.Function
Set.SurjOn.image_eq_of_mapsTo : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.SurjOn f s t → Set.MapsTo f s t → f '' s = t