mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.CodeBlock.toMessageData.loop : Lean.MessageData → Lean.Elab.Term.Do.Code → Lean.MessageData
-- Mathlib.Logic.Function.Basic
Function.update.eq_1 : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α),
  Function.update f a' v a = if h : a = a' then ⋯ ▸ v else f a
-- Lean.Server.FileWorker.SemanticHighlighting
/-- The non-overlapping tokens that have been definitively produced  -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.nonOverlapping : Lean.Server.FileWorker.HandleOverlapState✝ → Array Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyInf_iUnion_le : ∀ {X : Type u_1} {ι : Type u_2} [inst : UniformSpace X] (T : X → X) (F : ι → Set X),
  ⨆ i, Dynamics.coverEntropyInf T (F i) ≤ Dynamics.coverEntropyInf T (⋃ i, F i)
-- Mathlib.GroupTheory.Torsion
IsMulTorsion.torsionMulEquiv.eq_1 : ∀ {G : Type u_1} [inst : CommMonoid G] (tG : IsMulTorsion G),
  tG.torsionMulEquiv = (MulEquiv.submonoidCongr ⋯).trans Submonoid.topEquiv
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- The resolution maps intertwine the lift of a morphism and that morphism.  -/
CategoryTheory.ProjectiveResolution.lift_commutes_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z)
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) {Z_1 : ChainComplex C ℕ}
  (h : (ChainComplex.single₀ C).obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q)
      (CategoryTheory.CategoryStruct.comp Q.π h) =
    CategoryTheory.CategoryStruct.comp P.π (CategoryTheory.CategoryStruct.comp ((ChainComplex.single₀ C).map f) h)
-- Mathlib.ModelTheory.Syntax
/-- The sentence indicating that a basic relation symbol is symmetric.  -/
FirstOrder.Language.Relations.symmetric : {L : FirstOrder.Language} → L.Relations 2 → L.Sentence
-- Init.Data.List.Lemmas
List.map_append : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ l₂ : List α}, List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂
-- Mathlib.Algebra.Category.AlgCat.Basic
_private.Mathlib.Algebra.Category.AlgCat.Basic.0.AlgCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (carrier : Type v) [isRing : Ring carrier]
  [isAlgebra : Algebra R carrier],
  sizeOf { carrier := carrier, isRing := isRing, isAlgebra := isAlgebra } =
    1 + sizeOf carrier + sizeOf isRing + sizeOf isAlgebra
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A set `B` is a `G`-fixed block if `g • B = B` for all `g : G`.  -/
MulAction.IsFixedBlock : (G : Type u_1) → {X : Type u_2} → [SMul G X] → Set X → Prop
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- On square matrices, `Matrix.mulRightLinearMap` and `LinearMap.mulRight` coincide.  -/
mulRightLinearMap_eq_mulRight : ∀ {m : Type u_2} (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A],
  mulRightLinearMap m R = LinearMap.mulRight R
