mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Attach
/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
`a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
but is defined only when all members of `l` satisfy `P`, using the proof
to apply `f`.

We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`.
 -/
Vector.pmap : {α : Type u_1} →
  {β : Type u_2} → {n : ℕ} → {P : α → Prop} → ((a : α) → P a → β) → (xs : Vector α n) → (∀ a ∈ xs, P a) → Vector β n
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsTrivialOn.valuation_algebraMap_le_one : ∀ {Γ₀ : Type u_4} [inst : LinearOrderedCommMonoidWithZero Γ₀] {B : Type u_7} {A : Type u_8} [inst_1 : CommSemiring A]
  [inst_2 : Ring B] [inst_3 : Algebra A B] (v : Valuation B Γ₀) [Valuation.IsTrivialOn A v] (a : A),
  v ((algebraMap A B) a) ≤ 1
-- Mathlib.Order.Filter.Basic
Filter.nontrivial_iff_nonempty : ∀ {α : Type u}, Nontrivial (Filter α) ↔ Nonempty α
-- Mathlib.Data.Sum.Order
OrderIso.sumLexDualAntidistrib_symm_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (a : α),
  (OrderIso.sumLexDualAntidistrib α β).symm (Sum.inr (OrderDual.toDual a)) = OrderDual.toDual (Sum.inl a)
-- Init.Core
Ne.intro : ∀ {α : Sort u} {a b : α}, (a = b → False) → a ≠ b
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistribEquivOfBasis_symm_apply : ∀ {R : Type u_7} {M : Type u_8} {N : Type u_9} {ι : Type u_10} {κ : Type u_11} [inst : DecidableEq ι]
  [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] [inst_3 : Fintype κ] [inst_4 : CommSemiring R]
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : Module R M] [inst_8 : Module R N]
  (b : Module.Basis ι R M) (c : Module.Basis κ R N) (a : Module.Dual R (TensorProduct R M N)),
  (TensorProduct.dualDistribEquivOfBasis b c).symm a = ∑ x, ∑ x_1, a (b x ⊗ₜ[R] c x_1) • b.coord x ⊗ₜ[R] c.coord x_1
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.add_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : AddCommMonoid β]
  [inst_3 : Preorder β] [inst_4 : IsOrderedAddMonoid β] (f g : α →+o β) (a : α), (f + g) a = f a + g a
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.congr_trans : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_7}
  {M'' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : AddCommMonoid M''] [inst_5 : Module R M']
  [inst_6 : Module R M''] (e : M ≃ₗ[R] M') (f : M' ≃ₗ[R] M''),
  LinearMap.BilinForm.congr e ≪≫ₗ LinearMap.BilinForm.congr f = LinearMap.BilinForm.congr (e ≪≫ₗ f)
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended_add : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  (I J : FractionalIdeal M K),
  FractionalIdeal.extended L hf (I + J) = FractionalIdeal.extended L hf I + FractionalIdeal.extended L hf J
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ext : ∀ {K : Type u} [inst : Field K] (A B : ValuationSubring K), (∀ (x : K), x ∈ A ↔ x ∈ B) → A = B
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_filter_containsKey_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getEntry? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = none
-- Mathlib.Topology.Instances.Shrink
Shrink.toEquiv_homeomorph : ∀ (X : Type u) [inst : TopologicalSpace X] [inst_1 : Small.{v, u} X],
  (Shrink.homeomorph X).toEquiv = (equivShrink X).symm.homeomorph.symm
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_Y_ne' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
            P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3 →
              W.add P Q =
                W.dblZ P •
                  ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                      (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                    W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                      (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                    1]
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.map_top : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), LieSubmodule.map f ⊤ = f.range
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.getLastI.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) →
      (Unit → motive []) →
        ((a : α) → motive [a]) →
          ((head b : α) → motive [head, b]) →
            ((head head_1 : α) → (l : List α) → (l = [] → False) → motive (head :: head_1 :: l)) → motive x
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.nextn.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A subgraph of an acyclic graph is acyclic.  -/
SimpleGraph.IsAcyclic.subgraph : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → ∀ (H : G.Subgraph), H.coe.IsAcyclic
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
instHasDetPlusMinusOneAdjoinNegOne : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_3} [inst_2 : CommRing R]
  {𝒢 : Subgroup (GL n R)} [𝒢.HasDetPlusMinusOne], 𝒢.adjoinNegOne.HasDetPlusMinusOne
