mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- The left adjoint of a triangulated functor is triangulated.
 -/
CategoryTheory.Adjunction.isTriangulated_leftAdjoint : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [inst_12 : F.CommShift ℤ] [inst_13 : G.CommShift ℤ] [adj.CommShift ℤ] [G.IsTriangulated],
  F.IsTriangulated
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightEq_inv_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r r' : R₂ ⟶ R₁) (h : r = r') (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightEq L r r' h).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The only arrows of the discrete groupoid are the identity arrows.  -/
CategoryTheory.Subgroupoid.discrete : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C
-- Mathlib.Tactic.TermCongr
/-- Create the congruence hole. Used by `elabCHole`.

Saves the current mvarCounter as a proxy for age. We use this to avoid
reprocessing old congruence holes that happened to leak into the local context.  -/
Mathlib.Tactic.TermCongr.mkCHole : Bool → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner
product space has no eigenvalues.  -/
LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (μ : 𝕜), Module.End.eigenspace (T.restrict ⋯) μ = ⊥
-- Mathlib.Algebra.CharP.Invertible
CharP.natCast_gcdA_mul_intCast_eq_gcd : ∀ {R : Type u_1} [inst : Ring R] {p : ℕ} [CharP R p] (n : ℕ), ↑(n.gcdA p) * ↑n = ↑(n.gcd p)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The underlying `Mor₂` term of a `NormalExpr` term.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.e : Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Elements of disjoint, normal subgroups commute.  -/
Subgroup.commute_of_normal_of_disjoint : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G),
  H₁.Normal → H₂.Normal → Disjoint H₁ H₂ → ∀ (x y : G), x ∈ H₁ → y ∈ H₂ → Commute x y
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.continuous_equivIco_symm : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜],
  Continuous ⇑(AddCircle.equivIco p a).symm
-- Mathlib.Algebra.CharP.MixedCharZero
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.pnatCast_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))], ↑1 = 1
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_hom_inv_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C),
  CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (e.inv.app X).unop =
    CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj X))
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If an affine subspace contains a set of points, it contains the `spanPoints` of that set.  -/
AffineSubspace.spanPoints_subset_coe_of_subset_coe : ∀ {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} {s₁ : AffineSubspace k P}, s ⊆ ↑s₁ → spanPoints k s ⊆ ↑s₁
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.ext_iff : ∀ {G : Type u_3} [inst : Group G] {u v : UniformSpace G},
  IsUniformGroup G → IsUniformGroup G → (u = v ↔ nhds 1 = nhds 1)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.instDiv : Div GaussianInt
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverUnit_obj_left : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C), ((CategoryTheory.toOverUnit C).obj X).left = X
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The natural transformation from
`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b` to
`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a`. (This is an isomorphism.)  -/
CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (a b : EInt) →
                  (t.eTruncLT.obj b).comp ((t.eTruncGE.obj a).comp (t.eTruncLT.obj b)) ⟶
                    (t.eTruncLT.obj b).comp (t.eTruncGE.obj a)