-- Mathlib.CategoryTheory.Sites.InducedTopology
CategoryTheory.Functor.restrictedTopology.eq_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D),
  F.restrictedTopology K = (CategoryTheory.Precoverage.comap F K.toPrecoverage).toGrothendieck
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`.  -/
AddSubmonoid.toAddCommMonoid : {M : Type u_5} → [inst : AddCommMonoid M] → (S : AddSubmonoid M) → AddCommMonoid ↥S
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.isIndContained_iff_exists_iso_subgraph : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, G.IsIndContained H ↔ ∃ H' _e, H'.IsInduced
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α} {fallback : β k}, m₁.getD k fallback = m₂.getD k fallback
-- Mathlib.Order.Interval.Finset.Basic
/-- A function from a locally finite preorder is strictly monotone if and only if it is strictly
monotone when restricted to pairs satisfying `a ⋖ b`.  -/
strictMono_iff_forall_covBy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [LocallyFiniteOrder α] [inst_2 : Preorder β] (f : α → β),
  StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b
-- Mathlib.Computability.NFA
NFA.reverse_reverse : ∀ {α : Type u} {σ : Type v} (M : NFA α σ), M.reverse.reverse = M
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.map_ofHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} D]
  [inst_3 : CategoryTheory.Preadditive D] (f : K ⟶ L) (Φ : CategoryTheory.Functor C D) [inst_4 : Φ.Additive],
  (CochainComplex.HomComplex.Cochain.ofHom f).map Φ =
    CochainComplex.HomComplex.Cochain.ofHom ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).map f)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Fintype.piFinset_mul : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Mul (α i)] (s t : (i : ι) → Finset (α i)),
  (Fintype.piFinset fun i => s i * t i) = Fintype.piFinset s * Fintype.piFinset t
-- Init.Prelude
/-- Mapping a constant function.

Given `a : α` and `v : f β`, `mapConst a v` is equivalent to `(fun _ => a) <$> v`. For some
functors, this can be implemented more efficiently; for all other functors, the default
implementation may be used.
 -/
Functor.mapConst : {f : Type u → Type v} → [self : Functor f] → {α β : Type u} → α → f β → f α
-- Mathlib.Order.Category.CompleteLat
CompleteLat.Iso.mk_hom : ∀ {α β : CompleteLat} (e : ↑α ≃o ↑β),
  (CompleteLat.Iso.mk e).hom = CategoryTheory.ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instInvolutiveInv : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : InvolutiveInv G] → [ContinuousInv G] → InvolutiveInv (SeparationQuotient G)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_span_range_of_linearIndependent : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [RankCondition R]
  {ι : Type u} {v : ι → M},
  Function.Injective v → LinearIndependent R v → (Submodule.span R (Set.range v)).spanRank = Cardinal.mk ι
-- Mathlib.Analysis.Normed.Group.Defs
GroupNorm.toNormedGroup.eq_1 : ∀ {E : Type u_5} [inst : Group E] (f : GroupNorm E),
  f.toNormedGroup =
    { toNorm := f.toSeminormedGroup.toNorm, toGroup := f.toSeminormedGroup.toGroup,
      toPseudoMetricSpace := f.toSeminormedGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- An auxiliary definition to be used in the proof of `exists_of_sep` below.
Given a compatible family of local sections for `P⁺`, and representatives of said sections,
construct a compatible family of local sections of `P` over the combination of the covers
associated to the representatives.
The separatedness condition is used to prove compatibility among these local sections of `P`.  -/
CategoryTheory.GrothendieckTopology.Plus.meqOfSep : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [instCC : CategoryTheory.ConcreteCategory D FD] →
                  [inst_3 :
                      ∀ {X : C} (S : J.Cover X),
                        CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
                          (CategoryTheory.forget D)] →
                    [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                      [inst_5 :
                          ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                            CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
                        [∀ (X : C),
                              CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] →
                          (P : CategoryTheory.Functor Cᵒᵖ D) →
                            (∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))),
                                (∀ (I : S.Arrow),
                                    (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x =
                                      (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) →
                                  x = y) →
                              (X : C) →
                                (S : J.Cover X) →
                                  (s : CategoryTheory.Meq (J.plusObj P) S) →
                                    (T : (I : S.Arrow) → J.Cover I.Y) →
                                      (t : (I : S.Arrow) → CategoryTheory.Meq P (T I)) →
                                        (∀ (I : S.Arrow), ↑s I = CategoryTheory.GrothendieckTopology.Plus.mk (t I)) →
                                          CategoryTheory.Meq P (S.bind T)
-- Lean.Elab.App
/-- Get the function's named arguments (which were found during elaboration).  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getFoundNamedArgs : Lean.Elab.Term.ElabAppArgs.M (Array Lean.Name)
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.pappAck.eq_2 : ∀ (n : ℕ), Nat.Partrec.Code.pappAck n.succ = Nat.Partrec.Code.pappAck.step (Nat.Partrec.Code.pappAck n)
-- Mathlib.RepresentationTheory.Intertwining
/-- An `Equiv` between representations could be built from a `LinearEquiv` and an assumption
proving the `G`-equivariance.  -/
Representation.Equiv.mk : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} →
                      {σ : Representation A G W} → (e : V ≃ₗ[A] W) → (∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) → ρ.Equiv σ
-- Mathlib.Data.PFun
PFun.preimage_univ : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β), f.preimage Set.univ = f.Dom
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.mk.inj : ∀ {α : Type} {state state_1 : Std.Mutex (Std.CloseableChannel.Zero.State✝ α)},
  { state := state } = { state := state_1 } → state = state_1
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv'_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LinearMap.toMatrixAlgEquiv'.symm = Matrix.toLinAlgEquiv'
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_zero_of_unique : ∀ {α : Type u_1} [inst : Preorder α] [Unique α], Order.krullDim α = 0
-- Mathlib.Analysis.Calculus.Deriv.Add
hasStrictDerivAt_add_const_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasStrictDerivAt (fun x => f x + c) f' x ↔ HasStrictDerivAt f f' x
-- Mathlib.RingTheory.Smooth.Fiber
/-- Let `(R, m, k)` be a local ring, `(S, M, K)` be a local `R`-algebra that is `R`-flat such that
`k ⊗[R] S` is `k`-formally smooth.

Suppose there exists an `R`-presentation `S = P/I` with `I` finitely generated, and that
`P` is `R`-formally smooth and `Ω[P⁄R]` is `P`-finite free.

Then `S` is `R`-formally smooth.

Such `P` always exists when `S` is essentially of finite presentation over `R`.
See `FormallySmooth.of_formallySmooth_residueField_tensor`.
 -/
_private.Mathlib.RingTheory.Smooth.Fiber.0.Algebra.FormallySmooth.of_formallySmooth_residueField_tensor_aux : ∀ {R : Type u_1} {S : Type u_2} {P : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Module.Flat R S] [inst_4 : CommRing P] [inst_5 : Algebra R P] [inst_6 : Algebra P S] [IsScalarTower R P S]
  [inst_8 : IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
  [Algebra.FormallySmooth (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) S)]
  [Algebra.FormallySmooth R P] [Module.Free P Ω[P⁄R]] [Module.Finite P Ω[P⁄R]],
  Function.Surjective ⇑(algebraMap P S) → (RingHom.ker (algebraMap P S)).FG → Algebra.FormallySmooth R S
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.popScopes : ℕ → Lean.Elab.Command.CommandElabM Unit
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.property_map : ∀ {m : Type w → Type w'} [inst : Functor m] {α β : Type w} {x : Std.Iterators.PostconditionT m α} {f : α → β} {b : β},
  (Std.Iterators.PostconditionT.map f x).Property b ↔ ∃ a, f a = b ∧ x.Property a
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (a : B),
  (CategoryTheory.Lax.StrongTrans.id F).app a = (CategoryTheory.Lax.LaxTrans.id F).app a
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.two_mul_apply_root_root : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) (i j : ι) [FaithfulSMul S R],
  2 * (B.form (P.root i)) (P.root j) = P.pairing i j * (B.form (P.root j)) (P.root j)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.mk.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (a a_1 : NumberField.RingOfIntegers K)
  (e_a : a = a_1) (b b_1 : NumberField.RingOfIntegers K) (e_b : b = b_1) (c c_1 : NumberField.RingOfIntegers K)
  (e_c : c = c_1) (u u_1 : (NumberField.RingOfIntegers K)ˣ) (e_u : u = u_1) (ha : ¬hζ.toInteger - 1 ∣ a)
  (hb : ¬hζ.toInteger - 1 ∣ b) (hc : c ≠ 0) (coprime : IsCoprime a b) (hcdvd : hζ.toInteger - 1 ∣ c)
  (H : a ^ 3 + b ^ 3 = ↑u * c ^ 3),
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H } =
    { a := a_1, b := b_1, c := c_1, u := u_1, ha := ⋯, hb := ⋯, hc := ⋯, coprime := ⋯, hcdvd := ⋯, H := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.hasBinaryBiproduct_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBinaryBiproduct X Y F],
  CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.coe_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : One M] [inst_1 : One N] [inst_2 : One P] (g : OneHom N P)
  (f : OneHom M N), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.HasProjectiveDimensionLT.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C} {n : ℕ},
  (∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄, Subsingleton (CategoryTheory.Abelian.Ext X Y i)) →
    CategoryTheory.HasProjectiveDimensionLT X n
-- Mathlib.Analysis.Complex.Poisson
/-- **Poisson integral formula** for ℂ-differentiable functions on arbitrary disks in the complex plane,
formulated with the Poisson kernel of integration.
 -/
DiffContOnCl.circleAverage_poissonKernel_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E]
  {c : ℂ},
  DiffContOnCl ℂ f (Metric.ball c R) → w ∈ Metric.ball c R → Real.circleAverage (poissonKernel c w • f) c R = f w
-- Mathlib.RingTheory.AdicCompletion.Topology
IsPrecomplete.congr_ringEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) (e : R ≃+* S),
  IsPrecomplete (Ideal.map e I) S ↔ IsPrecomplete I R
-- Aesop.RuleSet.Name
Aesop.RuleSetName : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `X`-coordinate of a representative of `P + Q` for two distinct Jacobian point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`.  -/
WeierstrassCurve.Jacobian.addX : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → (Fin 3 → R) → R
-- Lean.Attributes
Lean.instInhabitedAttributeKind : Inhabited Lean.AttributeKind
-- Mathlib.Lean.ContextInfo
/-- Run tactic code in the context of an infotree node, capturing InfoTrees for suggestion extraction.

