mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulLeftMap_eq_mulMap_comp : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Submodule R S}
  (N : Submodule R S) {ι : Type u_1} [inst_3 : DecidableEq ι] (m : ι → ↥M),
  Submodule.mulLeftMap N m =
    M.mulMap N ∘ₗ
      LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.attrArgs : Lean.ParserDescr
-- Mathlib.Data.Finset.Lattice.Fold
Finset.apply_sup_eq_sup_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : SemilatticeSup γ] [inst_3 : OrderBot γ] {s : Finset β} {f : β → α} (g : α → γ),
  (∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → g ⊥ = ⊥ → g (s.sup f) = s.sup (g ∘ f)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instNeg : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] → [inst_7 : TopologicalSpace W] → [IsTopologicalAddGroup W] → Neg (P →ᴬ[R] W)
-- Std.Sync.Channel
/-- Values pushed into the channel that are waiting to be consumed.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.values : {α : Type} → Std.CloseableChannel.Unbounded.State✝ α → Std.Queue α
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- A subspace is complement to its orthogonal complement with respect to some reflexive bilinear
form if and only if that bilinear form restricted on to the subspace is nondegenerate.  -/
LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V} {W : Submodule K V},
  B.IsRefl → ((B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W))
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_congr_ae : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ENNReal},
  X =ᵐ[P] Y → P⁻[X | mΩ] =ᵐ[P] P⁻[Y | mΩ]
-- Lean.Meta.ArgsPacker
/-- Given types `(x : A) → R` and `(z : B) → R`, returns the type
```
(x : A ⊕' B) → R
```
 -/
