mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Basic
Matrix.piAddEquiv_symm_apply : ∀ {m : Type u_2} {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} [inst : (i : ι) → Add (β i)]
  (f : (i : ι) → Matrix m n (β i)), Matrix.piAddEquiv.symm f = Matrix.of fun j k i => f i j k
-- Mathlib.AlgebraicGeometry.Spec
/-- The induced map of a ring homomorphism on the ring spectra, as a morphism of topological spaces.
 -/
AlgebraicGeometry.Spec.topMap : {R S : CommRingCat} → (R ⟶ S) → (AlgebraicGeometry.Spec.topObj S ⟶ AlgebraicGeometry.Spec.topObj R)
-- Mathlib.Data.Fin.Fin2
Fin2.toFin_fz : ∀ (n : ℕ), Fin2.fz.toFin = 0
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 409 status code.
 -/
Std.Http.Response.conflict : Std.Http.Response.Builder
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- `ℝ≥0∞` is `MeasurableEquiv` to `ℝ≥0 ⊕ Unit`.  -/
ENNReal.ennrealEquivSum : ENNReal ≃ᵐ NNReal ⊕ Unit
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_lt_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {a : α} [Nonempty ι] {f : ι → α},
  BddBelow (Set.range f) → (iInf f < a ↔ ∃ i, f i < a)