Returns both the resulting goals and the InfoTrees produced during tactic execution.
Use `collectTryThisSuggestions` from `Mathlib.Lean.Elab.InfoTree` to extract suggestions.  -/
Lean.Elab.ContextInfo.runTacticCodeCapturingInfoTree : Lean.Elab.ContextInfo →
  Lean.Elab.TacticInfo →
    Lean.MVarId →
      Lean.Syntax → Lean.Elab.Command.CommandElabM (List Lean.MVarId × Lean.PersistentArray Lean.Elab.InfoTree)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.comp.inj : ∀ {e : Lean.Expr} {isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift} {f g h : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η θ : Mathlib.Tactic.BicategoryLike.Mor₂} {e_1 : Lean.Expr}
  {isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift} {f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂},
  Mathlib.Tactic.BicategoryLike.Mor₂.comp e isoLift? f g h η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂.comp e_1 isoLift?_1 f_1 g_1 h_1 η_1 θ_1 →
    e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1 ∧ θ = θ_1
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** with the Integral form of the remainder.

We assume that `f` is `n+1`-times continuously differentiable on the closed set `uIcc x₀ x`. Then
$$f(x) - (P_n f)(x₀, x) = \int_{x_0}^x \frac{f^{(n+1)}(t) (x - t)^n}{n!} dt,$$
where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated
derivative.  -/
taylor_integral_remainder : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → F} {x x₀ : ℝ}
  {n : ℕ},
  ContDiffOn ℝ (↑(n + 1)) f (Set.uIcc x₀ x) →
    f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x =
      ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n.factorial) • iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) t
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.exists_lt_of_prod_lt' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : LinearOrder M] {f g : ι → M} {s : Finset ι}
  [MulLeftMono M], ∏ i ∈ s, f i < ∏ i ∈ s, g i → ∃ i ∈ s, f i < g i
