mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Basis.Prod
/-- A distinguished basis carried by `LieAlgebra.Basis.prod`.  -/
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.basisProd : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {R : Type u_5} →
                    [inst_4 : CommRing R] →
                      [inst_5 : LieAlgebra R L₁] →
                        {H₁ : LieSubalgebra R L₁} →
                          (b₁ : LieAlgebra.Basis ι₁ H₁) →
                            [inst_6 : LieAlgebra R L₂] →
                              {H₂ : LieSubalgebra R L₂} →
                                (b₂ : LieAlgebra.Basis ι₂ H₂) →
                                  (Matrix.reindex eι eι) b₁.A = b₂.A →
                                    LieAlgebra.Basis ι₁ (LieAlgebra.Basis.prodCartan✝ eι b₁ b₂)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : β → β},
      (Std.DHashMap.Internal.Raw₀.Const.modify m k f).getKey? k = if m.contains k = true then some k else none
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_zero : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H), groupHomology.chainsMap f 0 = 0
-- Mathlib.Combinatorics.Graph.Maps
Graph.map_map : ∀ {α : Type u_1} {α' : Type u_2} {α'' : Type u_3} {β : Type u_4} {G : Graph α β} (f : α → α') (f' : α' → α''),
  Graph.map f' (Graph.map f G) = Graph.map (f' ∘ f) G
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The unit for the left Kan extension `f⁺ g`.  -/
CategoryTheory.Bicategory.lanUnit : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : a ⟶ c) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
            g ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Bicategory.lan f g)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_le_norm_of_ae_le : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : ↥(MeasureTheory.Lp E p μ)}
  {g : ↥(MeasureTheory.Lp F p μ)}, (∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖) → ‖f‖ ≤ ‖g‖
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.coeFn_sup : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : Lattice E] [inst_2 : HasSolidNorm E] [inst_3 : IsOrderedAddMonoid E]
  (f g : ↥(MeasureTheory.Lp E p μ)), ↑↑(f ⊔ g) =ᵐ[μ] ↑↑f ⊔ ↑↑g
-- Std.Internal.Do.Order.Basic
Lean.Order.iSup_prop_eq_exists : ∀ {ι : Type u} (f : ι → Prop), Lean.Order.iSup f = ∃ i, f i
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Balanced C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  S₁.ShortExact → S₂.ShortExact → CategoryTheory.IsIso φ.τ₁ → CategoryTheory.IsIso φ.τ₃ → CategoryTheory.IsIso φ.τ₂
-- Std.Data.TreeSet.Raw.Basic
/-- Tree sets without a bundled well-formedness invariant, suitable for use in nested
inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt, prefer `TreeSet`
over `TreeSet.Raw`. Lemmas about the operations on `Std.TreeSet.Raw` are available in the
module `Std.Data.TreeSet.Raw.Lemmas`.

A tree set stores elements of a certain type in a certain order. It depends on a comparator function
that defines an ordering on the keys and provides efficient order-dependent queries, such as
retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
certain laws that ensure a consistent ordering:

* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
and vice versa (see the `OrientedCmp` typeclass).
* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
is less than or equal to `c` (see the `TransCmp` typeclass).

Keys for which `cmp a b = Ordering.eq` are considered the same, i.e only one of them
can be contained in a single tree set at the same time.

To avoid expensive copies, users should make sure that the tree set is used linearly.

Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary
search tree with efficient order statistic lookups.
 -/
Std.TreeSet.Raw : (α : Type u) → autoParam (α → α → Ordering) Std.TreeSet.Raw._auto_1 → Type u
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.mk : {X Y : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} →
        (map : X ⟶ Y) →
          autoParam (CategoryTheory.CategoryStruct.comp A.ι map = CategoryTheory.CategoryStruct.comp φ B.ι)
              SSet.RelativeMorphism.comm._autoParam →
            SSet.RelativeMorphism A B φ