Lean.Meta.ArgsPacker.Mutual.uncurryTypeND : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edge_mem_incidenceSet_iff : ∀ {V : Type u} (G : SimpleGraph V) {a : V} {e : ↑G.edgeSet}, ↑e ∈ G.incidenceSet a ↔ a ∈ ↑e
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofBitVec : ∀ {b : BitVec 8}, { toBitVec := b }.toUSize = { toBitVec := BitVec.setWidth System.Platform.numBits b }
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- Multiplication on a commutative bialgebra as a bialgebra hom.  -/
Bialgebra.mulBialgHom : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : CommSemiring A] → [inst_2 : Bialgebra R A] → TensorProduct R A A →ₐc[R] A
-- Mathlib.Algebra.Free
FreeAddSemigroup.pure_bind : ∀ {α β : Type u} (f : α → FreeAddSemigroup β) (x : α), pure x >>= f = f x
-- Mathlib.Data.Finset.Sups
Finset.sups_assoc : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t u : Finset α), s ⊻ t ⊻ u = s ⊻ (t ⊻ u)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_inter_le_size_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₂.size
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Set.addConj_mem_fixingAddSubgroup : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {g : M},
  g +ᵥ t = s → ∀ {k : M}, k ∈ fixingAddSubgroup M t → (AddAut.addConj g) k ∈ fixingAddSubgroup M s
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_self : ∀ {a : ℕ}, (↑a).bmod a = 0
-- Lean.Compiler.IR.Basic
Lean.IR.instReprIRType : Repr Lean.IR.IRType
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_one : ∀ {α : Type u_1} [inst : DecidableEq α], FreeGroup.toWord 1 = []
-- Mathlib.RingTheory.Idempotents
/-- A family of orthogonal idempotents lift along nil ideals.  -/
OrthogonalIdempotents.lift_of_isNilpotent_ker : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {I : Type u_3} [Finite I],
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ {e : I → S}, OrthogonalIdempotents e → (∀ (i : I), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
-- Mathlib.Algebra.Ring.Regular
IsRegular.of_ne_zero' : ∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α}, k ≠ 0 → IsRegular k
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.IsProper.isUniquelyCodimOneFace : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} [self : h.IsProper] (s : h.ι),
  (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS
-- Mathlib.Util.Export
Lean.Export.OfState.mk : {α : Type} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      (Lean.Export.State → Lean.Export.Alloc α) →
        ((Lean.Export.Alloc α → Lean.Export.Alloc α) → Lean.Export.State → Lean.Export.State) → Lean.Export.OfState α
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.ExprWithHoles.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (expr : Lean.Expr), sizeOf { ref := ref, expr := expr } = 1 + sizeOf ref + sizeOf expr
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableOn.add_iff_left` -/
DifferentiableOn.fun_add_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 g s → (DifferentiableOn 𝕜 (fun i => f i + g i) s ↔ DifferentiableOn 𝕜 f s)
-- Aesop.RulePattern
/-- A partial map from the level metavariables occurring in the rule to the
pattern's level params.
 -/
Aesop.RulePattern.levelArgMap : Aesop.RulePattern → Array (Option ℕ)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValueCast?.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List ((a : α) × β a) → Sort u_3) →
      (x : List ((a : α) × β a)) →
        (Unit → motive []) → ((k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)) → motive x
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `u` is a family of uniform structures on `γ`, then
`𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i)`.  -/
UniformOnFun.iInf_eq : ∀ {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {𝔖 : Set (Set α)} {u : ι → UniformSpace γ},
  UniformOnFun.uniformSpace α γ 𝔖 = ⨅ i, UniformOnFun.uniformSpace α γ 𝔖
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the composition `η ≫ θ`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.comp₂M : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- Any additive functor `C ⥤ D` to a category `D` with finite biproducts extends to
a functor `Mat_ C ⥤ D`.  -/
CategoryTheory.Mat_.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            [CategoryTheory.Limits.HasFiniteBiproducts D] →
              (F : CategoryTheory.Functor C D) → [F.Additive] → CategoryTheory.Functor (CategoryTheory.Mat_ C) D
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.Subgraph.spanningCoe_sup_edge_le : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} {H : (G ⊔ SimpleGraph.edge s t).Subgraph}, ¬H.Adj s t → H.spanningCoe ≤ G
-- Mathlib.NumberTheory.SmoothNumbers
/-- A `k`-smooth number can be written as a square times a product of distinct primes `< k`.  -/
Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers : ∀ {n k : ℕ}, n ∈ k.smoothNumbers → ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id
-- Lean.Parser.Syntax
Lean.Parser.optPrecedence : Lean.Parser.Parser
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_univ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f Set.univ x ↔ ContDiffAt 𝕜 n f x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientGroup.instDiscreteMeasurableSpace : ∀ {G : Type u_6} [inst : Group G] [inst_1 : MeasurableSpace G] [DiscreteMeasurableSpace G] (S : Subgroup G),
  DiscreteMeasurableSpace (G ⧸ S)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.preimage_comap_zeroLocus_aux : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (s : Set R),
  PrimeSpectrum.comap f ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (⇑f '' s)
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_sub_right : ∀ {M : Type u} [inst : SubNegMonoid M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M),
  edist (a - c) (b - c) = edist a b
-- Init.Data.Nat.Lemmas
Nat.one_mod : ∀ (n : ℕ), 1 % (n + 2) = 1
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `locallyPathConnectedSpace_iff_pathComponentIn_mem_nhds`.

---

A space is locally path-connected iff all path components of open subsets are neighbourhoods.  -/
locPathConnectedSpace_iff_pathComponentIn_mem_nhds : ∀ {X : Type u_4} [inst : TopologicalSpace X],
  LocallyPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → x ∈ u → pathComponentIn u x ∈ nhds x
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- This ext lemma changes equalities on `αᵐᵒᵖ →+ β` to equalities on `α →+ β`.
This is useful because there are often ext lemmas for specific `α`s that will apply
to an equality of `α →+ β` such as `Finsupp.addHom_ext'`.  -/
AddMonoidHom.mul_op_ext : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] (f g : αᵐᵒᵖ →+ β),
  f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom → f = g
-- Init.Data.Int.Order
Int.le_def : ∀ {a b : ℤ}, a ≤ b ↔ (b - a).NonNeg
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.coe_toLinearEquiv : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : LinearMap.GeneralLinearGroup R M), ⇑f.toLinearEquiv = ⇑↑f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.minEntry!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minEntry! = t₂.minEntry!
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.ext : ∀ {x y : BoxIntegral.IntegrationParams},
  x.bRiemann = y.bRiemann → x.bHenstock = y.bHenstock → x.bDistortion = y.bDistortion → x = y
-- Mathlib.Order.SupIndep
iSupIndep.mono : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {s t : ι → α}, iSupIndep s → t ≤ s → iSupIndep t
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.sum_comp' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R S : C}
  {J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : J → (Q ⟶ R)) (h : R ⟶ S),
  CategoryTheory.CategoryStruct.comp (∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (g j)) h =
    ∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (CategoryTheory.CategoryStruct.comp (g j) h)
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
DifferentiableOn.inversion : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] {c x : E → F} {R : E → ℝ} {s : Set E},
  DifferentiableOn ℝ c s →
    DifferentiableOn ℝ R s →
      DifferentiableOn ℝ x s →
        (∀ a ∈ s, x a ≠ c a) → DifferentiableOn ℝ (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s
-- Lean.Parser.Term.Basic
Lean.Parser.Term.strictImplicitLeftBracket.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_mul : ∀ {a b : ISize} (h : System.Platform.numBits = 32), (a * b).toBitVec32 h = a.toBitVec32 h * b.toBitVec32 h
-- Mathlib.CategoryTheory.Action.Monoidal
Action.leftUnitor_inv_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.V).inv
-- Mathlib.CategoryTheory.Monoidal.Rigid.Functor
CategoryTheory.rightDualFunctor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.RightRigidCategory C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.rightDualFunctor C).map f = fᘁ.op.mop
-- Init.Data.Float.Float32
/-- Non-strict inequality of floating-point numbers. Typically used via the `≤` operator.
 -/