-- Mathlib.Tactic.ITauto
/-- Constructor for `xor p q`.  -/
Mathlib.Tactic.ITauto.IProp.xor : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_same_else : ∀ {w : ℕ} (c : Bool) (t e : BitVec w), ((bif c then t else e) == e) = (!c || t == e)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_smul : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} (P : Fin 3 → F) {u : F},
  IsUnit u → WeierstrassCurve.Projective.Point.toAffine W (u • P) = WeierstrassCurve.Projective.Point.toAffine W P
-- Mathlib.Data.NNReal.Defs
/-- If `Γ₀ˣ` is nontrivial and `f : Γ₀ →*₀ ℝ≥0` is strictly monotone, then for any positive
`r : ℝ≥0`, there exists `d : Γ₀ˣ` with `f d < r`.  -/
NNReal.exists_lt_of_strictMono : ∀ {Γ₀ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ₀] [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ NNReal},
  StrictMono ⇑f → ∀ {r : NNReal}, 0 < r → ∃ d, f ↑d < r
-- Mathlib.Computability.RE
PrimrecPred.computablePred : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop}, PrimrecPred p → ComputablePred p
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInTime.mk : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} →
      {f : α → β} →
        (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ) →
          (time : ℕ → ℕ) →
            ((a : α) →
                Turing.TM2OutputsInTime toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
                  (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a)))) (time (ea a).length)) →
              Turing.TM2ComputableInTime ea eb f
-- Mathlib.Algebra.Algebra.Basic
/-- Ring ⥤ ℤ-Alg  -/
Ring.toIntAlgebra : (R : Type u_1) → [inst : Ring R] → Algebra ℤ R
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (Std.HashMap.unitOfList l).contains k = l.contains k
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedLeanDiagnosticTag : Inhabited Lean.Lsp.LeanDiagnosticTag
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `Isometry.mapsTo_eball`. -/
Isometry.mapsTo_emetric_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ENNReal), Set.MapsTo f (Metric.eball x r) (Metric.eball (f x) r)
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.comp_id : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η : ApplicativeTransformation F G), η.comp ApplicativeTransformation.idTransformation = η
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_image_Icc : Real.arccos '' Set.Icc (-1) 1 = Set.Icc 0 Real.pi
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.comp_apply : ∀ {M N O : SemiNormedGrp₁} (f : M ⟶ N) (g : N ⟶ O) (r : M.carrier),
  ↑(SemiNormedGrp₁.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) r =
    ↑(SemiNormedGrp₁.Hom.hom g) (↑(SemiNormedGrp₁.Hom.hom f) r)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coeff_smul : ∀ {Γ : Type u_1} {Γ' : Type u_2} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] {R : Type u_7} {V : Type u_8} [inst_4 : Semiring R]
  [inst_5 : AddCommMonoid V] [inst_6 : Module R V] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ' V β) (g : Γ'),
  (s.smul t).hsum.coeff g = ∑ gh ∈ Finset.VAddAntidiagonal g ⋯, s.hsum.coeff gh.1 • t.hsum.coeff gh.2
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.dist_indicatorConstLp_eq_norm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} {t : Set α}
  {ht : MeasurableSet t} {hμt : μ t ≠ ⊤},
  dist (MeasureTheory.indicatorConstLp p hs hμs c) (MeasureTheory.indicatorConstLp p ht hμt c) =
    ‖MeasureTheory.indicatorConstLp p ⋯ ⋯ c‖
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- The distortion of a prepartition is the maximum of the distortions of the boxes of this
prepartition.  -/
BoxIntegral.Prepartition.distortion : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.Prepartition I → [Fintype ι] → NNReal