mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleDecl.mk.inj : ∀ {info : Lean.ConstantInfo} {kind : Lean.MetaM Lean.Lsp.CompletionItemKind}
  {tags : Lean.MetaM (Array Lean.Lsp.CompletionItemTag)} {info_1 : Lean.ConstantInfo}
  {kind_1 : Lean.MetaM Lean.Lsp.CompletionItemKind} {tags_1 : Lean.MetaM (Array Lean.Lsp.CompletionItemTag)},
  { info := info, kind := kind, tags := tags } = { info := info_1, kind := kind_1, tags := tags_1 } →
    info = info_1 ∧ kind = kind_1 ∧ tags = tags_1
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_arrow_comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory C F]
  (x : carrier X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.imageSubobject f).arrow)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.factorThruImageSubobject f)) x) =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations preserve natural scaling.  -/
AddCon.nsmul : ∀ {M : Type u_4} [inst : AddMonoid M] (c : AddCon M) (n : ℕ) {w x : M}, c w x → c (n • w) (n • x)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- The pushforward of presheaves of modules commutes with the forgetful functor
to presheaves of abelian groups.  -/
PresheafOfModules.pushforward₀CompToPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (R : CategoryTheory.Functor Dᵒᵖ RingCat) →
            (PresheafOfModules.pushforward₀ F R).comp (PresheafOfModules.toPresheaf (F.op.comp R)) ≅
              (PresheafOfModules.toPresheaf R).comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ Ab).obj F.op)
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_inverse_map_edge_op : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (c : C) (d : D),
  (CategoryTheory.Join.opEquiv C D).inverse.map (CategoryTheory.Join.edge (Opposite.op d) (Opposite.op c)) =
    Opposite.op (CategoryTheory.Join.edge c d)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_mono : ∀ {V : Type u} {G : SimpleGraph V} {H₁ H₂ : G.Subgraph}, H₁ ≤ H₂ → H₁.edgeSet ⊆ H₂.edgeSet
-- Mathlib.Data.Nat.Log
Nat.le_log_of_pow_le : ∀ {b x y : ℕ}, 1 < b → b ^ x ≤ y → x ≤ Nat.log b y
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
parallelepiped_orthonormalBasis_one_dim : ∀ {ι : Type u_1} [inst : Fintype ι] (b : OrthonormalBasis ι ℝ ℝ),
  parallelepiped ⇑b = Set.Icc 0 1 ∨ parallelepiped ⇑b = Set.Icc (-1) 0
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.mk.inj : ∀ {declName : Lean.Name} {levelParams : List Lean.Name} {type value : Lean.Expr} {recArgPos : ℕ}
  {declNames : Array Lean.Name} {fixedParamPerms : Lean.Elab.FixedParamPerms} {declName_1 : Lean.Name}
  {levelParams_1 : List Lean.Name} {type_1 value_1 : Lean.Expr} {recArgPos_1 : ℕ} {declNames_1 : Array Lean.Name}
  {fixedParamPerms_1 : Lean.Elab.FixedParamPerms},
  { declName := declName, levelParams := levelParams, type := type, value := value, recArgPos := recArgPos,
        declNames := declNames, fixedParamPerms := fixedParamPerms } =
      { declName := declName_1, levelParams := levelParams_1, type := type_1, value := value_1,
        recArgPos := recArgPos_1, declNames := declNames_1, fixedParamPerms := fixedParamPerms_1 } →
    declName = declName_1 ∧
      levelParams = levelParams_1 ∧
        type = type_1 ∧
          value = value_1 ∧ recArgPos = recArgPos_1 ∧ declNames = declNames_1 ∧ fixedParamPerms = fixedParamPerms_1
-- Mathlib.Order.Category.BddOrd
BddOrd.hom_ext : ∀ {X Y : BddOrd} {f g : X ⟶ Y}, BddOrd.Hom.hom f = BddOrd.Hom.hom g → f = g
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.compr₂.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : CommMonoid P] [inst_3 : CommMonoid Q] (f : M →* N →* P) (g : P →* Q),
  f.compr₂ g = (MonoidHom.compHom g).comp f