-- Mathlib.Data.Multiset.Bind
Multiset.nodup_bind : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → Multiset β},
  (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Multiset.Pairwise (Function.onFun Disjoint f) s
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_ne_zero`. -/
Ideal.ramificationIdx_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  {e : ℕ},
  e ≠ 0 → Ideal.map (algebraMap R S) p ≤ P ^ e → ¬Ideal.map (algebraMap R S) p ≤ P ^ (e + 1) → p.ramificationIdx' P ≠ 0
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.map.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (c d : AddCon M) (h : c ≤ d), c.map d h = c.lift d.mk' ⋯
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.motivePos : Lean.Meta.ElimInfo → ℕ
-- Mathlib.Order.Filter.Cofinite
Set.Finite.cofinite_inf_principal_sdiff : ∀ {α : Type u_2} {s t : Set α},
  t.Finite → Filter.cofinite ⊓ Filter.principal (s \ t) = Filter.cofinite ⊓ Filter.principal s
-- Mathlib.RepresentationTheory.Character
/-- The character is multiplicative under the tensor product.  -/
FDRep.char_tensor : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Monoid G] (V W : FDRep k G),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).character = V.character * W.character
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_map_erase : ∀ {α : Type u_2} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq α] (f : α → M) {a : α} {l : List α},
  a ∈ l → f a * (List.map f (l.erase a)).prod = (List.map f l).prod
-- Mathlib.Topology.Order.OrderClosed
PredOrder.nhdsGT_eq_nhdsNE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] [PredOrder α] (a : α),
  nhdsWithin a (Set.Ioi a) = nhdsWithin a {a}ᶜ
-- Mathlib.Topology.UniformSpace.Basic
nhds_eq_uniformity_prod : ∀ {α : Type ua} [inst : UniformSpace α] {a b : α},
  nhds (a, b) = (uniformity α).lift' fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}
-- Init.Data.Range.Polymorphic.Iterators
Std.Rii.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α] (x : Std.Rii α),
  Std.Rii.Internal.iter x = { internalState := { next := Std.PRange.least? } }
-- Mathlib.Data.FunLike.Group
FunLike.coeAddMonoidHom_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], Function.Injective ⇑(FunLike.coeAddMonoidHom F α β)
-- Lean.Elab.DefView
Lean.Elab.Command.mkDefViewOfTheorem : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.DefView
-- Mathlib.Tactic.ComputeDegree
/-- `dispatchLemma twoH` takes its input `twoH` from the output of `twoHeadsArgs`.

Using the information contained in `twoH`, it decides which lemma is the most appropriate.

`dispatchLemma` is essentially the main dictionary for `compute_degree`.
 -/
Mathlib.Tactic.ComputeDegree.dispatchLemma : Lean.Name × Lean.Name × (Lean.Name ⊕ Lean.Name) × List Bool → optParam Bool false → Lean.Name
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instLeftCancelMonoid : {α : Type u_1} → [RightCancelMonoid α] → LeftCancelMonoid αᵐᵒᵖ
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `modify` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.constModify : ∀ {α : Type u} [inst : Ord α] {x : Type v} {t : Std.DTreeMap.Internal.Impl α fun x_1 => x} {k : α} {f : x → x},
  t.WF → (Std.DTreeMap.Internal.Impl.Const.modify k f t).WF
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → ∀ {h : k' ∈ Std.ExtDHashMap.ofList l}, (Std.ExtDHashMap.ofList l).getKey k' h = k
-- Mathlib.RingTheory.Smooth.NoetherianDescent
/-- (Implementation detail): The finite type `R`-algebra.  -/
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.subalgebra : (R : Type u_1) →
  [inst : CommRing R] →
    {A : Type u} →
      {B : Type u_2} →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] →
            [inst_3 : CommRing B] → [inst_4 : Algebra A B] → Algebra.Smooth.DescentAux✝ A B → Subalgebra R A
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesFiniteLimitsEvalOfHasFiniteLimits : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] (n : ι),
  CategoryTheory.Limits.PreservesFiniteLimits (HomologicalComplex.eval C c n)
-- Init.Data.Ord.Basic
/-- Checks whether the ordering is `gt`.
 -/
Ordering.isGT : Ordering → Bool
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_const_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {w : ι → ℝ} (a : 𝕜) (f : ι → 𝕜),
  ⟪Function.const ι a, f⟫_[𝕜, w] = (∑ i, w i • f i) * (starRingEnd 𝕜) a
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_add_cancel_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b : α}, a ≤ b → b - a + a = b
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.instCoeFunPreZeroHypercoverFamilyForallForallPreZeroHypercoverProp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CoeFun (CategoryTheory.PreZeroHypercoverFamily C) fun x => ⦃X : C⦄ → CategoryTheory.PreZeroHypercover X → Prop
-- Batteries.Recycling.RBTree.Lemmas
/-- The value `y` returned by `upperBound? x` is greater or equal to `x`.  -/
RBTree.RBSet.upperBound?_ge : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp},
  t.upperBound? x = some y → cmp x y ≠ Ordering.gt
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- This is an equivalent condition to be a sheaf, which is useful for the abstraction to local
operators on elementary toposes. However this definition is defined only for sieves, not presieves.
The equivalence between this and `IsSheafFor` is given in `isSheafFor_iff_yonedaSheafCondition`.
This version is also useful to establish that being a sheaf is preserved under isomorphism of
presheaves.

See the discussion before Equation (3) of [MM92], Chapter III, Section 4. See also C2.1.4 of
[Elephant].  -/
CategoryTheory.Presieve.YonedaSheafCondition : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Functor Cᵒᵖ (Type v₁) → CategoryTheory.Sieve X → Prop
-- Mathlib.Data.Prod.Lex
/-- Dictionary / lexicographic ordering on pairs.  -/
Prod.Lex.instLE : (α : Type u_3) → (β : Type u_4) → [LT α] → [LE β] → LE (Lex (α × β))
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.left_pos : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < p
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods.toMethodsRefImpl : Lean.Meta.Sym.DSimp.Methods → Lean.Meta.Sym.DSimp.MethodsRef
-- Init.System.IO
/-- Returns the contents of a UTF-8-encoded text file as an array of lines.

Newline markers are not included in the lines.
 -/
IO.FS.lines : System.FilePath → IO (Array String)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairRight_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E')
  (X : D),
  (CategoryTheory.Join.mapPairRight Fₗ Fᵣ).inv.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (Fᵣ.obj X))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertIfNew.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → ∀ (b b_1 : β), b = b_1 → t.insertIfNew a b = t_1.insertIfNew a_1 b_1
-- Mathlib.Topology.UnitInterval
unitInterval.symm_lt_symm : ∀ {i j : ↑unitInterval}, unitInterval.symm i < unitInterval.symm j ↔ j < i
-- Mathlib.Data.DFinsupp.Encodable
instEncodableDFinsuppOfDecidableNeOfNat : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [Encodable ι] →
        [(i : ι) → Encodable (α i)] → [(i : ι) → (x : α i) → Decidable (x ≠ 0)] → Encodable (Π₀ (i : ι), α i)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Assuming that `(C, J)` is a dense subsite of `(D, K)` (via a functor `G : C ⥤ D`)
and `sheafPushforwardContinuous G A J K` is an equivalence of categories, and
that `HasWeakSheafify J A` holds, then this adjunction shows the existence
of a left adjoint to `sheafToPresheaf K A`.  -/
CategoryTheory.Functor.IsDenseSubsite.sheafifyAdjunctionOfIsEquivalence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (J : CategoryTheory.GrothendieckTopology C) →
          (K : CategoryTheory.GrothendieckTopology D) →
            (G : CategoryTheory.Functor C D) →
              (A : Type u_4) →
                [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                    [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence] →
                      [inst_5 : CategoryTheory.HasWeakSheafify J A] →
                        CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A ⊣
                          CategoryTheory.sheafToPresheaf K A
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instZero : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Zero (AdicCompletion.AdicCauchySequence I M)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.mk.injEq : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] (X : D) [mod : CategoryTheory.ModObj A X] (X_1 : D)
  (mod_1 : CategoryTheory.ModObj A X_1), ({ X := X, mod := mod } = { X := X_1, mod := mod_1 }) = (X = X_1 ∧ mod ≍ mod_1)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSubtype.match_1.eq_1 : ∀ (n : ℕ) (P : Fin (n + 1) → Prop) (inst : DecidablePred P)
  (motive : Fin (Fin.countP fun x => decide (P x.succ)) → Sort u_1) (k : ℕ)
  (hk : k < Fin.countP fun x => decide (P x.succ))
  (h_1 : (k : ℕ) → (hk : k < Fin.countP fun x => decide (P x.succ)) → motive ⟨k, hk⟩),
  (match ⟨k, hk⟩ with
    | ⟨k, hk⟩ => h_1 k hk) =
    h_1 k hk
-- Mathlib.Order.Fin.Basic
/-- `Fin.succ` as an `OrderEmbedding`  -/
Fin.succOrderEmb : (n : ℕ) → Fin n ↪o Fin (n + 1)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_add_sublist : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : FreeAddGroup α), (x + y).toWord.Sublist (x.toWord ++ y.toWord)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.coe_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ↑⊥ = Set.range ⇑(algebraMap R A)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The actual `AddSubgroup` obtained from an element of a
`AddSubgroupClass`  -/
AddSubgroup.ofClass : {S : Type u_3} →
  {G : Type u_4} → [inst : AddGroup G] → [inst_1 : SetLike S G] → [AddSubgroupClass S G] → S → AddSubgroup G
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.instSetLike : {G : Type u_1} → [inst : AddGroup G] → SetLike (AddSubgroup G) G
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {V W : HopfAlgCat R} {x y : V.Hom W}, x.toBialgHom' = y.toBialgHom' → x = y
-- Mathlib.Analysis.InnerProductSpace.Laplacian
InnerProductSpace.instLaplacian : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [FiniteDimensional ℝ E] →
        {F : Type u_3} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → Laplacian (E → F) (E → F)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumRingEquiv_C : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (r : R),
  (MvPolynomial.sumRingEquiv R S₁ S₂) (MvPolynomial.C r) = MvPolynomial.C (MvPolynomial.C r)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_pow : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M] (m : M) (r : R) (n : ℕ),
  AddMonoidAlgebra.single m r ^ n = AddMonoidAlgebra.single (n • m) (r ^ n)
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withTopCongr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (e : α ≃o β),
  e.withTopCongr =
    { toFun := WithTop.map ⇑e, invFun := e.withTopCongr.invFun, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Topology.Instances.ENNReal.Lemmas
continuous_of_le_add_edist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : α → ENNReal} (C : ENNReal),
  C ≠ ⊤ → (∀ (x y : α), f x ≤ f y + C * edist x y) → Continuous f
-- Mathlib.Order.CompleteLattice.Basic
iInf_psigma : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_8} {κ : ι → Sort u_9} (f : (i : ι) ×' κ i → α),
  ⨅ ij, f ij = ⨅ i, ⨅ j, f ⟨i, j⟩
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ γ_1 : CochainComplex.HomComplex.Cochain K L n),
  γ = γ_1 →
    ∀ (a n' : ℤ) (hn' : n + a = n') (T : CochainComplex.HomComplex.Triplet n'),
      γ.leftShift a n' hn' T = γ_1.leftShift a n' hn' T
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.fac : ∀ {V : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  (s : CategoryTheory.Limits.Cone (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.lift s)
      ((CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom V F₁ F₂).π.app j) =
    s.π.app j
-- Mathlib.Order.CompleteBooleanAlgebra
Prop.instCompleteBooleanAlgebra : CompleteBooleanAlgebra Prop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} [inst_3 : Inhabited (β k)] {v : β k}, (m.insert k v).get! k = v
-- Mathlib.Topology.MetricSpace.Kuratowski
/-- When the reference set is dense, the embedding map is an isometry on its image.  -/
KuratowskiEmbedding.embeddingOfSubset_isometry : ∀ {α : Type u} [inst : MetricSpace α] (x : ℕ → α), DenseRange x → Isometry (KuratowskiEmbedding.embeddingOfSubset x)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instFaithfulModulesSpecSheafModuleCatCarrierCarrierCommRingCatModulesSpecToSheaf : ∀ {R : CommRingCat}, AlgebraicGeometry.modulesSpecToSheaf.Faithful
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
PresheafOfModules.instIsRightAdjointPushforward : ∀ {C D : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R), (PresheafOfModules.pushforward φ).IsRightAdjoint
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.proved : Array Aesop.RappRef → Aesop.SafeRulesResult
-- Std.Http.Test.Helpers
_private.Std.Http.Test.Helpers.0.Std.Http.Internal.Test.withTimeout.loop : {α : Type} → String → ℕ → Task (Except IO.Error α) → ℕ → IO α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α},
  m.contains a = false → Std.ExtDHashMap.Const.get! m a = default
-- Lean.Elab.Tactic.Try
/-- `evalSuggest` for `try` tactic.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestTry : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafAddGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (G : Type u)
  [inst_9 : TopologicalSpace G] [inst_10 : ChartedSpace H G] [inst_11 : AddGroup G] [inst_12 : LieAddGroup I (↑⊤) G],
  smoothSheafAddGroup IM I M G = { obj := smoothPresheafAddGroup IM I M G, property := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflects_colimits_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  Subsingleton (CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
-- Mathlib.Geometry.Euclidean.Altitude
/-- An altitude of a simplex is the line that passes through a vertex
and is orthogonal to the opposite face.  -/
Affine.Simplex.altitude : {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 : ℕ} → Affine.Simplex ℝ P n → Fin (n + 1) → AffineSubspace ℝ P
-- Mathlib.Data.Nat.Nth
Nat.exists_lt_card_nth_eq : ∀ {p : ℕ → Prop} {x : ℕ}, p x → ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) ∧ Nat.nth p n = x
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_ne_top_of_ne_zero : ∀ {x : ENNReal} {y : ℝ}, x ≠ 0 → x ≠ ⊤ → x ^ y ≠ ⊤
-- Mathlib.Analysis.Convex.Function
/-- A function `-f` is convex iff `f` is concave.  -/
neg_convexOn_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f : E → β}, ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.add_add_tsub_cancel : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable c → c ≤ b → a + c + (b - c) = a + b
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSliceData.mk : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Roo α → Std.DTreeMap.Internal.Const.RooSliceData α β
-- Init.Grind.Lemmas
Lean.Grind.Nat.shiftLeft_congr : ∀ {a b k₁ k₂ k : ℕ}, a = k₁ → b = k₂ → (k == k₁ <<< k₂) = true → a <<< b = k
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.isAdmissible_iff_pairwise_and_le : ∀ {m : ℕ} {L : List ℕ},
  SimplexCategoryGenRel.IsAdmissible m L ↔
    List.Pairwise (fun x1 x2 => x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k
-- Mathlib.Data.Multiset.Bind
Multiset.map_join : ∀ {α : Type u_1} {β : Type v} (f : α → β) (S : Multiset (Multiset α)),
  Multiset.map f S.join = (Multiset.map (Multiset.map f) S).join
-- Mathlib.Analysis.Normed.Module.Bases
/-- The operators `succSub P i` satisfy a biorthogonality relation.  -/
SchauderBasis.succSub_ortho : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {P : ℕ → X →L[𝕜] X},
  (∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x) →
    ∀ (i j : ℕ) (x : X),
      (SchauderBasis.succSub P i) ((SchauderBasis.succSub P j) x) = if i = j then (SchauderBasis.succSub P j) x else 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateReset! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → ℕ → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Std.Http.Data.Method
/-- Perform a safe query with a request body.
Source: https://www.ietf.org/archive/id/draft-ietf-httpbis-safe-method-w-body-14.html#section-2
 -/
Std.Http.Method.query : Std.Http.Method
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of the `n`th power of a field element `x` (with `n : ℕ`)
is `n` times the logarithmic height of `x`.  -/
Height.logHeight₁_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K) (n : ℕ),
  Height.logHeight₁ (x ^ n) = ↑n * Height.logHeight₁ x
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_foldlM_loop : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → β → α → m β) (xs : Array α) (stop : ℕ)
  (h : stop ≤ xs.size) (i j : ℕ) (b : β),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.foldlM.loop (f x) xs stop h i j b
-- Mathlib.Order.RelClasses
instTrichotomousGt : ∀ {α : Type u} [inst : LinearOrder α], Std.Trichotomous fun x1 x2 => x2 < x1
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic.0.Std.Tactic.BVDecide.Gate.toString.match_1.eq_3 : ∀ (motive : Std.Tactic.BVDecide.Gate → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.Gate.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.Gate.xor) (h_3 : Unit → motive Std.Tactic.BVDecide.Gate.beq)
  (h_4 : Unit → motive Std.Tactic.BVDecide.Gate.or),
  (match Std.Tactic.BVDecide.Gate.beq with
    | Std.Tactic.BVDecide.Gate.and => h_1 ()
    | Std.Tactic.BVDecide.Gate.xor => h_2 ()
    | Std.Tactic.BVDecide.Gate.beq => h_3 ()
    | Std.Tactic.BVDecide.Gate.or => h_4 ()) =
    h_3 ()