mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Lean.PrettyPrinter.Delaborator
/-- Annotates `stx` with the go-to-def information of `target`.  -/
Lean.PrettyPrinter.Delaborator.annotateGoToDef : Lean.Term → Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.comp : ∀ {C : Type u} {X Y Z : CategoryTheory.FreeMonoidalCategory C} {f f' : X.Hom Y} {g g' : Y.Hom Z},
  CategoryTheory.FreeMonoidalCategory.HomEquiv f f' →
    CategoryTheory.FreeMonoidalCategory.HomEquiv g g' →
      CategoryTheory.FreeMonoidalCategory.HomEquiv (f.comp g) (f'.comp g')
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_uIoo : ∀ (x y : NNReal), ENNReal.ofNNReal '' Set.uIoo x y = Set.uIoo ↑x ↑y
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n →
    (UInt64.ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) UInt64.toUInt32_ofNatClamp_of_le._proof_1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stVar.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) (f : σ → Option (Γ k) → σ),
  Turing.TM2to1.stVar v l (Turing.TM2to1.StAct.peek f) = f v l.head?
-- Mathlib.Order.Atoms
instIsStronglyAtomicOrderDualOfIsStronglyCoatomic : ∀ {α : Type u_4} [inst : Preorder α] [IsStronglyCoatomic α], IsStronglyAtomic αᵒᵈ
-- Mathlib.Algebra.Order.Interval.Basic
Interval.bot_add : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (t : Interval α), ⊥ + t = ⊥
-- Mathlib.Algebra.Category.MonCat.Basic
CategoryTheory.Iso.monCatIsoToMulEquiv.eq_1 : ∀ {X Y : MonCat} (i : X ≅ Y), i.monCatIsoToMulEquiv = (MonCat.Hom.hom i.hom).toMulEquiv (MonCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.Analysis.RCLike.Inner
/-- Weighted inner product giving rise to the L2 norm, denoted as `⟪g, f⟫_[𝕜, w]`.  -/
RCLike.wInner : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    {E : ι → Type u_4} →
      [Fintype ι] →
        [inst : RCLike 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [(i : ι) → InnerProductSpace 𝕜 (E i)] → (ι → ℝ) → ((i : ι) → E i) → ((i : ι) → E i) → 𝕜
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.EStateM.adaptExcept.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) →
        ((a : α) → (s : σ) → motive (EStateM.Result.ok a s)) → motive x
-- Init.Data.Fin.Lemmas
Fin.intCast_def : ∀ {n : ℕ} [inst : NeZero n] (x : ℤ), ↑x = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_not : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {φ : L.Formula α} {v : α → M},
  φ.not.Realize v ↔ ¬φ.Realize v
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
/-- The sigma-algebra generated by a single set `s` is `{∅, s, sᶜ, univ}`.  -/
MeasurableSpace.generateFrom_singleton : ∀ {α : Type u_1} (s : Set α), MeasurableSpace.generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side.  -/
Orientation.tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).tan * ‖y‖ = ‖x‖
-- Mathlib.LinearAlgebra.Ray
/-- A ray (equivalence class of nonzero vectors with common positive multiples) in a module.  -/
Module.Ray : (R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [IsStrictOrderedRing R] → (M : Type u_2) → [inst_3 : AddCommMonoid M] → [Module R M] → Type u_2
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.lowerBound?_of_some : ∀ {α : Type u_1} {cut : α → Ordering} {y : α} {t : RBTree.RBNode α},
  ∃ x, RBTree.RBNode.lowerBound? cut t (some y) = some x
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instLawfulHasSizeInt_1 : Std.Rxo.LawfulHasSize ℤ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂)[k]? = none
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.instFinite : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  [Std.Iterators.Finite α m], Std.Iterators.Finite (Std.Iterators.Types.Drop α m β) m
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.geomSum.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hom_ext : ∀ {X Y : HeytAlg} {f g : X ⟶ Y}, HeytAlg.Hom.hom f = HeytAlg.Hom.hom g → f = g
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- The filter  -/
SummationFilter.filter : {β : Type u_4} → SummationFilter β → Filter (Finset β)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.head_eq_head' : ∀ {F : PFunctor.{uA, uB}} (x : F.M) (n : ℕ), x.head = PFunctor.Approx.head' (x.approx (n + 1))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- This is a helper construction that can be useful when verifying that a category has all
coequalizers. Given `F : WalkingParallelPair ⥤ C`, which is really the same as
`parallelPair (F.map left) (F.map right)`, and a cofork on `F.map left` and `F.map right`,
we get a cocone on `F`.

