mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `supPrime_ofDual`. -/
InfPrime.ofDual : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : αᵒᵈ}, InfPrime a → SupPrime (OrderDual.ofDual a)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_performRupCheck_of_assignmentsInvariant : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.AssignmentsInvariant → ∀ (rupHints : Array ℕ), (f.performRupCheck rupHints).1.AssignmentsInvariant
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.filter_eq_iInf : ∀ {𝕜 : Type u_2} {F : Type u_7} {ι : Type u_9} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : Module 𝕜 F] (p : SeminormFamily 𝕜 F ι), p.moduleFilterBasis.filter = ⨅ i, Filter.comap (⇑(p i)) (nhds 0)
-- Lean.Util.LeanOptions
Lean.instFromJsonLeanOptions : Lean.FromJson Lean.LeanOptions
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistribEquivOfBasis_apply_apply : ∀ {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  [inst_4 : ∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i))
  (x : PiTensorProduct R fun i => Module.Dual R (M i)) (x_1 : PiTensorProduct R fun i => M i),
  ((PiTensorProduct.dualDistribEquivOfBasis b) x) x_1 =
    (PiTensorProduct.constantBaseRingEquiv ι R) ((PiTensorProduct.piTensorHomMap x) x_1)
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instIsVerdierLeftLocalizingUnopOfIsVerdierRightLocalizingOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty Cᵒᵖ)
  [A.IsVerdierRightLocalizing B], A.unop.IsVerdierLeftLocalizing B.unop
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquivClass.mk : ∀ {F : Type u_5} {R : outParam (Type u_6)} {A : outParam (Type u_7)} {B : outParam (Type u_8)} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B]
  [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B] [inst_7 : EquivLike F A B]
  [toCoalgHomClass : CoalgHomClass F R A B], CoalgEquivClass F R A B
-- Mathlib.Data.Sign.Defs
SignType.neg_lt_neg_iff : ∀ {a b : SignType}, -a < -b ↔ b < a
-- Mathlib.Data.Complex.Basic
Complex.ofReal_zero : ↑0 = 0
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A domain finitely generated as a module over a field is a field.  -/
IsField.of_isDomain_of_finite : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : CommRing L] [IsDomain L] [inst_3 : Algebra K L]
  [Module.Finite K L], IsField L
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- Applying a doubly stochastic matrix to a vector preserves its sum.  -/
sum_mulVec_of_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R} {x : n → R},
  M ∈ doublyStochastic R n → ∑ i, M.mulVec x i = ∑ i, x i
-- Mathlib.Analysis.Complex.Order
Complex.sq_nonpos_iff : ∀ {z : ℂ}, z ^ 2 ≤ 0 ↔ z.re = 0
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
/-- **Frullani's integral** for functions valued in a complete normed space.
If `f` is locally integrable on `(0, ∞)` with `f x → L` as `x → 0⁺` and `f x → R` as `x → +∞`,
`0 < a` and `0 < b`, and `x ↦ x⁻¹ • (f (a * x) - f (b * x))` is integrable on `(0, ∞)`, then
`∫ x in Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R)`.  -/
Frullani.integral_Ioi_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {L R : E}
  [CompleteSpace E],
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a →
      0 < b →
        Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds L) →
          Filter.Tendsto f Filter.atTop (nhds R) →
            MeasureTheory.IntegrableOn (fun x => x⁻¹ • (f (a * x) - f (b * x))) (Set.Ioi 0) MeasureTheory.volume →
              ∫ (x : ℝ) in Set.Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = Real.log (b / a) • (L - R)
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_apply_2 : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} (p : Prop) (s₁ : σ₁) (s₂ : σ₂), Lean.Order.CompleteLattice.ofProp p s₁ s₂ = p
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.registerBuiltinUpwardPropagator : Lean.Name → Lean.Meta.Grind.Propagator → IO Unit
-- Mathlib.GroupTheory.Focal
AddSubgroup.focalAddSubgroupOf_eq_closure : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G),
  H.focalAddSubgroupOf = AddSubgroup.closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}
