mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_erase : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {a : α},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(m.erase a)).buckets).Perm
      (Std.Internal.List.eraseKey a (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe.inj : ∀ {c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe c₁ c₂ = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe c₁_1 c₂_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminator.typeNames : Lean.Meta.CustomEliminator → Array Lean.Name
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
/-- For `a` selfadjoint, an element commutes with `cfcₙ f a` if it commutes with `a`.

If the base ring is `ℝ` or `ℝ≥0`, see `Commute.cfcₙ_real` or `Commute.cfcₙ_nnreal` which don't
require the `IsSelfAdjoint` hypothesis on `a` (due to the junk value `cfcₙ f a = 0`).  -/
IsSelfAdjoint.commute_cfcₙ : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A},
  IsSelfAdjoint a → Commute a b → ∀ (f : 𝕜 → 𝕜), Commute (cfcₙ f a) b
-- Std.Data.HashMap.Lemmas
Std.HashMap.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {v : β},
  Array.find? (fun a => a.1 == k) m.toArray = some (k', v) ↔ m.getKey? k = some k' ∧ m.get? k = some v
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_sup : ∀ {M : Type u_2} [inst : Mul M] (S₁ S₂ : Subsemigroup Mᵐᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
_private.Mathlib.AlgebraicTopology.FundamentalGroupoid.Product.0.FundamentalGroupoidFunctor.prodToProdTop.match_1.splitter : (A : TopCat) →
  (B : TopCat) →
    (motive :
        (x y :
            ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) ×
              ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) →
          (x ⟶ y) → Sort u_3) →
      (x y :
          ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) ×
            ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) →
        (p : x ⟶ y) →
          ((fst : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)) →
              (snd : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) →
                (fst_1 : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)) →
                  (snd_1 : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) →
                    (p₀ : (fst, snd).1 ⟶ (fst_1, snd_1).1) →
                      (p₁ : (fst, snd).2 ⟶ (fst_1, snd_1).2) → motive (fst, snd) (fst_1, snd_1) (p₀, p₁)) →
            motive x y p
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.comp_isLocallyInjective_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallyInjective J f₁] [CategoryTheory.Presheaf.IsLocallySurjective J f₁],
  CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp f₁ f₂) ↔
    CategoryTheory.Presheaf.IsLocallyInjective J f₂
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In a commutative (possibly non-unital) semiring `R`, `NonUnitalSubsemiring.sumSq R` is
the (possibly non-unital) subsemiring of sums of squares in `R`.
 -/
NonUnitalSubsemiring.sumSq : (T : Type u_2) → [inst : NonUnitalCommSemiring T] → NonUnitalSubsemiring T
-- Init.Data.List.Lemmas
List.map_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : α → β},
  List.map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂
-- Mathlib.Topology.Algebra.Monoid
Submonoid.topologicalClosure.eq_1 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : SeparatelyContinuousMul M] (s : Submonoid M),
  s.topologicalClosure = { carrier := closure ↑s, mul_mem' := ⋯, one_mem' := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.toNat_intMax : ∀ {w : ℕ}, (BitVec.intMax w).toNat = 2 ^ (w - 1) - 1
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {b : β},
  b < ConditionallyCompleteLinearOrderedField.inducedMap α β a ↔ ∃ q, b < ↑q ∧ ↑q < a
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instModule : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        {T : Type u_4} →
          [inst_2 : Semiring R] → (v : AbsoluteValue R S) → [inst_3 : Semiring T] → [Module T R] → Module T (WithAbs v)
-- Mathlib.Order.BooleanAlgebra.Basic
compl_involutive : ∀ {α : Type u} [inst : BooleanAlgebra α], Function.Involutive compl
-- Mathlib.CategoryTheory.Enriched.HomCongr
CategoryTheory.Iso.eHomCongr_trans : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃),
  CategoryTheory.Iso.eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) =
    CategoryTheory.Iso.eHomCongr V α₁ β₁ ≪≫ CategoryTheory.Iso.eHomCongr V α₂ β₂
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.findSomeM?`.

Example:
```lean example
#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
 -/