If you're thinking about using this, have a look at
`hasCoequalizers_of_hasColimit_parallelPair`, which you may find to be an easier way of
achieving your goal.  -/
CategoryTheory.Limits.Cocone.ofCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} →
      CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
          (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) →
        CategoryTheory.Limits.Cocone F
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.realize_one : ∀ {α : Type u_1} {M : Type u_2} {v : α → M} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M],
  FirstOrder.Language.Term.realize v 1 = 1
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.not_bddBelow_coe : ¬BddBelow (Set.range fun x => ↑x)
-- Mathlib.Tactic.Ring.Common
/-- Given a commutative ring `β` with a scalar multiplication action on `α` and a `x : β`, cast
`x` to `α` such that the scalar multiplication turns into normal multiplication. Typically one
can think of `α` as being an algebra over `β`, but this file does not know about `Algebra`s.  -/
Mathlib.Tactic.Ring.Common.RingCompute.cast : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα →
          (v : Lean.Level) →
            (β : Q(Type v)) →
              Q(CommSemiring «$β») →
                (x : Q(SMul «$β» «$α»)) →
                  (x_1 : Q(«$β»)) →
                    Mathlib.Tactic.AtomM
                      ((y : Q(«$α»)) ×
                        Mathlib.Tactic.Ring.Common.ExSum BaseType sα q(«$y») × Q(∀ (a : «$α»), «$x_1» • a = «$y» * a))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : k' ∈ Std.ExtDTreeMap.Const.insertMany t l}, (Std.ExtDTreeMap.Const.insertMany t l).getKey k' h' = k
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The composite of `(X ◁ coprod.inl) : X ⊗ Y ⟶ X ⊗ (Y ⨿ Z)` and
`(∂L X Y Z).inv :  X ⊗ (Y ⨿ Z) ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`
is equal to the left coprojection `coprod.inl : X ⊗ Y ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`.  -/
CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.leftDistrib X Y Z).inv =
    CategoryTheory.Limits.coprod.inl
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.tsupport_derivCLM_subset : ∀ (𝕜 : Type u_2) {F : Type u_8} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : RCLike 𝕜]
  [inst_3 : NormedSpace 𝕜 F] (f : SchwartzMap ℝ F), tsupport ⇑((SchwartzMap.derivCLM 𝕜 F) f) ⊆ tsupport ⇑f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonResolvableCompletionItem : Lean.FromJson Lean.Lsp.ResolvableCompletionItem
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.πProductTo.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) {X : C}
  [inst_1 : CategoryTheory.Limits.HasProduct (P.productToFamily X)] {Y : C} (f f_1 : X ⟶ Y),
  f = f_1 → ∀ (hY : P Y), P.πProductTo f hY = P.πProductTo f_1 hY
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan.0.MeasureTheory.JordanDecomposition.eq_of_posPart_eq_posPart : ∀ {α : Type u_1} [inst : MeasurableSpace α] {j₁ j₂ : MeasureTheory.JordanDecomposition α},
  j₁.posPart = j₂.posPart → j₁.toSignedMeasure = j₂.toSignedMeasure → j₁ = j₂
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- If `f` sends two periodic points `x` and `y` of the same positive period to the same point,
then `x = y`. For a similar statement about points of different periods see `eq_of_apply_eq`.  -/
Function.IsPeriodicPt.eq_of_apply_eq_same : ∀ {α : Type u_1} {f : α → α} {x y : α} {n : ℕ},
  Function.IsPeriodicPt f n x → Function.IsPeriodicPt f n y → 0 < n → f x = f y → x = y