-- Mathlib.Order.MinMax
instCommutativeMin : ∀ {α : Type u} [inst : LinearOrder α], Std.Commutative min
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_mul_C : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  {p : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁),
  MvPolynomial.eval₂ f g (p * MvPolynomial.C a) = MvPolynomial.eval₂ f g p * f a
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.eraseMin_aux : ∀ {α : Type u_1} [inst : Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂ →
    Ordnode.Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.star : Lean.Meta.LazyDiscrTree.Key
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.antisymm : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =O[l] g → g =O[l] f → f =Θ[l] g
-- Mathlib.Computability.Language
Language.ext_iff : ∀ {α : Type u_1} {l m : Language α}, l = m ↔ ∀ (x : List α), x ∈ l ↔ x ∈ m
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.mul_log_nonpos : ∀ {x : ℝ}, 0 ≤ x → x ≤ 1 → x * Real.log x ≤ 0
-- Lean.Expr
Lean.mkApp6 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions.fromJson : Lean.Json → Except String Lean.Lsp.DidChangeWatchedFilesRegistrationOptions
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Reify.0.Lean.Meta.Grind.Arith.Linear.reify?.go : ℕ → Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM Lean.Meta.Grind.Arith.Linear.LinExpr
-- Mathlib.Algebra.Group.Action.Defs
VAddAssocClass.to₂₃₄ : ∀ (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [inst : VAdd M N] [inst_1 : VAdd M P]
  [inst_2 : VAdd M Q] [inst_3 : VAdd P Q] [inst_4 : AddMonoid N] [inst_5 : AddAction N P] [inst_6 : AddAction N Q]
  [VAddAssocClass M N P] [VAddAssocClass M N Q] [VAddAssocClass M P Q],
  (Function.Surjective fun m => m +ᵥ 0) → VAddAssocClass N P Q
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.empty_div : ∀ {α : Type u_2} [inst : Div α] {s : Set α}, ∅ / s = ∅
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.tensorEquiv_symm_single_eq_single_zero_tmul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] (mn : M × N) (r : R),
  (AddMonoidAlgebra.tensorEquiv R).symm (AddMonoidAlgebra.single mn r) =
    AddMonoidAlgebra.single mn.1 1 ⊗ₜ[R] AddMonoidAlgebra.single mn.2 r
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instAddCommGroup : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [AddCommGroup β] → AddCommGroup (MeasureTheory.SimpleFunc α β)
-- Lean.Meta.SynthInstance
Lean.Meta.synthInstanceCore? : Lean.Expr → optParam (Option ℕ) none → Lean.MetaM (Option Lean.Expr)
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceMap_toHom : ∀ {R S : CommRingCat} (f : R ⟶ S),
  (AlgebraicGeometry.Spec.locallyRingedSpaceMap f).toHom = (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
hasMFDerivWithinAt_inter' : ∀ {𝕜 : 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'} {x : M} {s t : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  t ∈ nhdsWithin x s → (HasMFDerivAt[s ∩ t] f x f' ↔ HasMFDerivAt[s] f x f')
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.monotone_pushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  Monotone (CategoryTheory.Presieve.pushforward f)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instIsMonHomHomLeftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X : C} [inst_3 : CategoryTheory.MonObj X],
  CategoryTheory.IsMonHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- Category structure on `Grpd`  -/
CategoryTheory.Grpd.category : CategoryTheory.LargeCategory CategoryTheory.Grpd
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.IsStandardEtale.of_isLocalizationAway : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardEtale R S] {Sₛ : Type u_4} [inst_4 : CommRing Sₛ] [inst_5 : Algebra S Sₛ] [inst_6 : Algebra R Sₛ]
  [IsScalarTower R S Sₛ] (s : S) [IsLocalization.Away s Sₛ], Algebra.IsStandardEtale R Sₛ
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Normed ring structure on the product of finitely many normed rings, using the sup norm.  -/
Pi.normedRing : {ι : Type u_3} → {R : ι → Type u_4} → [Fintype ι] → [(i : ι) → NormedRing (R i)] → NormedRing ((i : ι) → R i)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.aestronglyMeasurable : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : PseudoEMetricSpace E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E},
  (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    MeasureTheory.TendstoInMeasure μ f u g → MeasureTheory.AEStronglyMeasurable g μ
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- `colimitCocone F` becomes colimit after the application of `π₃ : ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.isColimitπ₃MapCoconeColimitCocone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [inst_3 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [inst_4 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.IsColimit
                    (CategoryTheory.ShortComplex.π₃.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))
-- Mathlib.CategoryTheory.Limits.Comma
/-- Provided that `R` preserves the appropriate limit, then the cone in `coneOfPreserves` is a
limit.  -/
CategoryTheory.Comma.coneOfPreservesIsLimit : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {B : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
            {T : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} T] →
                {L : CategoryTheory.Functor A T} →
                  {R : CategoryTheory.Functor B T} →
                    (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) →
                      [inst_4 : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] →
                        {c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))} →
                          CategoryTheory.Limits.IsLimit c₁ →
                            {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} →
                              (t₂ : CategoryTheory.Limits.IsLimit c₂) →
                                CategoryTheory.Limits.IsLimit (CategoryTheory.Comma.coneOfPreserves F c₁ t₂)
-- Init.Data.List.OfFn
/-- Creates a list by applying `f` to each potential index in order, starting at `0`.

Examples:
* `List.ofFn (n := 3) toString = ["0", "1", "2"]`
* `List.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = ["red", "green", "blue"]`
 -/
List.ofFn : {α : Type u_1} → {n : ℕ} → (Fin n → α) → List α
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.arg_eq_arg : ∀ {z w : Circle}, (↑z).arg = (↑w).arg ↔ z = w
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₂_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ),
  (X.sc₂ f g fg h n₀).g = (X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Lean.Parser.Term
Lean.Parser.Term.namedArgument : Lean.Parser.Parser
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.closure_setOfPred_im_lt`. -/
Complex.closure_setOf_im_lt : ∀ (a : ℝ), closure {z | z.im < a} = {z | z.im ≤ a}
-- Mathlib.Util.ElabWithoutMVars
/-- Elaborates a term with `errToSorry = false` and ensuring it has no metavariables.  -/
elabTermWithoutNewMVars : Lean.Name → Lean.Term → Lean.Elab.Tactic.TacticM Lean.Expr
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instSMul : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : PartialOrder Γ] → {V : Type u_8} → [inst_1 : Zero V] → [SMulZeroClass R V] → SMul R (HahnSeries Γ V)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.finsetSum_singleton : ∀ {M : Type u_5} {ι : Type u_6} [inst : AddCommMonoid M] (s : Finset ι) (I : ι → M), ∑ i ∈ s, {I i} = {∑ i ∈ s, I i}
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_eq_beth_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.lift.{v, u} c = Cardinal.beth (OfNat.ofNat n) ↔ c = Cardinal.beth (OfNat.ofNat n)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = false → t.getKey? a = none
-- Lean.Environment
/-- Subset of `modules` for which `importAll` is `true`. This is assumed to be a much smaller set so
we precompute it instead of iterating over all of `modules` multiple times. However, note that
in a non-`module` file, this is identical to `modules`.
 -/