Std.IterM.Total.findSomeM? : {α β γ : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → [Std.Iterators.Finite α m] → Std.IterM.Total m β → (β → m (Option γ)) → m (Option γ)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_iInf : ∀ {M : Type u_1} [inst : Monoid M] {ι : Sort u_2} (f : ι → Submonoid M), (iInf f).units = ⨅ i, (f i).units
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.descFunLift.eq_6 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (s : CategoryTheory.Limits.Cocone F) (x_1 y : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.descFunLift F s (x_1.mul y) =
    CommRingCat.Colimits.descFunLift F s x_1 * CommRingCat.Colimits.descFunLift F s y
-- Mathlib.Logic.Basic
/-- `Xor a b` is the exclusive-or of propositions.  -/
Xor : Prop → Prop → Prop
-- Lean.Server.References
/-- Adds the contents of an ilean file `ilean` at `path` to `self`.  -/
Lean.Server.References.addIlean : Lean.Server.References → System.FilePath → Lean.Server.Ilean → IO Lean.Server.References
-- Init.Data.List.MinMaxOn
List.maxOn?_eq_if : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α}, List.maxOn? f xs = if h : xs ≠ [] then some (List.maxOn f xs h) else none
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rcc α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Rcc α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.instNonUnitalNormedCommRing : {α : Type u_2} → [NonUnitalNormedCommRing α] → NonUnitalNormedCommRing αᵐᵒᵖ
-- Mathlib.GroupTheory.PushoutI
/-- The indexed pushout of monoids, which is the pushout in the category of monoids,
or the category of groups.  -/
Monoid.PushoutI : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] → [inst_1 : Monoid H] → ((i : ι) → H →* G i) → Type (max (max u_1 u_2) u_3)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.mk.inj : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {inst : Ring k}
  {inst_1 : AddCommGroup V1} {inst_2 : Module k V1} {inst_3 : AddTorsor V1 P1} {inst_4 : AddCommGroup V2}
  {inst_5 : Module k V2} {inst_6 : AddTorsor V2 P2} {toFun : P1 → P2} {linear : V1 →ₗ[k] V2}
  {map_vadd' : ∀ (p : P1) (v : V1), toFun (v +ᵥ p) = linear v +ᵥ toFun p} {toFun_1 : P1 → P2} {linear_1 : V1 →ₗ[k] V2}
  {map_vadd'_1 : ∀ (p : P1) (v : V1), toFun_1 (v +ᵥ p) = linear_1 v +ᵥ toFun_1 p},
  { toFun := toFun, linear := linear, map_vadd' := map_vadd' } =
      { toFun := toFun_1, linear := linear_1, map_vadd' := map_vadd'_1 } →
    toFun = toFun_1 ∧ linear = linear_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Naturality square for morphisms in the inverse direction.  -/
CategoryTheory.Limits.CategoricalPullback.Hom.w'_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (f : x ⟶ y) {Z : B} (h : F.obj y.fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map f.snd) (CategoryTheory.CategoryStruct.comp y.iso.inv h) =
    CategoryTheory.CategoryStruct.comp x.iso.inv (CategoryTheory.CategoryStruct.comp (F.map f.fst) h)
-- Mathlib.Analysis.Analytic.Constructions
/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic.  -/
AnalyticWithinAt.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A} {z : E}
  {s : Set E}, AnalyticWithinAt 𝕜 f s z → ∀ (n : ℕ), AnalyticWithinAt 𝕜 (f ^ n) s z
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, (absConvexHull 𝕜) s = s ↔ AbsConvex 𝕜 s
-- Mathlib.GroupTheory.Congruence.Defs
/-- The equivalence relation underlying a multiplicative congruence relation.  -/
Con.toSetoid : {M : Type u_1} → [inst : Mul M] → Con M → Setoid M
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_eq_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], Cardinal.toENat c = OfNat.ofNat n ↔ c = OfNat.ofNat n
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_mul_comm : ∀ (g h : GL (Fin 2) ℝ) (z : ℂ),
  (UpperHalfPlane.σ g) ((UpperHalfPlane.σ h) z) = (UpperHalfPlane.σ h) ((UpperHalfPlane.σ g) z)
-- Mathlib.Analysis.Real.Spectrum
SpectrumRestricts.lt_nnreal_iff : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] {a : A},
  SpectrumRestricts a ⇑ContinuousMap.realToNNReal →
    ∀ {r : NNReal}, (∀ x ∈ spectrum NNReal a, x < r) ↔ ∀ x ∈ spectrum ℝ a, x < ↑r
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.fst_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C × D), (CategoryTheory.Prod.fst C D).obj X = X.1
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instInfFiniteIndexNormalAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → Min (FiniteIndexNormalAddSubgroup G)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.union_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∪ t₂).Equiv (t₃ ∪ t₄)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.le_add_iff_nonneg_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : AddZeroClass α] [IsAddCommutative α] [AddLeftMono α] {a b : α},
  AddLECancellable a → (a ≤ b + a ↔ 0 ≤ b)
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.iff_forall_not_isBadSeq : ∀ {α : Type u_2} (r : α → α → Prop) (s : Set α),
  s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬Set.PartiallyWellOrderedOn.IsBadSeq r s f