-- Lean.HeadIndex
Lean.HeadIndex.mvar.injEq : ∀ (mvarId mvarId_1 : Lean.MVarId), (Lean.HeadIndex.mvar mvarId = Lean.HeadIndex.mvar mvarId_1) = (mvarId = mvarId_1)
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzeroD_eq_unzero : ∀ {α : Type u} {d : α} {x : WithZero α} (hx : x ≠ 0), WithZero.unzeroD d x = WithZero.unzero hx
-- Aesop.Tree.TreeM
Aesop.TreeM.Context.ruleSet : Aesop.TreeM.Context → Aesop.LocalRuleSet
-- Mathlib.Tactic.Ext
/-- When possible, `ext` lemmas are stated without a full set of arguments. As an example, for bundled
homs `f`, `g`, and `of`, `f.comp of = g.comp of → f = g` is a better `ext` lemma than
`(∀ x, f (of x) = g (of x)) → f = g`, as the former allows a second type-specific extensionality
lemmas to be applied to `f.comp of = g.comp of`.
If the domain of `of` is `ℕ` or `ℤ` and `of` is a `RingHom`, such a lemma could then make the goal
`f (of 1) = g (of 1)`.

For bundled morphisms, there is a `ext` lemma that always applies of the form
`(∀ x, ⇑f x = ⇑g x) → f = g`. When adding type-specific `ext` lemmas like the one above, we want
these to be tried first. This happens automatically since the type-specific lemmas are inevitably
defined later.
 -/
LibraryNote.«partially-applied_ext_lemmas» : Batteries.Util.LibraryNote
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Composition of refinement morphisms of pre-`0`-hypercovers.  -/
CategoryTheory.PreZeroHypercover.Hom.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {F : CategoryTheory.PreZeroHypercover S} →
          {G : CategoryTheory.PreZeroHypercover S} → E.Hom F → F.Hom G → E.Hom G
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_cancel : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a * b / b = a
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Context.quotContext : Lean.MetavarContext.MkBinding.Context → Lean.Name
-- Lean.Expr
/-- Given `e` of the form `f a_1 ... a_n ... a_m`, return `f a_1 ... a_n`.
If `n` is greater than the arity, then return `e`.
 -/
Lean.Expr.getAppPrefix : Lean.Expr → ℕ → Lean.Expr
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.V_id : ∀ (self : TopCat.GlueData.MkCore) (i : self.J), self.V i i = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.dropLast.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.dropLast = p.take (p.length - 1)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The lift of `g` along `f`.  -/
CategoryTheory.Bicategory.LeftLift.lift : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → CategoryTheory.Bicategory.LeftLift f g → (c ⟶ b)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.integrableOn_iff : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.IsFundamentalDomain G t μ →
      ∀ {f : α → E},
        (∀ (g : G) (x : α), f (g • x) = f x) → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f t μ)
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.instOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.SurjectiveOnStalks f
-- Mathlib.LinearAlgebra.Orientation
/-- Composing a basis with a linear equiv gives the negation of that orientation if and only if
the determinant is negative.  -/
Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (e : Module.Basis ι R M) (f : M ≃ₗ[R] M), (e.map f).orientation = -e.orientation ↔ LinearMap.det ↑f < 0
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Naturality lemma for `ΓHomEquiv` analogous to `Adjunction.homEquiv_naturality_right`.  -/
CategoryTheory.Sheaf.ΓHomEquiv_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] {X : A} {F F' : CategoryTheory.Sheaf J A}
  (f : (CategoryTheory.Functor.const Cᵒᵖ).obj X ⟶ F.obj) (g : F ⟶ F'),
  CategoryTheory.Sheaf.ΓHomEquiv (CategoryTheory.CategoryStruct.comp f g.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Sheaf.ΓHomEquiv f) ((CategoryTheory.Sheaf.Γ J A).map g)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opENorm_lsmul_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : NormSMulClass R E] [inst_7 : IsScalarTower 𝕜 R E] [Nontrivial E] {a : R},
  ‖(ContinuousLinearMap.lsmul 𝕜 R) a‖ₑ = ‖a‖ₑ
-- Init.Data.Fin.Lemmas
Fin.exists_fin_zero : ∀ {p : Fin 0 → Prop}, (∃ i, p i) ↔ False
-- Mathlib.Topology.Instances.PNat
PNat.instDiscreteTopology : DiscreteTopology ℕ+
-- Mathlib.NumberTheory.FLT.Three
/-- Given `(S : Solution)`, we have that `λ ^ 2` does not divide `S.a + η * S.b`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ¬(hζ.toInteger - 1) ^ 2 ∣
      FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
        ↑⋯.unit * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S)