-- Mathlib.Data.Set.SymmDiff
Set.union_symmDiff_union_subset : ∀ {α : Type u} {s t u v : Set α}, symmDiff (s ∪ t) (u ∪ v) ⊆ symmDiff s u ∪ symmDiff t v
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inr_fst_f_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : K.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Lean.Elab.Calc
/-- Elaborator for the `calc` term mode variant.  -/
Lean.Elab.Term.elabCalc : Lean.Elab.Term.TermElab
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_refl : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A], ↑(ContinuousAlgEquiv.refl R A) = ContinuousAlgHom.id R A
-- Init.Data.Array.Basic
/-- Folds a function over an array from the left, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the array in order, using `f`.

The optional parameters `start` and `stop` control the region of the array to be folded. Folding
proceeds from `start` (inclusive) to `stop` (exclusive), so no folding occurs unless `start < stop`.
By default, the entire array is used.

Examples:
 * `#[a, b, c].foldl f z  = f (f (f z a) b) c`
 * `#[1, 2, 3].foldl (· ++ toString ·) "" = "123"`
 * `#[1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"`
 -/
Array.foldl : {α : Type u} → {β : Type v} → (β → α → β) → β → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → β
-- Mathlib.NumberTheory.LSeries.RiemannZeta
riemannZeta_def_of_ne_zero : ∀ {s : ℂ}, s ≠ 0 → riemannZeta s = completedRiemannZeta s / s.Gammaℝ
-- Mathlib.Algebra.Free
FreeSemigroup.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (head : α) (tail : List α),
  sizeOf { head := head, tail := tail } = 1 + sizeOf head + sizeOf tail
-- Mathlib.Algebra.Lie.Basic
/-- Lie module equivalences are reflexive.  -/
LieModuleEquiv.refl : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → M ≃ₗ⁅R,L⁆ M
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_eq_headD_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.minKeyD fallback = t.keys.headD fallback
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {f : α → β → γ} {k : α}, t.WF → (Std.TreeMap.Raw.map f t).getKey! k = t.getKey! k
-- Init.Grind.AC
/-- `superpose_ac_idempotent` for the non-commutative case. This is the "head"-case
 -/
Lean.Grind.AC.superpose_head_idempotent : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op}
  (x : Lean.Grind.AC.Var) (lhs₁ rhs₁ rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_head_idempotent_cert x lhs₁ rhs₁ rhs = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs
-- Mathlib.Geometry.Euclidean.Altitude
/-- The height of a vertex of a simplex is the distance between it and the foot of the altitude
from that vertex.  -/
Affine.Simplex.height : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Fin (n + 1) → ℝ
-- Mathlib.Tactic.NormNum.NatFactorial
/-- Evaluates the `Nat.factorial` function.  -/
Mathlib.Meta.NormNum.evalNatFactorial : Mathlib.Meta.NormNum.NormNumExt
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst : Int.Internal.Linear.Var →
  Lean.Meta.Grind.Arith.Cutsat.EqCnstr →
    Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.PresheafedSpace C)) →
      (∀ (i j : toGlueData.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (toGlueData.f i j)) →
        AlgebraicGeometry.PresheafedSpace.GlueData C
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend_exactAt : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') (j' : ι'),
  (∀ (j : ι), e.f j ≠ j') → (K.extend e).ExactAt j'
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_int_le : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R), ∃ n, ↑n ≤ x
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instHasColimit : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [∀ (n : ι), CategoryTheory.Limits.HasColimit (F.comp (HomologicalComplex.eval C c n))],
  CategoryTheory.Limits.HasColimit F
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rco.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rco α}, r.iter.toArray = r.toArray
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_rio : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ},
  Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi xs.toList