-- Mathlib.Algebra.BigOperators.Fin
List.sum_ofFn : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} {f : Fin n → M}, (List.ofFn f).sum = ∑ i, f i
-- Mathlib.Algebra.Homology.Bifunctor
/-- The second differential on `mapBifunctor K₁ K₂ F c`  -/
HomologicalComplex.mapBifunctor.D₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            (K₁ : HomologicalComplex C₁ c₁) →
                              (K₂ : HomologicalComplex C₂ c₂) →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [inst_9 : K₁.HasMapBifunctor K₂ F c] →
                                            [inst_10 : DecidableEq J] →
                                              (j j' : J) → (K₁.mapBifunctor K₂ F c).X j ⟶ (K₁.mapBifunctor K₂ F c).X j'
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.LHom.substructureReduct.congr_simp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {L' : FirstOrder.Language} [inst_1 : L'.Structure M]
  (φ φ_1 : L →ᴸ L') (e_φ : φ = φ_1) [inst_2 : φ.IsExpansionOn M], φ.substructureReduct = φ_1.substructureReduct
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_def : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin n → M), ∑ i, f i = (List.map f (List.finRange n)).sum
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiable.mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M},
  MDiff f → MDiff[s] f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.length_toList : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.toList.length = t.size
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.inhabited : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → Inhabited (ContMDiffSection I F n V)
-- Mathlib.Algebra.CharP.Algebra
/-- If `R →+* A` is injective, and `A` is of exponential characteristic `p`, then `R` is also of
exponential characteristic `p`. Similar to `RingHom.charZero`.  -/
RingHom.expChar : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] (f : R →+* A),
  Function.Injective ⇑f → ∀ (p : ℕ) [ExpChar A p], ExpChar R p
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.lineCount_eq_pointCount : ∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.ProjectivePlane P L] [Finite P] [Finite L]
  (p : P) (l : L), Configuration.lineCount L p = Configuration.pointCount P l
-- Mathlib.Topology.MetricSpace.Infsep
Set.subsingleton_of_einfsep_eq_top : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α}, s.einfsep = ⊤ → s.Subsingleton
-- Mathlib.CategoryTheory.Localization.Pi
/-- If `L : C ⥤ D` is a localization functor for `W : MorphismProperty C`, then
the induced functor `(Discrete J ⥤ C) ⥤ (Discrete J ⥤ D)` is also a localization
for `W.functorCategory (Discrete J)` if `W` contains identities.  -/
CategoryTheory.Functor.IsLocalization.instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities : ∀ {J : Type} [Finite J] {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [W.ContainsIdentities] [L.IsLocalization W],
  ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Discrete J) C D).obj L).IsLocalization
    (W.functorCategory (CategoryTheory.Discrete J))