-- Init.Data.Range.Polymorphic.PRange
Std.Roc.HasRcoIntersection.mk : {α : Type w} → (Std.Roc α → Std.Rco α → Std.Rco α) → Std.Roc.HasRcoIntersection α
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.instInhabitedKey : Inhabited Lean.Meta.DiscrTree.Key
-- Mathlib.LinearAlgebra.Contraction
/-- A linear equivalence between `Dual M ⊗ Dual N` and `Dual (M ⊗ N)` given bases for `M` and `N`.
It sends `f ⊗ g` to the composition of `TensorProduct.map f g` with the natural
isomorphism `R ⊗ R ≃ R`.
 -/
TensorProduct.dualDistribEquivOfBasis : {R : Type u_7} →
  {M : Type u_8} →
    {N : Type u_9} →
      {ι : Type u_10} →
        {κ : Type u_11} →
          [DecidableEq ι] →
            [DecidableEq κ] →
              [Fintype ι] →
                [Fintype κ] →
                  [inst : CommSemiring R] →
                    [inst_1 : AddCommMonoid M] →
                      [inst_2 : AddCommMonoid N] →
                        [inst_3 : Module R M] →
                          [inst_4 : Module R N] →
                            Module.Basis ι R M →
                              Module.Basis κ R N →
                                TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R]
                                  Module.Dual R (TensorProduct R M N)
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.addLeftMono : ∀ {α : Type u} [inst : LE α] [inst_1 : Add α] [c : AddLeftMono α], AddLeftMono αᵒᵈ
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_copy : ∀ {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- `volume` is the canonical measure on `α`.  -/
MeasureTheory.MeasureSpace.volume : {α : Type u_6} → [self : MeasureTheory.MeasureSpace α] → MeasureTheory.Measure α
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.comp_mul_le : ∀ {E : Type u_3} {F : Type u_4} [inst : CommGroup E] [inst_1 : CommGroup F] (p : GroupSeminorm E) (f g : F →* E),
  p.comp (f * g) ≤ p.comp f + p.comp g
-- Init.Data.Array.Lemmas
Array.foldl_add_const : ∀ {α : Type u_1} {xs : Array α} {a b : ℕ}, Array.foldl (fun x x_1 => x + a) b xs = b + a * xs.size
-- Batteries.Recycling.RBTree.WF
/-- The `insert` function is balanced if the input is balanced.
(We lose track of both the color and the black-height of the result,
so this is only suitable for use on the root of the tree.)
 -/
RBTree.RBNode.Balanced.insert : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cmp : α → α → Ordering} {v : α} {t : RBTree.RBNode α},
  t.Balanced c n → ∃ c' n', (RBTree.RBNode.insert cmp t v).Balanced c' n'