Float32.le : Float32 → Float32 → Bool
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodCongr.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : MulOneClass N'] [inst_3 : MulOneClass M'] (f : M ≃* M') (g : N ≃* N'),
  f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_mul' := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {a k : α} {v : β k}, (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instCompleteLattice : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CompleteLattice (CategoryTheory.Precoverage C)
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.isClosedMap_smul : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] {c : M}, IsUnit c → IsClosedMap fun x => c • x
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.differentiable_mulExpNegMulSq : ∀ {ε : ℝ}, Differentiable ℝ ε.mulExpNegMulSq
-- Mathlib.Control.LawfulFix
Part.Fix.approx_mono : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) ⦃i j : ℕ⦄,
  i ≤ j → Part.Fix.approx (⇑f) i ≤ Part.Fix.approx (⇑f) j
-- Mathlib.Data.Finset.SymmDiff
Finset.symmDiff_subset_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, symmDiff s t ⊆ s ∪ t
-- Aesop.Tree.Data
Aesop.instDecidableEqRappId.decEq : (x x_1 : Aesop.RappId) → Decidable (x = x_1)
-- Mathlib.Data.Finset.Insert
Finset.cons_induction_on : ∀ {α : Type u_3} {motive : Finset α → Prop} (s : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)) → motive s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.MonoidalCategory.DayFunctor C V} {α β : F ⟶ G}, α = β ↔ α.natTrans = β.natTrans
-- Mathlib.RingTheory.PrincipalIdealDomain
PrincipalIdealRing.isMaximal_of_irreducible : ∀ {R : Type u} [inst : CommSemiring R] [IsPrincipalIdealRing R] {p : R}, Irreducible p → Ideal.IsMaximal (R ∙ p)
-- Init.Prelude
EStateM.instInhabited : {ε σ α : Type u} → [Inhabited ε] → Inhabited (EStateM ε σ α)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportKind.mk : Bool → Bool → Lean.Lsp.LeanImportMetaKind → Lean.Lsp.LeanImportKind
-- Mathlib.Data.List.Forall2
List.forall₂_nil_left_iff : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List β}, List.Forall₂ R [] l ↔ l = []
-- Init.Data.UInt.Basic
/-- The modulo operator for 16-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `UInt16.mod 5 2 = 1`
* `UInt16.mod 4 2 = 0`
* `UInt16.mod 4 0 = 4`
 -/
