mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Slice.Operations
Std.Slice.instToIterator : {γ : Type u_1} →
  {m : Type u_2 → Type u_3} → {α β : Type u_2} → [Std.ToIterator γ m α β] → Std.ToIterator (Std.Slice γ) m α β
-- Mathlib.RingTheory.Flat.Domain
/-- Tensor product of linearly independent families is linearly independent over domains.
This is true over non-domains if one of the modules is flat.
See `LinearIndepOn.tmul_of_flat_left`.  -/
LinearIndepOn.tmul_of_isDomain : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : AddCommGroup N] [inst_5 : Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M}
  {w : κ → N} {s : Set ι} {t : Set κ},
  LinearIndepOn R v s → LinearIndepOn R w t → LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The left dual space of an R-module M is the R-module of linear maps `M → R`.  -/
Module.Dual : (R : Type u_4) → (M : Type u_5) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_5 u_4)
-- Mathlib.Data.Nat.ModEq
Nat.add_modEq_right : ∀ {n a : ℕ}, a + n ≡ a [MOD n]
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- The chain complex `s.nondegComplex` attached to a splitting of a simplicial object `X`
becomes isomorphic to the normalized Moore complex `N₁.obj X` defined as a formal direct
factor in the category `Karoubi (ChainComplex C ℕ)`.  -/
CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) →
        [inst_1 : CategoryTheory.Preadditive C] →
          (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex ≅
            AlgebraicTopology.DoldKan.N₁.obj X
-- Lean.Level
Lean.simpLevelMax' : Lean.Level → Lean.Level → Lean.Level → Lean.Level
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.Replacement.apply : Lean.Elab.Term.MutualClosure.Replacement → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Having wide pushout at any universe level implies having binary pushouts.  -/
CategoryTheory.Limits.hasPushouts_of_hasWidePushouts : ∀ (D : Type u) [inst : CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasWidePushouts D],
  CategoryTheory.Limits.HasPushouts D
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- The pushout of two maps `f : S ⟶ X₁` and `g : S ⟶ X₂` is the quotient
by the equivalence relation on `X₁ ⊕ X₂` generated by this relation.  -/
CategoryTheory.Limits.Types.Pushout.Rel : {S X₁ X₂ : Type u} → (S ⟶ X₁) → (S ⟶ X₂) → X₁ ⊕ X₂ → X₁ ⊕ X₂ → Prop
-- Mathlib.Topology.Order.Lattice
TopologicalLattice.toContinuousInf : ∀ {L : Type u_1} {inst : TopologicalSpace L} {inst_1 : Lattice L} [self : TopologicalLattice L], ContinuousInf L
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.w_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.RightLift f g} (h : s ⟶ t) {Z : c ⟶ a} (h_1 : g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight h.left f)
      (CategoryTheory.CategoryStruct.comp t.counit h_1) =
    CategoryTheory.CategoryStruct.comp s.counit h_1
-- Init.Grind.Interactive
/-- `repeat tac` repeatedly applies `tac` so long as it succeeds.
The tactic `tac` may be a tactic sequence, and if `tac` fails at any point in its execution,
`repeat` will revert any partial changes that `tac` made to the tactic state.
The tactic `tac` should eventually fail, otherwise `repeat tac` will run indefinitely.
 -/
Lean.Parser.Tactic.Grind.grindRepeat_ : Lean.ParserDescr
-- Init.Control.StateCps
/-- For continuation monads, it is not possible to provide a computable `MonadAttach` instance that
actually adds information about the return value. Therefore, this instance always attaches a proof
of `True`.
 -/
StateCpsT.instMonadAttach : {m : Type u → Type v} → {ε : Type u} → MonadAttach (StateCpsT ε m)
-- Std.Http.Protocol.H1.Writer
/-- Updates the writer's state machine to a new state.
 -/
Std.Http.Protocol.H1.Writer.setState : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Writer.State → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir
-- Init.Data.String.Termination
String.Pos.instWellFoundedRelationDown : {s : String} → WellFoundedRelation (String.Pos.Down s)
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
/-- Auxiliary definition for `Presheaf.preservesLimitHomFamily`.  -/
CategoryTheory.Presheaf.preservesLimitHomFamilyTgt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} J] →
        [CategoryTheory.LocallySmall.{w, v, u} C] →
          (F : CategoryTheory.Functor J Cᵒᵖ) →
            PLift (CategoryTheory.Limits.HasLimit F) → CategoryTheory.Functor Cᵒᵖ (Type w)
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.normalizerMonoidHom_apply_symm_apply_coe : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : ↥(Subgroup.normalizer ↑H)) (a : ↥H),
  ↑((MulEquiv.symm (H.normalizerMonoidHom x)) a) = (↑x)⁻¹ * ↑a * ↑x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