-- Mathlib.AlgebraicGeometry.Fiber
/-- The scheme-theoretic fiber of `f` at `y` is homeomorphic to `f ⁻¹' {y}`.  -/
AlgebraicGeometry.Scheme.Hom.fiberHomeo : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (y : ↥Y) → ↥(AlgebraicGeometry.Scheme.Hom.fiber f y) ≃ₜ ↑(⇑f ⁻¹' {y})
-- Mathlib.Analysis.Matrix.Spectrum
/-- rank of a Hermitian matrix is the rank of after diagonalization by the eigenvector unitary  -/
Matrix.IsHermitian.rank_eq_rank_diagonal : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.rank = (Matrix.diagonal hA.eigenvalues).rank
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.image_finsetProd : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : FunLike F α β] [inst_1 : CommMonoid α]
  [inst_2 : CommMonoid β] [MonoidHomClass F α β] (f : F) (m : Finset ι) (s : ι → Set α),
  ⇑f '' ∏ i ∈ m, s i = ∏ i ∈ m, ⇑f '' s i
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.brecOn.go : {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u} →
    {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
      {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
        (t : Lean.Language.Lean.CommandParsedSnapshot) →
          ((t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t) →
            ((t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
                Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t) →
              ((t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
                  Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t) →
                ((t : Task Lean.Language.Lean.CommandParsedSnapshot) →
                    Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t) →
                  motive_1 t ×' t.below
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.beq_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : BEq β] {m₃ m₄ : Std.HashMap.Raw α β},
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Mathlib.Topology.PartitionOfUnity
/-- Each point `x ∈ s` belongs to the interior of `{x | f i x = 1}` for some `i`.  -/
BumpCovering.eventuallyEq_one' : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : BumpCovering ι X s),
  ∀ x ∈ s, ∃ i, ⇑(self.toFun i) =ᶠ[nhds x] 1
-- Init.Data.Int.Order
Int.ne_of_lt : ∀ {a b : ℤ}, a < b → a ≠ b
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.ISize.beq_eq_decide_eq : ∀ {a b : ISize}, (a == b) = decide (a = b)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- The bijection of `Trident.IsLimit.homIso` is natural in `Z`.  -/
CategoryTheory.Limits.Trident.IsLimit.homIso_natural : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) {Z Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt),
  ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) =
    CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {fallback : β} {f : Option β → Option β},
      Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.alter t k f) k fallback =
        (f (Std.DTreeMap.Raw.Const.get? t k)).getD fallback
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- Any injective linear map from `Rⁿ` to `Rᵐ` guarantees `n ≤ m`.  -/
StrongRankCondition.le_of_fin_injective : ∀ {R : Type u} {inst : Semiring R} [self : StrongRankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R),
  Function.Injective ⇑f → n ≤ m
-- Mathlib.MeasureTheory.Integral.CompactlySupported
CompactlySupportedContinuousMap.integralLinearMap_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (μ : MeasureTheory.Measure X) [inst_3 : MeasureTheory.IsFiniteMeasureOnCompacts μ]
  (f : CompactlySupportedContinuousMap X NNReal),
  (CompactlySupportedContinuousMap.integralLinearMap μ) f = NNReal.mk (∫ (x : X), ↑(f x) ∂μ) ⋯
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.balance' : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      (∃ l' r', Ordnode.BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')) →
        Ordnode.Valid' o₁ (l.balance' x r) o₂
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The arrow isomorphism `X □ (∅ ⟶ ⋆) ≅ X` in a CCC with pushouts, an initial object, and a
terminal object.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [CategoryTheory.MonoidalClosed C] →
          (X : CategoryTheory.Arrow C) →
            {I : C} →
              (i : CategoryTheory.Limits.IsInitial I) →
                {T : C} → CategoryTheory.Limits.IsTerminal T → ((X □ CategoryTheory.Arrow.mk (i.to T)) ≅ X)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcCallParams.mk.injEq : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (sessionId : UInt64) (method : Lean.Name)
  (params : Lean.Json) (toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams) (sessionId_1 : UInt64)
  (method_1 : Lean.Name) (params_1 : Lean.Json),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams, sessionId := sessionId, method := method,
        params := params } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1, sessionId := sessionId_1, method := method_1,
        params := params_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1 ∧
      sessionId = sessionId_1 ∧ method = method_1 ∧ params = params_1)
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.mk.injEq : ∀ {α : Type u} (inner inner_1 : Std.HashMap.Raw α Unit), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (hd : CategoryTheory.Limits.IsColimit d),
  (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun K =>
        CategoryTheory.Limits.Cofork.ext
          (CategoryTheory.Iso.refl (((I.ofSigmaCoforkFunctor hc).comp (I.toSigmaCoforkFunctor hc hd)).obj K).pt) ⋯)
      ⋯
-- Mathlib.Tactic.Positivity.Core
/-- Given an expression `e`, use the core method of the `positivity` tactic to prove it positive,
or, failing that, nonnegative; return a Boolean (signalling whether the strict or non-strict
inequality was established) together with the proof as an expression.  -/
Mathlib.Meta.Positivity.bestResult : Lean.Expr → Lean.MetaM (Bool × Lean.Expr)
-- Lean.Elab.DeclNameGen
/-- Given an expression, generates a "base name" for a declaration.
The top-level foralls in `e` are treated as being binders, so use the `...Of...` naming convention.
The current namespace is used to seed the seen expressions with each prefix of the namespace that's a global constant.