-- Init.System.IO
IO.TaskState.finished.sizeOf_spec : sizeOf IO.TaskState.finished = 1
-- Aesop.EMap
Aesop.EMap.insert : {α : Type} → Lean.Expr → α → Aesop.EMap α → Lean.MetaM (Aesop.EMap α)
-- Mathlib.Data.List.Basic
List.mem_map_of_involutive : ∀ {α : Type u} {f : α → α}, Function.Involutive f → ∀ {a : α} {l : List α}, a ∈ List.map f l ↔ f a ∈ l
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.maxDegree_top : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V], ⊤.maxDegree = Fintype.card V - 1
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_comp : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → R) (p : MvPolynomial σ R), f ((MvPolynomial.eval g) p) = MvPolynomial.eval₂ f (⇑f ∘ g) p
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- `Products I` is the type of lists of decreasing elements of `I`, so a typical element is
`[i₁, i₂, ...]` with `i₁ > i₂ > ...`. We order `Products I` lexicographically, so `[] < [i₁, ...]`,
and `[i₁, i₂, ...] < [j₁, j₂, ...]` if either `i₁ < j₁`, or `i₁ = j₁` and `[i₂, ...] < [j₂, ...]`.

Terms `m = [i₁, i₂, ..., iᵣ]` of this type will be used to represent products of the form
`e C i₁ ··· e C iᵣ : LocallyConstant C ℤ` . The function associated to `m` is `m.eval`.
 -/
Profinite.NobelingProof.Products : (I : Type u_1) → [LinearOrder I] → Type (max 0 u_1)
-- Lean.Meta.LazyDiscrTree
/-- Returns candidates from this module in this module that match the expression.

* `moduleRef` is a references to a lazy discriminator tree only containing
this module's definitions.
 -/
Lean.Meta.LazyDiscrTree.findModuleMatches : {α : Type} →
  Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef α → Lean.Expr → Lean.MetaM (Lean.Meta.LazyDiscrTree.MatchResult α)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections],
  CategoryTheory.Limits.HasLimit F
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_top_left : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⊤.relIndex H = 1
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.inner_nonneg_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsPositive → ∀ (x : E), 0 ≤ inner 𝕜 (T x) x
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffOn.comp_contDiff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set F} {g : F → G} {f : E → F},
  ContDiffOn 𝕜 n g s → ContDiff 𝕜 n f → (∀ (x : E), f x ∈ s) → ContDiff 𝕜 n (g ∘ f)
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
/-- The jump of `variationOnFromTo` on the left of a point is given by the distance between the
left limit and the value of the function.  -/
variationOnFromTo.leftLim_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_3} [inst_1 : PseudoMetricSpace E] [CompleteSpace E] {f : α → E}
  {a b : α},
  BoundedVariationOn f Set.univ →
    Function.leftLim (variationOnFromTo f Set.univ a) b =
      variationOnFromTo f Set.univ a b - dist (f b) (Function.leftLim f b)