-- Init.Data.List.Erase
List.mem_of_mem_eraseP : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, a ∈ List.eraseP p l → a ∈ l
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsTrivialBlock.eq_1 : ∀ {X : Type u_2} (B : Set X), AddAction.IsTrivialBlock B = (B.Subsingleton ∨ B = Set.univ)
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.instPartialOrder : (A : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing A] → [inst_1 : LieRing L] → [inst_2 : Module A L] → PartialOrder (LieRinehartSubalgebra A L)
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.joinPoint : Array Lean.IR.Param → Lean.IR.FnBody → Lean.IR.LocalContextEntry
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.isZero_trivial : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Limits.IsZero (CategoryTheory.Grp.trivial C)
-- Mathlib.GroupTheory.SemidirectProduct
/-- The bijection between the semidirect product and the product.  -/
SemidirectProduct.equivProd : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → N ⋊[φ] G ≃ N × G
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- See also `Ideal.mem_quotient_iff_mem_sup` if the assumption `I ≤ J` is not available.  -/
Ideal.mem_quotient_iff_mem : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided],
  I ≤ J → ∀ {x : R}, (Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J
-- Std.Data.DTreeMap.Raw.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.DTreeMap.Raw.Const.modify : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → (β → β) → Std.DTreeMap.Raw α (fun x => β) cmp
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_neg : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι} [inst_1 : Neg β],
  MeasureTheory.stoppedValue (-u) τ = -MeasureTheory.stoppedValue u τ
-- Aesop.Options.Public
Aesop.instBEqStrategy.beq : Aesop.Strategy → Aesop.Strategy → Bool
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- A Hamiltonian path is a walk `p` that visits every vertex exactly once. Note that while
this definition doesn't contain that `p` is a path, `p.isPath` gives that.  -/
SimpleGraph.Walk.IsHamiltonian : {α : Type u_1} → [DecidableEq α] → {G : SimpleGraph α} → {a b : α} → G.Walk a b → Prop
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.comp_lift : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f]
  {Y' : AlgebraicGeometry.Scheme} (g' : Y' ⟶ Y) (H_1 : Set.range ⇑g ⊆ Set.range ⇑f),
  CategoryTheory.CategoryStruct.comp g' (AlgebraicGeometry.IsOpenImmersion.lift f g H_1) =
    AlgebraicGeometry.IsOpenImmersion.lift f (CategoryTheory.CategoryStruct.comp g' g) ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_eq_get!_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)}, Std.Internal.List.maxKey! l = (Std.Internal.List.maxKey? l).get!
-- Init.Core
/-- If `h : α = β` is a proof of type equality, then `h.mp : α → β` is the induced
"cast" operation, mapping elements of `α` to elements of `β`.

You can prove theorems about the resulting element by induction on `h`, since
`rfl.mp` is definitionally the identity function.
 -/
Eq.mp : {α β : Sort u} → α = β → α → β
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.instIsOpenImmersionMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) [AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.IsOpenImmersion (f ∣_ U)
-- Batteries.Data.PairingHeap
/-- `O(n)`. Fold a monadic function over the tree structure to accumulate a value.  -/
Batteries.PairingHeapImp.Heap.foldTreeM : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → {α : Type u_3} → [Monad m] → β → (α → β → β → m β) → Batteries.PairingHeapImp.Heap α → m β
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
MulRightReflectLE.mk : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : LE M], (∀ {b a₁ a₂ : M}, a₁ * b ≤ a₂ * b → a₁ ≤ a₂) → MulRightReflectLE M
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF →
    t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], (t₁ ∩ t₂).get! k = if t₂.contains k = true then t₁.get! k else default
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0_k_eq_erase0 : ∀ (s : Lean.Grind.AC.Seq), s.erase0_k = s.erase0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.isoMk_hom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ≅ f'.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom)
      CategoryTheory.StructuredArrow.isoMk._auto_1),
  (CategoryTheory.StructuredArrow.isoMk g w).hom.right = g.hom
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.mk.injEq : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (toAffineEquiv : P₁ ≃ᵃ[k] P₂)
  (continuous_toFun : autoParam (Continuous toAffineEquiv.toFun) ContinuousAffineEquiv.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toAffineEquiv.invFun) ContinuousAffineEquiv.continuous_invFun._autoParam)
  (toAffineEquiv_1 : P₁ ≃ᵃ[k] P₂)
  (continuous_toFun_1 : autoParam (Continuous toAffineEquiv_1.toFun) ContinuousAffineEquiv.continuous_toFun._autoParam)
  (continuous_invFun_1 :
    autoParam (Continuous toAffineEquiv_1.invFun) ContinuousAffineEquiv.continuous_invFun._autoParam),
  ({ toAffineEquiv := toAffineEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toAffineEquiv := toAffineEquiv_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 }) =
    (toAffineEquiv = toAffineEquiv_1)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- `Completion.toCompletion` and `Completion.ofCompletion` as an equivalence.  -/