Lean.EnvironmentHeader.importAllModules : Lean.EnvironmentHeader → Array Lean.EffectiveImport
-- Std.Sync.Channel
/-- The slot in `buf` that the next receive will happen from.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.recvIdx : {α : Type} → Std.CloseableChannel.Bounded.State✝ α → ℕ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.w_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y) {Z : D}
  (h : T.obj Y.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.hom
      (CategoryTheory.CategoryStruct.comp (T.map (CategoryTheory.StructuredArrow.Hom.right f)) h) =
    CategoryTheory.CategoryStruct.comp Y.hom h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k},
  t.WF → (Std.DTreeMap.Internal.Impl.filterMap! f t).getD k fallback = ((t.get? k).bind (f k)).getD fallback
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.eq_2 : ∀ (motive : Nat.Partrec.Code → Sort u_1) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match Nat.Partrec.Code.succ with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_2 ()
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.base : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : CategoryTheory.Precoverage C} →
      {ι : C → Type w} → (X : C) → ι X → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι X
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.single_div_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommGroup Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedAddMonoid Γ]
  [inst_3 : Field R] (a b : Γ) (r s : R),
  (HahnSeries.single a) r / (HahnSeries.single b) s = (HahnSeries.single (a - b)) (r / s)
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- **Alias** of `CategoryTheory.SimplicialThickening.functorMap`.

---

Auxiliary definition for `SimplicialThickening.functor`  -/
CategoryTheory.SimplicialThickening.orderHom : {J K : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : LinearOrder K] →
      (f : J →o K) →
        (i j : CategoryTheory.SimplicialThickening J) →
          CategoryTheory.Functor (i ⟶ j) ({ as := f i.as } ⟶ { as := f j.as })
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
toAdd_prod : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → Multiplicative M),
  Multiplicative.toAdd (∏ i ∈ s, f i) = ∑ i ∈ s, Multiplicative.toAdd (f i)
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.isComplex₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ComposableArrows C 0), S.IsComplex
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.biUnion_vadd_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (s : Finset α) (t : Finset β),
  (s.biUnion fun x => x +ᵥ t) = s +ᵥ t
-- Lean.Meta.Coe
/-- Recurse through projection functions (e.g. `(f a b c).fst.snd` => `f`)  -/
_private.Lean.Meta.Coe.0.Lean.Meta.recProjTarget : (e : Lean.Expr) → optParam Lean.Name e.getAppFn.constName! → Lean.MetaM Lean.Name
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.zpow_apply_eq_of_apply_apply_eq_self : ∀ {α : Type u_1} {f : Equiv.Perm α} {x : α}, f (f x) = x → ∀ (i : ℤ), (f ^ i) x = x ∨ (f ^ i) x = f x
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkGateCached.go.match_4.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (motive : (aig : Std.Sat.AIG α) → aig.BinaryInput → Sort u_1)
  (decls : Array (Std.Sat.AIG.Decl α)) (cache : Std.Sat.AIG.Cache α decls) (hdag : Std.Sat.AIG.IsDAG α decls)
  (hzero : 0 < decls.size) (hconst : decls[0] = Std.Sat.AIG.Decl.false)
  (input : { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.BinaryInput)
  (h_1 :
    (decls : Array (Std.Sat.AIG.Decl α)) →
      (cache : Std.Sat.AIG.Cache α decls) →
        (hdag : Std.Sat.AIG.IsDAG α decls) →
          (hzero : 0 < decls.size) →
            (hconst : decls[0] = Std.Sat.AIG.Decl.false) →
              (input : { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.BinaryInput) →
                motive { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } input),
  (match { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }, input with
    | { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }, input =>
      h_1 decls cache hdag hzero hconst input) =
    h_1 decls cache hdag hzero hconst input
-- Init.Prelude
/-- Compute whether `x` is a tagged pointer or not.  -/
isScalarObj : {α : Type u} → α → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termG₂ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.instCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [CompactSpace M], CompactSpace Mᵐᵒᵖ
-- Init.Core
Bool.of_not_eq_false : ∀ {b : Bool}, ¬b = false → b = true
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Int.ideal_span_absNorm_eq_self : ∀ (J : Ideal ℤ), Ideal.span {↑(Ideal.absNorm J)} = J
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).hom
      (HomologicalComplex.singleObjHomologySelfIso c j A).inv =
    ((HomologicalComplex.single C c j).obj A).homologyπ j
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller₀_sModEq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} {n : ℕ},
  (Ideal.Quotient.mk I) y = (Perfection.coeff (R ⧸ I) p n) x →
    (Perfection.teichmuller₀ p I) x ≡ y ^ p ^ n [SMOD I ^ (n + 1)]