EuclideanGeometry.oangle.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.neg_one_pow_smul_map_insertNth : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (p : Fin (n + 1)) (x : E) (v : Fin n → E),
  (-1) ^ ↑p • f (p.insertNth x v) = f (Matrix.vecCons x v)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.map_mk_symm_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : Mᵈᵐᵃ),
  Filter.map (⇑DomMulAct.mk.symm) (nhds x) = nhds (DomMulAct.mk.symm x)
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_eq_if : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α},
  List.minIdxOn? f xs = if h : xs ≠ [] then some (List.minIdxOn f xs h) else none
-- Mathlib.Topology.Algebra.Field
/-- Left-multiplication by a nonzero element of a topological division ring is proper, i.e.,
inverse images of compact sets are compact.  -/
Filter.tendsto_cocompact_mul_left₀ : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : TopologicalSpace K] [SeparatelyContinuousMul K] {a : K},
  a ≠ 0 → Filter.Tendsto (fun x => a * x) (Filter.cocompact K) (Filter.cocompact K)
-- Aesop.RulePattern
Aesop.RulePattern.match : Lean.Expr → Aesop.RulePattern → Aesop.BaseM (Option Aesop.Substitution)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonMonoidHom_apply : ∀ {α : Type u_2} [inst : MulOneClass α] (a : α), Set.singletonMonoidHom a = {a}
-- Mathlib.Data.Finsupp.Basic
Finsupp.domCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] (e : α ≃ β) (f : β ≃ γ),
  (Finsupp.domCongr e).trans (Finsupp.domCongr f) = Finsupp.domCongr (e.trans f)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instAdd.eq_1 : ∀ {α : Type u},
  FreeAddGroup.instAdd =
    { add := fun x y => Quot.liftOn x (fun L₁ => Quot.liftOn y (fun L₂ => FreeAddGroup.mk (L₁ ++ L₂)) ⋯) ⋯ }
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.completeLattice : {α : Type u_1} → [inst : LE α] → CompleteLattice (LowerSet α)
-- Mathlib.RingTheory.Unramified.Pi
Algebra.FormallyUnramified.instForall : ∀ {R : Type u_1} {I : Type u_2} [Finite I] (f : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (f i)]
  [inst_2 : (i : I) → Algebra R (f i)] [∀ (i : I), Algebra.FormallyUnramified R (f i)],
  Algebra.FormallyUnramified R ((i : I) → f i)
-- Mathlib.RingTheory.Ideal.Over
Ideal.comap_liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} {C : Type u_4} [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] (Q : Ideal C) (p : Ideal A) [Q.LiesOver p] {F : Type u_6}
  [inst_6 : FunLike F B C] [inst_7 : AlgHomClass F A B C] (f : F), (Ideal.comap f Q).LiesOver p
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_nnratCast : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (q : ℚ≥0), WithVal.toVal v ↑q = ↑q
-- Mathlib.Topology.Algebra.Group.Basic
/-- In a Hausdorff magma with continuous multiplication, the centralizer of any set is closed.  -/
Set.isClosed_centralizer : ∀ {M : Type u_1} (s : Set M) [inst : Mul M] [inst_1 : TopologicalSpace M] [SeparatelyContinuousMul M] [T2Space M],
  IsClosed s.centralizer
-- Mathlib.Topology.Algebra.Module.FiniteDimension
FiniteDimensional.complete : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : UniformSpace E] [T2Space E] [IsUniformAddGroup E] [inst_6 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  [FiniteDimensional 𝕜 E], CompleteSpace E
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- An alternative version to `Submodule.FG.rTensor.directLimit_apply`.  -/
Submodule.FG.rTensor.directLimit_apply' : ∀ (R : Type u) (M : Type u_1) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq { P // P.FG }] {P : Submodule R M} (hP : P.FG)
  (u : TensorProduct R (↥P) N),
  (Submodule.FG.rTensor.directLimit R M N)
      ((Module.DirectLimit.of R { P // P.FG } (fun P => TensorProduct R (↥↑P) N)
          (fun ⦃x x_1⦄ h => LinearMap.rTensor N (Submodule.inclusion h)) ⟨P, hP⟩)
        u) =
    (LinearMap.rTensor N P.subtype) u
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω),
  μ.toFiniteMeasure s = μ s
-- Mathlib.Algebra.MvPolynomial.Division
_private.Mathlib.Algebra.MvPolynomial.Division.0.MvPolynomial.«term_/ᵐᵒⁿᵒᵐⁱᵃˡ__1» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Group.BallSphere
coe_neg_ball : ∀ {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.ball 0 r)), ↑(-v) = -↑v
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.freeFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (X : Type u),
  SheafOfModules.freeFunctor.obj X = SheafOfModules.free X
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalSpecialize : Lean.Elab.Tactic.Tactic
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opFunctor_obj_σ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 1)),
  (SimplicialObject.opFunctor.obj X).σ i =
    CategoryTheory.CategoryStruct.comp SimplicialObject.opObjIso.hom
      (CategoryTheory.CategoryStruct.comp (X.σ i.rev) SimplicialObject.opObjIso.inv)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_eq_sup : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : σ) (f : MvPolynomial σ R),
  MvPolynomial.degreeOf n f = f.support.sup fun m => m n