NumberField.InfinitePlace.Completion.equivCompletion : {K : Type u_1} → [inst : Field K] → (v : NumberField.InfinitePlace K) → v.Completion ≃ (↑v).Completion
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.emptyWithCapacity_equiv_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {c : ℕ}, m.WF → ((Std.DHashMap.Raw.emptyWithCapacity c).Equiv m ↔ m.isEmpty = true)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise on `S ∪ {x₀} : Set X`* along some nontrivial
filter, and if the family `𝓕` is equicontinuous at `x₀ : X` within `S`, then the limit is
continuous at `x₀` within `S`.  -/
Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι} [l.NeBot]
  {F : ι → X → α} {f : X → α} {S : Set X} {x₀ : X},
  (∀ x ∈ S, Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))) →
    Filter.Tendsto (fun x => F x x₀) l (nhds (f x₀)) → EquicontinuousWithinAt F S x₀ → ContinuousWithinAt f S x₀
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.containsThenInsert : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a},
  m.WF → (m.containsThenInsert a b).2.WF
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_of_det_mem_nonZeroDivisors : ∀ {m : Type um} {R : Type u_1} [inst : CommRing R] [Nontrivial R] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  {A : Matrix m m R}, A.det ∈ nonZeroDivisors R → A.rank = Fintype.card m
-- Lean.Elab.Tactic.Monotonicity
_private.Lean.Elab.Tactic.Monotonicity.0.Lean.Meta.Monotonicity.applyConst : Lean.MVarId → Lean.Name → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_zero : Nat.bitIndices 0 = []
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_of_pos : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulStrictMono α]
  [MulPosStrictMono α], a < b → c < d → 0 < a → 0 < d → a * c < b * d
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.InfinitePos.not_infiniteNeg : ∀ {x : ℝ*}, x.InfinitePos → ¬x.InfiniteNeg
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.mk.injEq : ∀ (toTop : TopCat) [fintype : Fintype ↑toTop] (toTop_1 : TopCat) (fintype_1 : Fintype ↑toTop_1),
  ({ toTop := toTop, fintype := fintype } = { toTop := toTop_1, fintype := fintype_1 }) =
    (toTop = toTop_1 ∧ fintype ≍ fintype_1)
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [inst_3 : IsNonarchimedeanLocalField K], Finite (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, t.contains a = false → t.getKeyD a fallback = fallback
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_spanningCoe : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), G'.spanningCoe.edgeSet = G'.edgeSet
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_vec_bit0_eq_alt0 : ∀ {α : Type u} {n : ℕ} (x : α) (u : Fin n → α) (i : Fin (n + 1)),
  Matrix.vecCons x u (i + i) = Matrix.vecAlt0 ⋯ (Matrix.vecAppend ⋯ (Matrix.vecCons x u) (Matrix.vecCons x u)) i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.distinct_keys_toList : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → List.Pairwise (fun a b => (a.fst == b.fst) = false) m.toList
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.regular : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ},
  G.IsSRGWith n k ℓ μ → G.IsRegularOfDegree k
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.f.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  (i i_1 : ↥b.support),
  i = i_1 →
    ∀ (a a_1 : ↥b.support ⊕ ι),
      a = a_1 →
        ∀ (a_2 a_3 : ↥b.support ⊕ ι),
          a_2 = a_3 → RootPairing.GeckConstruction.f i a a_2 = RootPairing.GeckConstruction.f i_1 a_1 a_3
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_eq_mul_prod_subtype_ne : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : CommMonoid M] [inst_2 : DecidableEq α] (f : α → M) (a : α),
  ∏ i, f i = f a * ∏ i, f ↑i
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.symm_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.symm.h₂ = -h.h₂
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CStarMatrix.mapₗ.eq_1 : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : Semiring R]
  [inst_1 : Semiring S] {σ : R →+* S} [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid B] [inst_4 : Module R A]
  [inst_5 : Module S B] (f : A →ₛₗ[σ] B),
  CStarMatrix.mapₗ f = { toFun := fun M => M.map ⇑f, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sum_fun_sum : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [inst : Fintype ι] {ι' : Type u_3} [inst_1 : Fintype ι'] {Y : ι' → Ω → ℝ},
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    (∀ (i : ι'), MeasureTheory.MemLp (Y i) 2 μ) →
      ProbabilityTheory.covariance (fun ω => ∑ i, X i ω) (fun ω => ∑ j, Y j ω) μ =
        ∑ i, ∑ j, ProbabilityTheory.covariance (X i) (Y j) μ
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_of_chromaticNumber_ne_top : ∀ {V : Type u} {G : SimpleGraph V}, G.chromaticNumber ≠ ⊤ → G.Colorable G.chromaticNumber.toNat
-- Mathlib.SetTheory.Lists
Lists'.Subset.below : {α : Type u_1} →
  {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop} →
    {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop} → {a a_1 : Lists' α true} → a.Subset a_1 → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.fderivWithin' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s t : Set E},
  f₁ =ᶠ[nhdsWithin x s] f → t ⊆ s → fderivWithin 𝕜 f₁ t =ᶠ[nhdsWithin x s] fderivWithin 𝕜 f t
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The alternating face map complex, as a functor  -/
AlgebraicTopology.alternatingFaceMapComplex : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (ChainComplex C ℕ)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.inv` -/
MeromorphicOn.fun_inv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s : 𝕜 → 𝕜'} {U : Set 𝕜}, MeromorphicOn s U → MeromorphicOn (fun i => (s i)⁻¹) U
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Monomial degree of powers (in a reduced ring)  -/
MonomialOrder.degree_pow : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [IsReduced R] (f : MvPolynomial σ R)
  (n : ℕ), m.degree (f ^ n) = n • m.degree f
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_neg_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E}, LipschitzWith K (-f) ↔ LipschitzWith K f
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.orderBot : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → OrderBot (CategoryTheory.Pretopology C)
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isComplex_smul_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Gal(K/k)}
  {w : NumberField.InfinitePlace K}, (σ • w).IsComplex ↔ w.IsComplex
-- Mathlib.Order.PartialSups
partialSups_eq_sUnion_image : ∀ {α : Type u_1} (s : ℕ → Set α) (n : ℕ), (partialSups s) n = ⋃₀ ↑(Finset.image s (Finset.range (n + 1)))
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.erase : {α : Type u_1} →
  {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → α → Lean.PersistentHashMap α β
-- Init.Data.List.Nat.TakeDrop
/-- This lemma will be renamed to `List.extract_eq_drop_take` as soon as the current deprecated
lemma `List.extract_eq_drop_take` has been removed.
 -/
List.extract_eq_drop_take' : ∀ {α : Type u_1} {l : List α} {start stop : ℕ}, l.extract start stop = List.drop start (List.take stop l)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.prodMk : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G},
  f =o[𝕜; l] k → g =o[𝕜; l] k → (fun x => (f x, g x)) =o[𝕜; l] k
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelEmbedding.total`. -/
RelEmbedding.isTotal : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [Std.Total s], Std.Total r
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseRequestTarget.authority : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.RequestTarget
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.ProbabilityTheory.incrementsToRestrict.eq_1 : ∀ {T : Type u_1} {E : Type u_3} [inst : LinearOrder T] (R : Type u_4) [inst_1 : Semiring R] [inst_2 : AddCommMonoid E]
  [inst_3 : Module R E] [inst_4 : TopologicalSpace E] [inst_5 : ContinuousAdd E] (I : Finset T),
  ProbabilityTheory.incrementsToRestrict✝ R I =
    { toFun := fun x i => ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, x j, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.differentiable_iteratedDeriv_sin : ∀ (n : ℕ), Differentiable ℝ (iteratedDeriv n Real.sin)
-- Mathlib.RingTheory.Unramified.Basic
/-- Being unramified is transported via algebra isomorphisms.  -/
Algebra.Unramified.of_equiv : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} {B : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.Unramified R A] (e : A ≃ₐ[R] B), Algebra.Unramified R B
-- Std.Time.Format.Modifier
Std.Time.Modifier.E.sizeOf_spec : ∀ (presentation : Std.Time.Text), sizeOf (Std.Time.Modifier.E presentation) = 1 + sizeOf presentation
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq_spec : ∀ (x x_1 : Lean.Grind.Linarith.Poly),
  (x == x_1) =
    match x, x_1 with
    | Lean.Grind.Linarith.Poly.nil, Lean.Grind.Linarith.Poly.nil => true
    | Lean.Grind.Linarith.Poly.add a a_1 a_2, Lean.Grind.Linarith.Poly.add b b_1 b_2 =>
      a == b && (a_1 == b_1 && a_2 == b_2)
    | x, x_2 => false
-- Std.Do.SPred.SVal
Std.Do.SVal.getThe_there : ∀ {σ : Type u} {σs : List (Type u)} [inst : Std.Do.SVal.GetTy σ σs] (σ' : Type u) (s : σ'),
  Std.Do.SVal.getThe σ s = Std.Do.SVal.getThe σ