UInt16.mod : UInt16 → UInt16 → UInt16
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_mul : ∀ {R : Type u_1} [inst : Semiring R] (I : Ideal R), Submodule.annihilator I * I = ⊥
-- Lean.Meta.Tactic.UnifyEq
Lean.Meta.UnifyEqResult.mk : Lean.MVarId → Lean.Meta.FVarSubst → ℕ → Lean.Meta.UnifyEqResult
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Point reflection in `x` as an affine isometric automorphism.  -/
AffineIsometryEquiv.pointReflection : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] → [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → P → P ≃ᵃⁱ[𝕜] P
-- Mathlib.Data.List.Nodup
List.nodup_middle : ∀ {α : Type u} {a : α} {l₁ l₂ : List α}, (l₁ ++ a :: l₂).Nodup ↔ (a :: (l₁ ++ l₂)).Nodup
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Reversing the order of three points preserves affine independence.  -/
AffineIndependent.reverse_of_three : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, AffineIndependent k ![p₁, p₂, p₃] → AffineIndependent k ![p₃, p₂, p₁]
-- Mathlib.MeasureTheory.Measure.Restrict
/-- See also `Measure.ae_sum_iff`.  -/
MeasureTheory.ae_finsetSum_measure_iff : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {p : α → Prop} {s : Finset ι}
  {μ : ι → MeasureTheory.Measure α}, (∀ᵐ (x : α) ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ i, p x
-- Mathlib.Order.Copy
GeneralizedHeytingAlgebra.copy.congr_simp : ∀ {α : Type u} (c c_1 : GeneralizedHeytingAlgebra α) (e_c : c = c_1) (le le_1 : α → α → Prop) (e_le : le = le_1)
  (eq_le : le = LE.le) (top top_1 : α) (e_top : top = top_1) (eq_top : top = ⊤) (sup sup_1 : α → α → α)
  (e_sup : sup = sup_1) (eq_sup : sup = max) (inf inf_1 : α → α → α) (e_inf : inf = inf_1) (eq_inf : inf = min)
  (himp himp_1 : α → α → α) (e_himp : himp = himp_1) (eq_himp : himp = HImp.himp),
  c.copy le eq_le top eq_top sup eq_sup inf eq_inf himp eq_himp = c_1.copy le_1 ⋯ top_1 ⋯ sup_1 ⋯ inf_1 ⋯ himp_1 ⋯
-- Batteries.Data.Array.Match
Array.Matcher.Iterator.mk : {σ : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {α : Type u_1} →
      [inst : BEq α] →
        {m : Array.Matcher α} →
          [inst_1 : Std.Iterator σ n α] → Std.IterM n α → Fin (m.table.size + 1) → Array.Matcher.Iterator σ n α m
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∪ t₂).getKey? k = t₁.getKey? k
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.Linter.mk.injEq : ∀ (test : Lean.Name → Lean.MetaM (Option Lean.MessageData)) (noErrorsFound errorsFound : Lean.MessageData)
  (isFast : Bool) (test_1 : Lean.Name → Lean.MetaM (Option Lean.MessageData))
  (noErrorsFound_1 errorsFound_1 : Lean.MessageData) (isFast_1 : Bool),
  ({ test := test, noErrorsFound := noErrorsFound, errorsFound := errorsFound, isFast := isFast } =
      { test := test_1, noErrorsFound := noErrorsFound_1, errorsFound := errorsFound_1, isFast := isFast_1 }) =
    (test = test_1 ∧ noErrorsFound = noErrorsFound_1 ∧ errorsFound = errorsFound_1 ∧ isFast = isFast_1)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- If `e : M ≃+ N` is an additive equivalence between two additive monoids, then
`AddMonoidAlgebra.domCongr e` is an algebra equivalence between their additive monoid algebras.  -/
AddMonoidAlgebra.domCongr : (R : Type u_1) →
  (A : Type u_4) →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddMonoid M] → [inst_4 : AddMonoid N] → M ≃+ N → AddMonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra A N
-- Mathlib.Data.Sigma.Lex
PSigma.lex_iff : ∀ {ι : Sort u_1} {α : ι → Sort u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : (i : ι) ×' α i},
  PSigma.Lex r s a b ↔ r a.fst b.fst ∨ ∃ (h : a.fst = b.fst), s b.fst (h ▸ a.snd) b.snd
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- If a sequence `g` converges to some `b`, then the sequence of constant functions
`fun n ↦ fun a ↦ g n` converges to the constant function `fun a ↦ b` on any set `s`.  -/
Filter.Tendsto.tendstoUniformlyOnFilter_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {p : Filter ι} {g : ι → β} {b : β},
  Filter.Tendsto g p (nhds b) → ∀ (p' : Filter α), TendstoUniformlyOnFilter (fun n x => g n) (fun x => b) p p'
-- Mathlib.Data.Real.Embedding
Archimedean.ratLt_nonempty : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x : M), (Archimedean.ratLt x).Nonempty
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.det_toMatrix_prod : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n]
  (L : List (Matrix.TransvectionStruct n R)), (List.map Matrix.TransvectionStruct.toMatrix L).prod.det = 1
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateCol_add : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R)
  (j : n) (u v : n → R), (M.updateCol j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det
-- Mathlib.CategoryTheory.FinCategory.Basic
CategoryTheory.finCategoryDiscreteOfFintype : (J : Type v) → [Fintype J] → CategoryTheory.FinCategory (CategoryTheory.Discrete J)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fst_snd_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'}
  {ν : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  {X : Ω → ℝ} {Y : Ω' → ℝ},
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 ν → ProbabilityTheory.covariance (fun p => X p.1) (fun p => Y p.2) (μ.prod ν) = 0
-- Mathlib.Order.Hom.Basic
/-- `Subtype.val` as a bundled monotone function.  -/
OrderHom.Subtype.val : {α : Type u_2} → [inst : Preorder α] → (p : α → Prop) → Subtype p →o α
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineMap.lineMap_vadd : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (v v' : V₁) (p : P₁) (c : k),
  (AffineMap.lineMap v v') c +ᵥ p = (AffineMap.lineMap (v +ᵥ p) (v' +ᵥ p)) c
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  (X.cokernelSequenceCycles f g fg h n).X₂ = (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.coe_smulRight : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : Semiring S] [inst_6 : Module R S]
  [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M), ⇑(f.smulRight x) = fun c => f c • x