Collects all constants that contribute to the name in the `MkInstM` state.
This can be used to decide whether to further transform the generated name;
in particular, this enables checking whether the generated name mentions declarations
from the current module or project.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseName : Lean.Expr → Lean.Elab.Command.NameGen.MkNameM✝ String
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.le_antisymm : ∀ {α : Type u} (self : Std.Packages.LinearOrderOfLEArgs α),
  let this := self.le;
  ∀ (a b : α), a ≤ b → b ≤ a → a = b
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.mul : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      AddMonoidAlgebra.Monic D p → AddMonoidAlgebra.Monic D q → AddMonoidAlgebra.Monic D (p * q)
-- Mathlib.Algebra.Group.PUnit
PUnit.instSub_mathlib.eq_1 : PUnit.instSub_mathlib = { sub := fun x x_1 => PUnit.unit }
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F] (A : adj.toComonad.Coalgebra),
  CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instInhabitedHandleOverlapState.default : Lean.Server.FileWorker.HandleOverlapState✝
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.restrictHom.congr_simp : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [inst_5 : IsDomain C] [inst_6 : Algebra A B]
  [inst_7 : Algebra A C] [inst_8 : Algebra B C] [inst_9 : FaithfulSMul A B] [inst_10 : FaithfulSMul B C]
  [inst_11 : IsScalarTower A B C] [inst_12 : Finite G] [inst_13 : Finite G'] [inst_14 : MulSemiringAction G C]
  [inst_15 : IsGaloisGroup G A C] [inst_16 : MulSemiringAction G' B] [inst_17 : IsGaloisGroup G' A B],
  IsGaloisGroup.restrictHom G G' A B C = IsGaloisGroup.restrictHom G G' A B C
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.liftExtend.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ φ_1 : K.restriction e ⟶ L) (e_φ : φ = φ_1) (hφ : e.HasLift φ),
  e.liftExtend φ hφ = e.liftExtend φ_1 ⋯
-- Lean.Meta.Structure
_private.Lean.Meta.Structure.0.Lean.Meta.etaStruct?.sameParams : Array Lean.Expr → Array Lean.Expr → Lean.MetaM Bool
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
/-- The pairs of parts of a partition `P` which are not `ε`-uniform in a graph `G`. Note that we
dismiss the diagonal. We do not care whether `s` is `ε`-uniform with itself.  -/
Finpartition.nonUniforms : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [Field 𝕜] →
      [LinearOrder 𝕜] →
        [inst : DecidableEq α] →
          {A : Finset α} →
            Finpartition A → (G : SimpleGraph α) → [DecidableRel G.Adj] → 𝕜 → Finset (Finset α × Finset α)
-- Init.Data.UInt.Bitwise
UInt32.toUSize_xor : ∀ (a b : UInt32), (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z}
  [inst_1 : CategoryTheory.IsIso f] [inst_2 : CategoryTheory.IsIso h],
  CategoryTheory.inv (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) (CategoryTheory.inv f)
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Relations.Solution.tensor_var : ∀ {A : Type u} [inst : CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module A M₁] [inst_4 : Module A M₂] {relations₁ : Module.Relations A} {relations₂ : Module.Relations A}
  (solution₁ : relations₁.Solution M₁) (solution₂ : relations₂.Solution M₂) (x : (relations₁.tensor relations₂).G),
  (solution₁.tensor solution₂).var x =
    match x with
    | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂
-- Mathlib.Data.NNReal.Defs
/-- Reinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  -/
Real.toNNReal : ℝ → NNReal
-- Init.Data.Option.Lemmas
Option.filter_map : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} {p : β → Bool},
  Option.filter p (Option.map f x) = Option.map f (Option.filter (p ∘ f) x)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isBasis_affineOpens : ∀ (X : AlgebraicGeometry.Scheme), TopologicalSpace.Opens.IsBasis X.affineOpens
-- Init.Core
/-- If `h : α = β` is a proof of type equality, then `h.mpr : β → α` is the induced
"cast" operation in the reverse direction, mapping elements of `β` to elements of `α`.

You can prove theorems about the resulting element by induction on `h`, since
`rfl.mpr` is definitionally the identity function.
 -/
Eq.mpr : {α β : Sort u} → α = β → β → α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constToList_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β},
  m₁.Equiv m₂ → (Std.DHashMap.Const.toList m₁).Perm (Std.DHashMap.Const.toList m₂)
-- Init.Data.Array.Extract
Array.push_extract_getElem : ∀ {α : Type u_1} {as : Array α} {i j : ℕ} (h : j < as.size), (as.extract i j).push as[j] = as.extract (min i j) (j + 1)
-- Init.Data.UInt.Bitwise
UInt8.or_comm : ∀ (a b : UInt8), a ||| b = b ||| a
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with addition.  -/
ContDiffAt.laplacian_add_nhds : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E},
  ContDiffAt ℝ 2 f₁ x →
    ContDiffAt ℝ 2 f₂ x → Laplacian.laplacian (f₁ + f₂) =ᶠ[nhds x] Laplacian.laplacian f₁ + Laplacian.laplacian f₂
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sum_excenterWeightsUnnorm_empty_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  0 < ∑ i, s.excenterWeightsUnnorm ∅ i