-- Lean.Meta.Closure
Lean.Meta.Closure.State.newLocalDecls : Lean.Meta.Closure.State → Array Lean.LocalDecl
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instDistribMulAction : {S : Type u_1} →
  {R : Type u_3} →
    {c₁ c₂ c₃ : R} →
      [inst : Semiring S] →
        [inst_1 : AddCommGroup R] → [DistribMulAction S R] → DistribMulAction S (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace : ∀ (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i j k : D.J),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k))
    AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.coconeQuotientDiagDesc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {V U : OpenSubgroup (CategoryTheory.Aut F)} →
            (h : (↑U).Normal) →
              {A : C} →
                (u :
                    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
                      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
                        (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U))) →
                  (hUinV : U ≤ V) →
                    (s :
                        CategoryTheory.Limits.Cocone
                          ((CategoryTheory.PreGaloisCategory.quotientDiag✝ V h u).comp
                            (CategoryTheory.PreGaloisCategory.functorToAction F))) →
                      (CategoryTheory.PreGaloisCategory.coconeQuotientDiag✝ h u hUinV).pt ⟶ s.pt
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_eq_bot : ∀ {M : Type u_2} [inst : Mul M] {S : Subsemigroup M}, S.op = ⊥ ↔ S = ⊥
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v, u₁} C} {J : Type v} {U : J → C} {V : J × J → C}
  {f : (i j : J) → V (i, j) ⟶ U i}
  {f_mono : autoParam (∀ (i j : J), CategoryTheory.Mono (f i j)) CategoryTheory.GlueData.f_mono._autoParam}
  {f_hasPullback :
    autoParam (∀ (i j k : J), CategoryTheory.Limits.HasPullback (f i j) (f i k))
      CategoryTheory.GlueData.f_hasPullback._autoParam}
  {f_id : autoParam (∀ (i : J), CategoryTheory.IsIso (f i i)) CategoryTheory.GlueData.f_id._autoParam}
  {t : (i j : J) → V (i, j) ⟶ V (j, i)} {t_id : ∀ (i : J), t i i = CategoryTheory.CategoryStruct.id (V (i, i))}
  {t' : (i j k : J) → CategoryTheory.Limits.pullback (f i j) (f i k) ⟶ CategoryTheory.Limits.pullback (f j k) (f j i)}
  {t_fac :
    ∀ (i j k : J),
      CategoryTheory.CategoryStruct.comp (t' i j k) (CategoryTheory.Limits.pullback.snd (f j k) (f j i)) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f i j) (f i k)) (t i j)}
  {cocycle :
    ∀ (i j k : J),
      CategoryTheory.CategoryStruct.comp (t' i j k) (CategoryTheory.CategoryStruct.comp (t' j k i) (t' k i j)) =
        CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f i j) (f i k))}
  {J_1 : Type v} {U_1 : J_1 → C} {V_1 : J_1 × J_1 → C} {f_1 : (i j : J_1) → V_1 (i, j) ⟶ U_1 i}
  {f_mono_1 : autoParam (∀ (i j : J_1), CategoryTheory.Mono (f_1 i j)) CategoryTheory.GlueData.f_mono._autoParam}
  {f_hasPullback_1 :
    autoParam (∀ (i j k : J_1), CategoryTheory.Limits.HasPullback (f_1 i j) (f_1 i k))
      CategoryTheory.GlueData.f_hasPullback._autoParam}
  {f_id_1 : autoParam (∀ (i : J_1), CategoryTheory.IsIso (f_1 i i)) CategoryTheory.GlueData.f_id._autoParam}
  {t_1 : (i j : J_1) → V_1 (i, j) ⟶ V_1 (j, i)}
  {t_id_1 : ∀ (i : J_1), t_1 i i = CategoryTheory.CategoryStruct.id (V_1 (i, i))}
  {t'_1 :
    (i j k : J_1) →
      CategoryTheory.Limits.pullback (f_1 i j) (f_1 i k) ⟶ CategoryTheory.Limits.pullback (f_1 j k) (f_1 j i)}
  {t_fac_1 :
    ∀ (i j k : J_1),
      CategoryTheory.CategoryStruct.comp (t'_1 i j k) (CategoryTheory.Limits.pullback.snd (f_1 j k) (f_1 j i)) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f_1 i j) (f_1 i k)) (t_1 i j)}
  {cocycle_1 :
    ∀ (i j k : J_1),
      CategoryTheory.CategoryStruct.comp (t'_1 i j k) (CategoryTheory.CategoryStruct.comp (t'_1 j k i) (t'_1 k i j)) =
        CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f_1 i j) (f_1 i k))},
  { J := J, U := U, V := V, f := f, f_mono := f_mono, f_hasPullback := f_hasPullback, f_id := f_id, t := t,
        t_id := t_id, t' := t', t_fac := t_fac, cocycle := cocycle } =
      { J := J_1, U := U_1, V := V_1, f := f_1, f_mono := f_mono_1, f_hasPullback := f_hasPullback_1, f_id := f_id_1,
        t := t_1, t_id := t_id_1, t' := t'_1, t_fac := t_fac_1, cocycle := cocycle_1 } →
    J = J_1 ∧ U ≍ U_1 ∧ V ≍ V_1 ∧ f ≍ f_1 ∧ t ≍ t_1 ∧ t' ≍ t'_1
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_disjoint_iUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [Countable β] {v : MeasureTheory.VectorMeasure α M} {f : β → Set α} [T2Space M],
  (∀ (i : β), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → v (⋃ i, f i) = ∑' (i : β), v (f i)
-- Init.Data.Array.Lemmas
Array.append_right_inj : ∀ {α : Type u_1} {ys₁ ys₂ : Array α} (xs : Array α), xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Decomp.0.SimpleGraph.Walk.length.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2) (v v_1 : V) (h : G.Adj u v_1)
  (q : G.Walk v_1 v) (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_2 : V) → (h : G.Adj u v_2) → (q : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons h q)),
  (match v, SimpleGraph.Walk.cons h q with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h q => h_2 v v_2 h q) =
    h_2 v v_1 h q
-- Mathlib.Data.Set.Finite.Basic
Set.card_image_of_injective : ∀ {α : Type u} {β : Type v} (s : Set α) [inst : Fintype ↑s] {f : α → β} [inst_1 : Fintype ↑(f '' s)],
  Function.Injective f → Fintype.card ↑(f '' s) = Fintype.card ↑s
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Uniform convergence on a filter `p'` to a constant function is equivalent to convergence in
`p ×ˢ p'`.  -/
tendsto_prod_filter_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α}
  {c : β}, Filter.Tendsto (↿F) (p ×ˢ p') (nhds c) ↔ TendstoUniformlyOnFilter F (fun x => c) p p'
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.uliftYonedaAdjunction_homEquiv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ}
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) [inst_3 : L.IsLeftKanExtension α]
  {P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} {Y : ℰ} (f : L.obj P ⟶ Y) {Z : Cᵒᵖ} (z : P.obj Z),
  (CategoryTheory.ConcreteCategory.hom ((((CategoryTheory.Presheaf.uliftYonedaAdjunction L α).homEquiv P Y) f).app Z))
      z =
    {
      down :=
        CategoryTheory.CategoryStruct.comp (α.app (Opposite.unop Z))
          (CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.uliftYonedaEquiv.symm z)) f) }