-- Mathlib.Data.Nat.Fib.Basic
Nat.fastFibAux.eq_1 : ∀ (n : ℕ),
  n.fastFibAux =
    Nat.binaryRec (Nat.fib 0, Nat.fib 1)
      (fun b x p =>
        if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
      n
-- Mathlib.Data.Sum.Interval
Finset.inl_mem_sumLexLift : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f₁ : α₁ → β₁ → Finset γ₁} {f₂ : α₂ → β₂ → Finset γ₂} {g₁ : α₁ → β₂ → Finset γ₁} {g₂ : α₁ → β₂ → Finset γ₂}
  {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂} {c₁ : γ₁},
  Sum.inl c₁ ∈ Finset.sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      ∃ a₁ b₂, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ c₁ ∈ g₁ a₁ b₂
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
/-- The standard topological simplex of dimension `1` is homeomorphic to `TopCat.I`.  -/
TopCat.stdSimplexHomeomorphI : ↑(stdSimplex ℝ (Fin 2)) ≃ₜ ↑TopCat.I
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.lIso_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {adj₁ adj₂ : a ⟶ b}
  (e : adj₁ ≅ adj₂), (CategoryTheory.Bicategory.Adj.lIso e).inv = e.inv.τl
-- Mathlib.Data.Int.Cast.Lemmas
/-- `coe : ℤ → α` as an `AddMonoidHom`.  -/
Int.castAddHom : (α : Type u_5) → [inst : AddGroupWithOne α] → ℤ →+ α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).size ≤
    l.length
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.simp : Lean.Meta.Sym.Simp.Simproc
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_smul : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : NormedAddCommGroup E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E]
  [inst_4 : IsBoundedSMul 𝕜 E] [SMulCommClass ℝ 𝕜 E] [inst_6 : CompleteSpace E] (c : 𝕜) (f : ↥(MeasureTheory.Lp E 1 μ)),
  MeasureTheory.L1.integral (c • f) = c • MeasureTheory.L1.integral f
-- Init.Data.String.Defs
String.Internal.intercalateImpl : String → List String → String
-- Lean.Meta.MethodSpecs
Lean.MethodSpecsAttrData.mk.sizeOf_spec : ∀ (clsName : Lean.Name) (privateSpecs : Bool),
  sizeOf { clsName := clsName, privateSpecs := privateSpecs } = 1 + sizeOf clsName + sizeOf privateSpecs
-- Mathlib.Data.ENNReal.Action
ENNReal.instIsOrderedModuleNNReal : IsOrderedModule NNReal ENNReal
-- Mathlib.Algebra.Polynomial.GroupRingAction
/-- An equivariant map induces an equivariant map on polynomials.  -/
MulSemiringActionHom.polynomial : {M : Type u_1} →
  [inst : Monoid M] →
    {P : Type u_2} →
      [inst_1 : CommSemiring P] →
        [inst_2 : MulSemiringAction M P] →
          {Q : Type u_3} →
            [inst_3 : CommSemiring Q] →
              [inst_4 : MulSemiringAction M Q] → (P →+*[M] Q) → Polynomial P →+*[M] Polynomial Q
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.TableEntry.waiters : Lean.Meta.SynthInstance.TableEntry → Array Lean.Meta.SynthInstance.Waiter
-- Init.Data.String.PosRaw
/-- Decreases `p` by `offset`. This is not an `HSub` instance because it should be a relatively
rare operation, so we use a name to make accidental use less likely. To unoffset a position
by the size of a character `c` or string `s`, you can use `p - c` resp. `p - s`.

This should be seen as an operation that converts absolute positions into relative positions.

See also `Pos.Raw.decreaseBy`, which is an "unadvancing" operation.
 -/
String.Pos.Raw.unoffsetBy : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Analysis.Normed.Operator.Extend
/-- Extend a densely defined operator that preserves the norm to a linear isometry equivalence.  -/
LinearEquiv.extendOfIsometry : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {Eₗ : Type u_4} →
        {F : Type u_5} →
          {Fₗ : Type u_6} →
            [inst : NormedField 𝕜] →
              [inst_1 : NormedField 𝕜₂] →
                [inst_2 : AddCommGroup E] →
                  [inst_3 : Module 𝕜 E] →
                    [inst_4 : AddCommGroup F] →
                      [inst_5 : Module 𝕜₂ F] →
                        [inst_6 : NormedAddCommGroup Eₗ] →
                          [inst_7 : NormedSpace 𝕜 Eₗ] →
                            [CompleteSpace Eₗ] →
                              [inst_9 : NormedAddCommGroup Fₗ] →
                                [inst_10 : NormedSpace 𝕜₂ Fₗ] →
                                  [CompleteSpace Fₗ] →
                                    {σ₁₂ : 𝕜 →+* 𝕜₂} →
                                      {σ₂₁ : 𝕜₂ →+* 𝕜} →
                                        [inst_12 : RingHomInvPair σ₁₂ σ₂₁] →
                                          [inst_13 : RingHomInvPair σ₂₁ σ₁₂] →
                                            (f : E ≃ₛₗ[σ₁₂] F) →
                                              (e₁ : E →ₗ[𝕜] Eₗ) →
                                                (e₂ : F →ₗ[𝕜₂] Fₗ) →
                                                  DenseRange ⇑e₁ →
                                                    DenseRange ⇑e₂ → (∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) → Eₗ ≃ₛₗᵢ[σ₁₂] Fₗ