-- Lean.Environment
Lean.registerPersistentEnvExtensionUnsafe : {α β σ : Type} → [Inhabited σ] → Lean.PersistentEnvExtensionDescr α β σ → IO (Lean.PersistentEnvExtension α β σ)
-- Lean.KeyedDeclsAttribute
/-- Attribute description  -/
Lean.KeyedDeclsAttribute.Def.descr : {γ : Type} → Lean.KeyedDeclsAttribute.Def γ → String
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.algSpec_obj_hom : ∀ {R : CommRingCat} (X : (CommAlgCat ↑R)ᵒᵖ),
  ((AlgebraicGeometry.algSpec R).obj X).hom =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑(Opposite.unop X)))
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.testBit.match_1.eq_4 : ∀ (motive : PosNum → ℕ → Sort u_1) (p : PosNum) (n : ℕ) (h_1 : Unit → motive PosNum.one 0)
  (h_2 : (x : ℕ) → motive PosNum.one x) (h_3 : (a : PosNum) → motive a.bit0 0)
  (h_4 : (p : PosNum) → (n : ℕ) → motive p.bit0 n.succ) (h_5 : (a : PosNum) → motive a.bit1 0)
  (h_6 : (p : PosNum) → (n : ℕ) → motive p.bit1 n.succ),
  (match p.bit0, n.succ with
    | PosNum.one, 0 => h_1 ()
    | PosNum.one, x => h_2 x
    | a.bit0, 0 => h_3 a
    | p.bit0, n.succ => h_4 p n
    | a.bit1, 0 => h_5 a
    | p.bit1, n.succ => h_6 p n) =
    h_4 p n
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.monic_mul_leadingCoeff_inv : ∀ {K : Type u_1} [inst : DivisionRing K] {p : Polynomial K}, p ≠ 0 → (p * Polynomial.C p.leadingCoeff⁻¹).Monic
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The "free algebra" functor, sending a type `S` to the free algebra on `S`.  -/
AlgCat.free : (R : Type u) → [inst : CommRing R] → CategoryTheory.Functor (Type u) (AlgCat R)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.IsEffectiveEquivalenceRelation.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A},
  Nonempty (CategoryTheory.EffectiveEquivalenceRelation p₁ p₂) → CategoryTheory.IsEffectiveEquivalenceRelation p₁ p₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.degreeOf.eq_def : ∀ (m : Lean.Grind.CommRing.Mon) (x : Lean.Grind.CommRing.Var),
  m.degreeOf x =
    match m with
    | Lean.Grind.CommRing.Mon.unit => 0
    | Lean.Grind.CommRing.Mon.mult pw m => bif pw.x == x then pw.k else m.degreeOf x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- The restriction functor from sheaves of `R`-modules to sheaves of `R.over X`-modules
for some `X : D`.  -/
SheafOfModules.overFunctor : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      (R : CategoryTheory.Sheaf K RingCat) →
        (X : D) → CategoryTheory.Functor (SheafOfModules R) (SheafOfModules (R.over X))