-- Init.WFComputable
Acc.ndrecOn_eq_ndrecOnC : @Acc.ndrecOn = @Acc.ndrecOnC
-- Mathlib.Data.Fin.SuccPred
/-- Embedding `i : Fin n` into `Fin (n + 1)` with a hole around `p : Fin (n + 1)`
never results in `p` itself  -/
Fin.succAbove_ne : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.succAbove i ≠ p
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
CommMonCat.Hom.Simps.hom : (X Y : CommMonCat) → X.Hom Y → ↑X →* ↑Y
-- Mathlib.RingTheory.WittVector.Truncated
/-- We can turn a truncated Witt vector `x` into a Witt vector
by setting all coefficients after `x` to be 0.
 -/
TruncatedWittVector.out : {p n : ℕ} → {R : Type u_1} → [CommRing R] → TruncatedWittVector p n R → WittVector p R
-- Mathlib.Data.Set.Lattice
Set.sUnion_iUnion : ∀ {α : Type u_1} {ι : Sort u_5} (s : ι → Set (Set α)), ⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.gc_map_comap : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
  GaloisConnection (Subsemiring.map f) (Subsemiring.comap f)
-- Mathlib.Logic.Function.Defs
Function.prod_const_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (a : α) (b : β),
  Function.prod (Function.const ι a) (Function.const ι b) = Function.const ι (a, b)
-- Mathlib.Order.SymmDiff
symmDiff_le_sup : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, symmDiff a b ≤ a ⊔ b
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (p : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  p = Lean.Grind.Linarith.Poly.nil →
    (match p with
      | Lean.Grind.Linarith.Poly.nil => h_1 ()
      | Lean.Grind.Linarith.Poly.add k v p => h_2 k v p) ≍
      h_1 ()
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt_chartAt_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {H : Type u_4} {M' : Type u_6} {H' : Type u_7} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  [inst_4 : TopologicalSpace H'] [inst_5 : TopologicalSpace M'] [inst_6 : ChartedSpace H' M']
  [inst_7 : ChartedSpace H H'] (x : M') {y : E},
  y ∈ (extChartAt I x).target → writtenInExtChartAt I I x (↑(chartAt H' x)) y = y
-- Init.Data.Option.Lemmas
Option.or_none : ∀ {α : Type u_1} {o : Option α}, o.or none = o
-- Init.Data.Order.Opposite
/-- Creates a {name}`Max` instance from a {name}`Min` instance.

The result is a {lean}`Max α` instance that uses {lean}`min.min` as its {name}`max` operation.

If {name}`min` obeys laws, then {lean}`min.oppositeMax` obeys the corresponding laws for {name}`Max`.
To automatically derive these laws, use {lit}`open scoped Std.OppositeOrderInstances`.

For example, one can use the derived instances to prove properties about the opposite {name}`Max`
instance:

```lean
open scoped Std.OppositeOrderInstances in
example [LE α] [DecidableLE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] {a b : α} :
    letI : LE α := LE.opposite inferInstance
    letI : Max α := (inferInstance : Min α).oppositeMax
    max a b = if b ≤ a then a else b :=
  letI : LE α := LE.opposite inferInstance
  letI : Max α := (inferInstance : Min α).oppositeMax
  Std.max_eq_if
```

Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLeftLeaningMax α`
instance for the opposite order that is required by {name}`max_eq_if`.
 -/
Min.oppositeMax : {α : Type u_1} → Min α → Max α
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_add : ∀ {K : Type u_1} [inst : RCLike K] (z w : K),
  RCLike.normSq (z + w) = RCLike.normSq z + RCLike.normSq w + 2 * RCLike.re (z * (starRingEnd K) w)
-- Init.Data.String.Lemmas.Order
String.Pos.lt_ofSliceTo_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos},
  q < String.Pos.ofSliceTo p ↔ ∃ (h : q ≤ p₀), p₀.sliceTo q h < p
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instQuasiCompactToNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.QuasiCompact (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.Rel.smul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {n : ℕ}
  {a : M}, DividedPowerAlgebra.Rel R M (MvPolynomial.X (n, r • a)) (r ^ n • MvPolynomial.X (n, a))
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.not_isHamiltonianCycle_of_infinite : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} [h : Infinite α],
  ¬p.IsHamiltonianCycle
-- Lean.Compiler.IR.Basic
/-- Return `1 : uint8` Iff `RC(x) > 1`  -/
Lean.IR.Expr.isShared : Lean.IR.VarId → Lean.IR.Expr