-- Mathlib.Data.Seq.Defs
Stream'.Seq.head_cons : ∀ {α : Type u} (a : α) (s : Stream'.Seq α), (Stream'.Seq.cons a s).head = some a
-- Mathlib.Data.Finset.Range
Finset.exists_nat_subset_range : ∀ (s : Finset ℕ), ∃ n, s ⊆ Finset.range n
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_apply_left : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), (Equiv.swap a b) a = b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k},
  Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl = true →
    compare k a ≠ Ordering.eq → Std.DTreeMap.Internal.Impl.contains a t = true
-- Mathlib.SetTheory.Ordinal.Enum
/-- The set in the definition of `enumOrd` is nonempty.  -/
_private.Mathlib.SetTheory.Ordinal.Enum.0.Ordinal.enumOrd_nonempty : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → ∀ (o : Ordinal.{u}), (s ∩ {b | ∀ c < o, Ordinal.enumOrd s c < b}).Nonempty
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (keys : Array α) (vals : Array β) (hsz : keys.size = vals.size),
  (Lean.PersistentHashMap.Node.collision keys vals hsz).measure = vals.size
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_mul_emod_self_right : ∀ (a b c : ℤ), (a + -(b * c)) % c = a % c
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [inst : AddGroup R], (↑x).im = 0
-- Mathlib.Algebra.Ring.Identities
/-- Sophie Germain's identity, see <https://www.cut-the-knot.org/blue/SophieGermainIdentity.shtml>.
 -/
pow_four_add_four_mul_pow_four : ∀ {R : Type u_1} [inst : CommRing R] {a b : R}, a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.congr_arg : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {f : E ≃ₛₗᵢ[σ₁₂] E₂} {x x' : E}, x = x' → f x = f x'
-- Mathlib.Topology.Algebra.Ring.Ideal
Ideal.coe_connectedComponentOfZero : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Ring R] [inst_2 : IsTopologicalRing R],
  ↑(Ideal.connectedComponentOfZero R) = connectedComponent 0
-- Mathlib.RepresentationTheory.Basic
Representation.ofMulAction_def : ∀ {k : Type u_1} [inst : Semiring k] {G : Type u_2} [inst_1 : Monoid G] {H : Type u_3} [inst_2 : MulAction G H] (g : G),
  (Representation.ofMulAction k G H) g =
    ↑(MonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ
      (Finsupp.lmapDomain k k fun x => g • x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce_nil : ∀ {α : Type u_1} [inst : DecidableEq α], FreeGroup.reduce [] = []
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.ofNat : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : StarRing R] (n : ℕ) [inst_2 : n.AtLeastTwo],
  IsSelfAdjoint (OfNat.ofNat n)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.antidiagonalTuple_two : ∀ (n : ℕ),
  Finset.Nat.antidiagonalTuple 2 n =
    Finset.map (piFinTwoEquiv fun x => ℕ).symm.toEmbedding (Finset.HasAntidiagonal.antidiagonal n)
-- Init.Data.String.TakeDrop
/-- If `pat` matches at `pos`, returns the position after the end of the match.
Returns `none` otherwise.

This function is generic over all currently supported patterns.
 -/
String.Pos.revSkip? : {ρ : Type} → {s : String} → s.Pos → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Option s.Pos
-- Mathlib.Algebra.Group.End
Equiv.Perm.extendDomainHom_injective : ∀ {α : Type u_4} {β : Type u_5} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  Function.Injective ⇑(Equiv.Perm.extendDomainHom f)
-- Lean.Meta.Tactic.Grind.Types
/-- Case-split information.  -/
Lean.Meta.Grind.SplitInfo : Type
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_ofNNRealHom : ⇑ENNReal.ofNNRealHom = WithTop.some
-- Init.Data.SInt.Lemmas
Int16.toInt32_div_of_ne_left : ∀ (a b : Int16), a ≠ Int16.minValue → (a / b).toInt32 = a.toInt32 / b.toInt32
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.AdicCauchySequence.map_comp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u_4} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P),
  AdicCompletion.AdicCauchySequence.map I g ∘ₗ AdicCompletion.AdicCauchySequence.map I f =
    AdicCompletion.AdicCauchySequence.map I (g ∘ₗ f)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The underlying monoid homomorphism.  -/
AddCommGrpCat.Hom.hom' : {A B : AddCommGrpCat} → A.Hom B → ↑A →+ ↑B