-- Mathlib.Analysis.SumOverResidueClass
/-- If a decreasing sequence of real numbers is summable on one residue class
modulo `m`, then it is also summable on every other residue class mod `m`.  -/
summable_indicator_mod_iff_summable_indicator_mod : ∀ {m : ℕ} [NeZero m] {f : ℕ → ℝ},
  Antitone f → ∀ {k : ZMod m} (l : ZMod m), Summable ({n | ↑n = k}.indicator f) → Summable ({n | ↑n = l}.indicator f)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
TensorAlgebra.equivFreeAlgebra_symm_ι : ∀ {κ : Type uκ} {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis κ R M) (i : κ),
  (TensorAlgebra.equivFreeAlgebra b).symm (FreeAlgebra.ι R i) = (TensorAlgebra.ι R) (b i)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.toIsHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [self : p.IsStronglyCartesian f φ],
  p.IsHomLift f φ
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
LinearMap.BilinForm.toDual.eq_1 : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate),
  B.toDual b = LinearMap.linearEquivOfInjective B ⋯ ⋯
-- Mathlib.Data.Quot
Quotient.map₂_mk : ∀ {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {γ : Sort u_4} {sc : Setoid γ} (f : α → β → γ)
  (h : ∀ ⦃a₁ a₂ : α⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂ : β⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) (x : α) (y : β),
  Quotient.map₂ f h ⟦x⟧ ⟦y⟧ = ⟦f x y⟧
-- Mathlib.FieldTheory.Normal.Defs
AlgHom.restrictNormal_comp : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} {K₃ : Type u_5} [inst_1 : Field K₁]
  [inst_2 : Field K₂] [inst_3 : Field K₃] [inst_4 : Algebra F K₁] [inst_5 : Algebra F K₂] [inst_6 : Algebra F K₃]
  (ϕ : K₁ →ₐ[F] K₂) (ψ : K₂ →ₐ[F] K₃) (E : Type u_6) [inst_7 : Field E] [inst_8 : Algebra F E] [inst_9 : Algebra E K₁]
  [inst_10 : Algebra E K₂] [inst_11 : Algebra E K₃] [inst_12 : IsScalarTower F E K₁] [inst_13 : IsScalarTower F E K₂]
  [inst_14 : IsScalarTower F E K₃] [inst_15 : Normal F E],
  (ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.tendsto_filterAt_iff : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {ι : Type u_2} {l : Filter ι} {f : ι → Set X} {x : X},
  Filter.Tendsto f l (v.filterAt x) ↔
    (∀ᶠ (i : ι) in l, f i ∈ v.setsAt x) ∧ ∀ ε > 0, ∀ᶠ (i : ι) in l, f i ⊆ Metric.closedBall x ε
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceEditClientCapabilities : Type
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.c_mul_im_sq_le_normSq_denom : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane), (↑g 1 0 * z.im) ^ 2 ≤ Complex.normSq (UpperHalfPlane.denom g ↑z)
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.IsSubterminal.isoDiag_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C} (hA : CategoryTheory.IsSubterminal A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A],
  hA.isoDiag.hom = CategoryTheory.inv (CategoryTheory.Limits.diag A)
-- Lean.Elab.Parallel
/-- Runs a list of TacticM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in completion order (greedily).

The iterator runs in TacticM, and as it yields each result, it updates the TacticM state
to reflect the state when that particular task completed. This means the state is
threaded through the iteration in task completion order.

Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
Lean.Elab.Tactic.TacticM.parIterGreedyWithCancel : {α : Type} →
  List (Lean.Elab.Tactic.TacticM α) →
    Lean.Elab.Tactic.TacticM (BaseIO PUnit.{1} × Std.IterM Lean.Elab.Tactic.TacticM (Except Lean.Exception α))