-- Mathlib.Topology.ContinuousOn
/-- If two sets coincide around `x`, then being continuous within one or the other at `x` is
equivalent. See also `continuousWithinAt_congr_set'` which requires that the sets coincide
locally away from a point `y`, in a T1 space.  -/
continuousWithinAt_congr_set : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, s =ᶠ[nhds x] t → (ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x)
-- Mathlib.Topology.WithTopology
WithTopology.instOrd : {X : Type u_1} → (t : TopologicalSpace X) → [Ord X] → Ord (WithTopology X t)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousLinearMap.compContinuousMultilinearMapL_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} {G : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousConstSMul 𝕜 F] [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜 G]
  [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G] [inst_13 : ContinuousConstSMul 𝕜 G] (g : F →L[𝕜] G)
  (f : ContinuousMultilinearMap 𝕜 E F),
  ((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G) g) f = g.compContinuousMultilinearMap f
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.sigmaι_eq_iff : ∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ] (i j : σ) (x : ↥(g i)) (y : ↥(g j)),
  (CategoryTheory.Limits.Sigma.ι g i) x = (CategoryTheory.Limits.Sigma.ι g j) y ↔ ⟨i, x⟩ = ⟨j, y⟩
-- Mathlib.CategoryTheory.Subobject.Basic
/-- `exists f` applied to a subobject `x` is isomorphic to the image of `x.arrow ≫ f`.  -/
CategoryTheory.Subobject.existsIsoImage : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasImages C] →
        (f : X ⟶ Y) →
          (x : CategoryTheory.Subobject X) →
            CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.exists f).obj x) ≅
              CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp x.arrow f)
-- Mathlib.Algebra.Lie.UniversalEnveloping
/-- The universal property of the universal enveloping algebra: Lie algebra morphisms into
associative algebras lift to associative algebra morphisms from the universal enveloping algebra.  -/
UniversalEnvelopingAlgebra.lift : (R : Type u₁) →
  {L : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {A : Type u₃} →
            [inst_3 : Ring A] → [inst_4 : Algebra R A] → (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A)
-- Mathlib.Logic.Embedding.Basic
Function.instEmbeddingLikeEmbedding : ∀ {α : Sort u} {β : Sort v}, EmbeddingLike (α ↪ β) α β
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_one_add_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε : Type u_8} [inst : ENorm ε] (f : α → ε) (μ ν : MeasureTheory.Measure α),
  MeasureTheory.eLpNorm f 1 (μ + ν) = MeasureTheory.eLpNorm f 1 μ + MeasureTheory.eLpNorm f 1 ν
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.instIsIsoOverAsOverHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] (f : X ⟶ Y) [CategoryTheory.IsIso f] [inst_4 : CategoryTheory.HomIsOver f S],
  CategoryTheory.IsIso (CategoryTheory.OverClass.asOverHom S f)
-- Mathlib.Algebra.Group.Invertible.Basic
Invertible.ofLeftInverse_invOf : ∀ {R : Type u_1} {S : Type u_2} {G : Type u_3} [inst : MulOneClass R] [inst_1 : MulOneClass S] [inst_2 : FunLike G S R]
  [inst_3 : MonoidHomClass G S R] (f : R → S) (g : G) (r : R) (h : Function.LeftInverse (⇑g) f)
  [inst_4 : Invertible (f r)], ⅟r = ⅟(g (f r))
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        (coevaluation' :
            CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) →
          (evaluation' :
              CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶
                CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →
            autoParam
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y coevaluation')
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).inv
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight evaluation' Y)) =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom
                    (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
                CategoryTheory.ExactPairing.coevaluation_evaluation'._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight coevaluation' X)
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y X).hom
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X evaluation')) =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
                      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
                  CategoryTheory.ExactPairing.evaluation_coevaluation'._autoParam →
                CategoryTheory.ExactPairing X Y
-- Mathlib.Algebra.Homology.Single
CochainComplex.toSingle₀Equiv_apply : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V)
  (f : C ⟶ (CochainComplex.single₀ V).obj X), (C.toSingle₀Equiv X) f = f.f 0
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_carrier : ∀ {G : Type u_1} [inst : Group G] {s : Subgroup G} {x : G}, x ∈ s.carrier ↔ x ∈ s
-- Mathlib.CategoryTheory.Action.Limits
Action.instReflectsLimitForget : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J] (F : CategoryTheory.Functor J (Action V G)),
  CategoryTheory.Limits.ReflectsLimit F (Action.forget V G)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The counit axiom associated to a coalgebra.  -/