-- Mathlib.RingTheory.Valuation.ValuationRing
/-- If `𝒪` satisfies `v.integers 𝒪` where `v` is a valuation on a field, then `𝒪`
is a valuation ring.  -/
ValuationRing.of_integers : ∀ {𝒪 : Type u} {K : Type v} {Γ : Type w} [inst : CommRing 𝒪] [inst_1 : Field K] [inst_2 : Algebra 𝒪 K]
  [inst_3 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (hh : v.Integers 𝒪), ValuationRing 𝒪
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int32.intCast : IntCast Int32
-- Mathlib.Data.Set.Image
Set.preimage_inr_image_inl : ∀ {α : Type u_1} {β : Type u_2} (s : Set α), Sum.inr ⁻¹' Sum.inl '' s = ∅
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (compare k km).isLE = true
-- Mathlib.Algebra.Ring.Defs
CommSemiring.toCommMonoid : {R : Type u} → [self : CommSemiring R] → CommMonoid R
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.hom_ext_iff : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {X : C} {f g : CategoryTheory.Limits.chosenCoend F ⟶ X},
  f = g ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j) g
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.instLE : {α : Type u_1} → LE (MeasurableSpace α)
-- Mathlib.CategoryTheory.Action.Basic
Action.res_map_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] (f : G →* H) {X Y : Action V H} (p : X ⟶ Y), ((Action.res V f).map p).hom = p.hom
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t₁ t₂ : Set β}, s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
/-- Extracts target vector from the tableau, putting auxiliary variables aside (see `stateLP`).  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.extractSolution : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType → Array ℚ
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield is closed under subtraction.  -/
Subfield.sub_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x y : K}, x ∈ s → y ∈ s → x - y ∈ s
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- the morphism between the "nondegenerate" `n`-simplices for all `n : ℕ`  -/
CategoryTheory.SimplicialObject.Split.Hom.f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S₁ S₂ : CategoryTheory.SimplicialObject.Split C} → S₁.Hom S₂ → (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.monObj_one : ∀ {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]
  {F : CategoryTheory.Functor C D} [inst_4 : F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.MonObj (F.obj X)],
  CategoryTheory.MonObj.one =
    hF.preimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.MonObj.one)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.prod_apply : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [inst : VAdd M α] [inst_1 : VAdd N γ]
  [inst_2 : VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ), ⇑(f.prod g) = fun x => (f x, g x)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_self_of_le_one : ∀ {x : NNReal} {z : ℝ}, x ≤ 1 → 1 ≤ z → x ^ z ≤ x
-- Mathlib.Order.Antichain
IsStrongAntichain.preimage : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsStrongAntichain r s →
    ∀ {f : β → α}, Function.Injective f → (∀ (a b : β), r' a b → r (f a) (f b)) → IsStrongAntichain r' (f ⁻¹' s)
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.mk_toNat_eq_card : ∀ {α : Type u} [inst : Fintype α], Cardinal.toNat (Cardinal.mk α) = Fintype.card α
-- Lean.Data.PrefixTree
/-- Returns the value of the longest key in `t` that is a prefix of `k`, if any.  -/
Lean.PrefixTreeNode.findLongestPrefix? : {α : Type u_1} → {β : Type u_2} → (cmp : α → α → Ordering) → Lean.PrefixTreeNode α β cmp → List α → Option β
-- Mathlib.Algebra.Star.Conjneg
conjneg_surjective : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R],
  Function.Surjective conjneg
-- Mathlib.Data.PFun
/-- Product of partial functions.  -/
PFun.prodMap : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → (α →. γ) → (β →. δ) → α × β →. γ × δ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multicospanShape_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (j : E.I₁'),
  E.multicospanShape.snd j = j.fst.2
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_fst_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : q + 1 = p),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q ⋯)
      ((↑(CochainComplex.mappingCone.fst φ)).v q p hpq) =
    CategoryTheory.CategoryStruct.id (F.X p)
-- Lean.Structure
Lean.StructureResolutionOrderResult.mk.injEq : ∀ (resolutionOrder : Array Lean.Name) (conflicts : Array Lean.StructureResolutionOrderConflict)
  (resolutionOrder_1 : Array Lean.Name) (conflicts_1 : Array Lean.StructureResolutionOrderConflict),
  ({ resolutionOrder := resolutionOrder, conflicts := conflicts } =
      { resolutionOrder := resolutionOrder_1, conflicts := conflicts_1 }) =
    (resolutionOrder = resolutionOrder_1 ∧ conflicts = conflicts_1)
-- Mathlib.Algebra.Module.LocalizedModule.Exact
/-- Localization of modules is an exact functor, proven here for `LocalizedModule`.
See `IsLocalizedModule.map_exact` for the more general version.  -/
LocalizedModule.map_exact : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M₀ : Type u_2} [inst_1 : AddCommMonoid M₀]
  [inst_2 : Module R M₀] {M₁ : Type u_3} [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] {M₂ : Type u_4}
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂),
  Function.Exact ⇑g ⇑h →
    Function.Exact ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g)
      ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₁) (LocalizedModule.mkLinearMap S M₂)) h)
-- Std.Http.Data.Body.Any
Std.Http.Body.Any.mk.inj : ∀ {recv : Std.Async.Async (Option Std.Http.Chunk)} {close : Std.Async.Async Unit} {isClosed : Std.Async.Async Bool}
  {recvSelector : Std.Async.Selector (Option Std.Http.Chunk)}
  {tryRecv : Std.Async.Async (Option (Option Std.Http.Chunk))}
  {getKnownSize : Std.Async.Async (Option Std.Http.Body.Length)}
  {setKnownSize : Option Std.Http.Body.Length → Std.Async.Async Unit} {recv_1 : Std.Async.Async (Option Std.Http.Chunk)}
  {close_1 : Std.Async.Async Unit} {isClosed_1 : Std.Async.Async Bool}
  {recvSelector_1 : Std.Async.Selector (Option Std.Http.Chunk)}
  {tryRecv_1 : Std.Async.Async (Option (Option Std.Http.Chunk))}
  {getKnownSize_1 : Std.Async.Async (Option Std.Http.Body.Length)}
  {setKnownSize_1 : Option Std.Http.Body.Length → Std.Async.Async Unit},
  { recv := recv, close := close, isClosed := isClosed, recvSelector := recvSelector, tryRecv := tryRecv,
        getKnownSize := getKnownSize, setKnownSize := setKnownSize } =
      { recv := recv_1, close := close_1, isClosed := isClosed_1, recvSelector := recvSelector_1, tryRecv := tryRecv_1,
        getKnownSize := getKnownSize_1, setKnownSize := setKnownSize_1 } →
    recv = recv_1 ∧
      close = close_1 ∧
        isClosed = isClosed_1 ∧
          recvSelector = recvSelector_1 ∧
            tryRecv = tryRecv_1 ∧ getKnownSize = getKnownSize_1 ∧ setKnownSize = setKnownSize_1
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableAt.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {f₂ : E → G},
  DifferentiableAt 𝕜 f₁ x → DifferentiableAt 𝕜 f₂ x → DifferentiableAt 𝕜 (fun x => (f₁ x, f₂ x)) x
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_eq_headD_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
    ∀ {fallback : α}, Std.Internal.List.minKeyD l fallback = (Std.Internal.List.keys l).headD fallback
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_cons_nil : ∀ {α : Type u_1} (x : α) (s : Stream'.Seq α), dist (Stream'.Seq.cons x s) Stream'.Seq.nil = 1
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
disjoint_measurableAtom_of_notMem : ∀ {β : Type u_2} [inst : MeasurableSpace β] {x y : β},
  x ∉ measurableAtom y → Disjoint (measurableAtom x) (measurableAtom y)
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.instCoalgebraStruct : {R : Type u_1} →
  {n : Type u_2} →
    [inst : CommSemiring R] →
      [Fintype n] →
        [DecidableEq n] →
          {A : n → Type u_3} →
            [inst_3 : (i : n) → AddCommMonoid (A i)] →
              [inst_4 : (i : n) → Module R (A i)] →
                [(i : n) → CoalgebraStruct R (A i)] → CoalgebraStruct R ((i : n) → A i)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mem_toOpens : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U : OpenAddSubgroup G} {g : G}, g ∈ ↑U ↔ g ∈ U
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- The topological space structure on `Snowflaking X α _ _` is induced from the original space.  -/
Metric.Snowflaking.instTopologicalSpace : {X : Type u_1} →
  {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [TopologicalSpace X] → TopologicalSpace (Metric.Snowflaking X α hα₀ hα₁)
-- Init.Data.Vector.Lemmas
Vector.forall_mem_singleton : ∀ {α : Type u_1} {p : α → Prop} {a : α}, (∀ x ∈ #v[a], p x) ↔ p a