CategoryTheory.Comonad.Coalgebra.counit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) {Z : C}
  (h : self.A ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (G.ε.app self.A) h) = h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_inter_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → m₁.isEmpty = true → (m₁.inter m₂ ⋯).isEmpty = true
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_zero : √0 = 0
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.toSubmonoid_zpowers : ∀ {G : Type u_2} [inst : Group G] (g : G), (Subgroup.zpowers g).toSubmonoid = Submonoid.powers g ⊔ Submonoid.powers g⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- If `G` is isomorphic to `H`, then `G` is inducingly contained in `H`.  -/
SimpleGraph.Iso.isIndContained : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H), G.IsIndContained H
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.instHasProductsType : CategoryTheory.Limits.HasProducts (Type v)
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Fmla.subsumes_left : ∀ (f f₁ f₂ : Sat.Fmla), f.subsumes (f₁.and f₂) → f.subsumes f₁
-- Mathlib.Data.Vector3
Vector3.append_nil : ∀ {α : Type u_1} {n : ℕ} (w : Vector3 α n), [].append w = w
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.instSMulCommClassForall : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : DistribSMul S R] [SMulCommClass R S R], SMulCommClass (Matrix n n R) S (n → R)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- **Alias** of `circleIntegrable_congr`.

---

Circle integrability depends only on the restriction of the function to the sphere.
 -/
crcleIntegrable_congr : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E},
  Set.EqOn f₁ f₂ (Metric.sphere c |R|) → (CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R)
-- Init.Data.BitVec.Lemmas
BitVec.truncate_eq_setWidth : ∀ {w v : ℕ} {x : BitVec w}, BitVec.truncate v x = BitVec.setWidth v x
-- Mathlib.Topology.Continuous
ContinuousAt.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) (x : X),
  ContinuousAt f x = Filter.Tendsto f (nhds x) (nhds (f x))
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.isChar0Inst : Lean.Meta.Grind.Arith.FieldNormNum.Context✝ → Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_sub_id_strictMono : StrictMono fun x => Real.sinh x - x
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.exists_prime_dvd_of_not_inf_one : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : α},
  a ≠ 0 → b ≠ 0 → Associates.mk a ⊓ Associates.mk b ≠ 1 → ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIsoX_hom_D₁ : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j j' : J),
  CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j).hom (K.D₁ c j j') =
    CategoryTheory.CategoryStruct.comp (K.flip.D₂ c j j') (K.totalFlipIsoX c j').hom
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instEmptyCollection : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → EmptyCollection (Std.DTreeMap α β cmp)
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.inj_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
  IsDenseEmbedding e → ∀ {x y : α}, e x = e y ↔ x = y
-- Mathlib.RingTheory.Flat.Basic
/-- `Submodule.toBaseChange` as a `LinearEquiv`.  -/
Submodule.toBaseChange.toLinearEquiv : {R : Type u_1} →
  (A : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          [Module.Flat R A] →
            {M : Type u_5} →
              [inst_4 : AddCommMonoid M] →
                [inst_5 : Module R M] → (p : Submodule R M) → TensorProduct R A ↥p ≃ₗ[A] ↥(Submodule.baseChange A p)
-- Lean.Data.Lsp.CodeActions
/-- A command this code action executes.

If a code action provides an edit and a command, first the edit is executed and then the command.  -/
Lean.Lsp.CodeAction.command? : Lean.Lsp.CodeAction → Option Lean.Lsp.Command
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.data? : Lean.Lsp.CallHierarchyItem → Option Lean.Json
-- Mathlib.Order.DirSupClosed
/-- The condition `(d ∩ s).Nonempty` in `DirSupInaccOn` can be replaced with the stronger
`∃ b ∈ d, Ici b ∩ d ⊆ s` (under mild assumptions on `D`).  -/
dirSupInaccOn_iff_inter_subset : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α],
  IsLowerSet D →
    (DirSupInaccOn D s ↔
      ∀ ⦃d : Set α⦄,
        d ∈ D →
          d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s)
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_coe : ∀ {α : Type u_3} [inst : AddMonoid α] (l : List α) (comm : {x | x ∈ ↑l}.Pairwise AddCommute),
  (↑l).noncommSum comm = l.sum
-- Lean.Meta.HaveTelescope
/-- Do not eliminate unused `let`-declarations.  -/
Lean.Meta.ZetaUnusedMode.no : Lean.Meta.ZetaUnusedMode