mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.App
/-- Valid named arguments found while traversing the function's type.  -/
Lean.Elab.Term.ElabAppArgs.State.foundNamedArgs : Lean.Elab.Term.ElabAppArgs.State → Array Lean.Name
-- Mathlib.Order.Basic
LE.le.gt_or_le : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, a ≤ b → ∀ (c : α), a < c ∨ c ≤ b
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.IsSplitEqualizer.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X} [inst_1 : SizeOf C]
  (leftRetraction : X ⟶ W) (rightRetraction : Y ⟶ X)
  (condition :
    autoParam (CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
      CategoryTheory.IsSplitEqualizer.condition._autoParam)
  (ι_leftRetraction :
    autoParam (CategoryTheory.CategoryStruct.comp ι leftRetraction = CategoryTheory.CategoryStruct.id W)
      CategoryTheory.IsSplitEqualizer.ι_leftRetraction._autoParam)
  (bottom_rightRetraction :
    autoParam (CategoryTheory.CategoryStruct.comp g rightRetraction = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.IsSplitEqualizer.bottom_rightRetraction._autoParam)
  (top_rightRetraction :
    autoParam
      (CategoryTheory.CategoryStruct.comp f rightRetraction = CategoryTheory.CategoryStruct.comp leftRetraction ι)
      CategoryTheory.IsSplitEqualizer.top_rightRetraction._autoParam),
  sizeOf
      { leftRetraction := leftRetraction, rightRetraction := rightRetraction, condition := condition,
        ι_leftRetraction := ι_leftRetraction, bottom_rightRetraction := bottom_rightRetraction,
        top_rightRetraction := top_rightRetraction } =
    1 + sizeOf leftRetraction + sizeOf rightRetraction + sizeOf condition + sizeOf ι_leftRetraction +
        sizeOf bottom_rightRetraction +
      sizeOf top_rightRetraction
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_cos_sq : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.cos x ^ 2 = (Real.cos b * Real.sin b - Real.cos a * Real.sin a + b - a) / 2
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.length_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keys.length = m.size
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} [inst_3 : Inhabited (β k)],
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.ofList l cmp).get! k = default
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.nsmul_subset : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {H : AddSubgroup G} {n : ℕ}, s ⊆ ↑H → n • s ⊆ ↑H
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.joinpoint.inj : ∀ {name : Lean.Name} {params : Array (Lean.Elab.Term.Do.Var × Bool)} {body k : Lean.Elab.Term.Do.Code}
  {name_1 : Lean.Name} {params_1 : Array (Lean.Elab.Term.Do.Var × Bool)} {body_1 k_1 : Lean.Elab.Term.Do.Code},
  Lean.Elab.Term.Do.Code.joinpoint name params body k = Lean.Elab.Term.Do.Code.joinpoint name_1 params_1 body_1 k_1 →
    name = name_1 ∧ params = params_1 ∧ body = body_1 ∧ k = k_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_Ψ₃_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 3 ≠ 0 → W.Ψ₃.coeff 4 ≠ 0
-- Lean.Meta.Tactic.Grind.EMatch
/-- Context for the E-matching monad.  -/
Lean.Meta.Grind.EMatch.Context : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_nat_mul_pi : ∀ (n : ℕ), Real.sin (↑n * Real.pi) = 0
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_abs_mod_two : ∀ (a : ℤ), ↑|a| = ↑a
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.isUnits_det_units : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : (Matrix n n α)ˣ),
  IsUnit (↑A).det
-- Mathlib.Algebra.Homology.Augment
/-- Augmenting a truncated complex with the original object and morphism is isomorphic
(with components the identity) to the original complex.
 -/
ChainComplex.augmentTruncate : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (C : ChainComplex V ℕ) → (ChainComplex.truncate.obj C).augment (C.d 1 0) ⋯ ≅ C
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAt.sum : ∀ {𝕜 : 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] {x : E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F} {A' : ι → E →L[𝕜] F},
  (∀ i ∈ u, HasFDerivAt (A i) (A' i) x) → HasFDerivAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x / a) ⁻¹' Set.Ico b c = Set.Ico (b * a) (c * a)
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.of_isIdempotentElem : ∀ {R : Type u_1} [inst : Ring R] {e : R}, IsIdempotentElem e → CompleteOrthogonalIdempotents ![e, 1 - e]
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.weightedHomogeneousComponent_of_weightedOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {w : σ → ℕ} {f : MvPowerSeries σ R} {p : ℕ},
  ↑p = MvPowerSeries.weightedOrder w f → (MvPowerSeries.weightedHomogeneousComponent w p) f ≠ 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `OrderedRing` instance with `Preorder`  -/
Lean.Meta.Grind.Arith.Linear.Struct.orderedRingInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {l : List α}, (↑m).size ≤ (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).size
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (t.alter k f).isEmpty = false →
        ((t.alter k f).minKey! = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.factorThruImageSubobject.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  CategoryTheory.Limits.factorThruImageSubobject f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f)
      (CategoryTheory.Limits.imageSubobjectIso f).inv
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.coe_mulSingle : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → MulOneClass (f i)] (i : I),
  ⇑(MonoidHom.mulSingle f i) = Pi.mulSingle i
-- Mathlib.RingTheory.ClassGroup.Basic
/-- Send a nonzero integral ideal to an invertible fractional ideal.  -/
FractionalIdeal.mk0 : {R : Type u_1} →
  (K : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsFractionRing R K] →
            [IsDomain R] →
              [inst_5 : IsDedekindDomain R] → ↥(nonZeroDivisors (Ideal R)) →* (FractionalIdeal (nonZeroDivisors R) K)ˣ
-- Lean.MetavarContext
Lean.MetavarKind.noConfusionType : Sort v✝ → Lean.MetavarKind → Lean.MetavarKind → Sort v✝
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressItemFast : String → Lean.Lsp.ResolvableCompletionItem → String
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Context.config : Lean.Meta.Try.Collector.Context → Lean.Try.Config
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- `Finsupp.mapDomain` as a `LinearEquiv`.  -/
Finsupp.mapDomain.linearEquiv : {α : Type u_1} →
  (M : Type u_2) →
    (R : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {α' : Type u_9} → α ≃ α' → (α →₀ M) ≃ₗ[R] α' →₀ M
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.initialOfCorepresentableBy_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type u_1)} {X : C}
  (h : F.CorepresentableBy X), (CategoryTheory.Functor.Elements.initialOfCorepresentableBy h).fst = X
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.disjoint_rootSpan_ker_rootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [IsDomain R] [inst_5 : Module R M] [inst_6 : Module R N]
  (P : RootPairing ι R M N) [P.IsAnisotropic], Disjoint (P.rootSpan R) (LinearMap.ker P.RootForm)
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.forgetToTop_full : (CategoryTheory.forget₂ AlexDisc TopCat).Full
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.opFunctor_map_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X ⟶ Y),
  (CategoryTheory.Square.opFunctor.map φ).τ₄ = φ.unop.τ₁.op
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_sdiv : ∀ (a b : BitVec 32), Int32.ofBitVec (a.sdiv b) = Int32.ofBitVec a / Int32.ofBitVec b
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.lift₃NatTrans.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_13, u_13} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (L₃ : CategoryTheory.Functor C₃ D₃) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) (W₃ : CategoryTheory.MorphismProperty C₃) [inst_7 : L₁.IsLocalization W₁]
  [inst_8 : L₂.IsLocalization W₂] [inst_9 : L₃.IsLocalization W₃] [inst_10 : W₁.ContainsIdentities]
  [inst_11 : W₂.ContainsIdentities] [inst_12 : W₃.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)))
  [inst_13 : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁']
  [inst_14 : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (τ τ_1 : F₁ ⟶ F₂),
  τ = τ_1 →
    CategoryTheory.Localization.lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' τ =
      CategoryTheory.Localization.lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' τ_1
-- Std.Http.Data.Version
/-- `HTTP/2.0`
 -/
Std.Http.Version.v20 : Std.Http.Version
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_mono : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) {s t : Set α},
  MeasurableSet s → s ∩ p.support ⊆ t → p.toMeasure s ≤ p.toMeasure t
-- Init.Data.Vector.Lemmas
Vector.eraseIdx_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {h : xs.size = n} {i : ℕ} (h' : i < n),
  (Vector.mk xs h).eraseIdx i h' = Vector.mk (xs.eraseIdx i ⋯) ⋯
-- Mathlib.Data.List.Cycle
Cycle.nil.eq_1 : ∀ {α : Type u_1}, Cycle.nil = ↑[]
-- Init.Meta.Defs
Lean.Syntax.find? : Lean.Syntax → (Lean.Syntax → Bool) → Option Lean.Syntax
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.singleton_add : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidableEq α] {s : Finset α} (a : α), {a} + s = a +ᵥ s
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_zero : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F],
  ContinuousLinearMapWOT.ofCLM 0 = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- An equality constraint and its justification/proof.  -/
Lean.Meta.Grind.Arith.Linear.EqCnstr : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negDblY_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Equation P →
    P 2 ≠ 0 →
      W.negDblY P =
        (-(MvPolynomial.eval P) W.polynomialX *
              ((MvPolynomial.eval P) W.polynomialX ^ 2 -
                      W.a₁ * (MvPolynomial.eval P) W.polynomialX * P 2 * (P 1 - W.negY P) -
                    W.a₂ * P 2 ^ 2 * (P 1 - W.negY P) ^ 2 -
                  2 * P 0 * P 2 * (P 1 - W.negY P) ^ 2 -
                P 0 * P 2 * (P 1 - W.negY P) ^ 2) +
            P 1 * P 2 ^ 2 * (P 1 - W.negY P) ^ 3) /
          P 2 ^ 2
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.DTreeMap.Raw.Const.unitOfList l cmp).getKey! k = default
-- Mathlib.Analysis.Convex.Function
/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic
structures aren't necessarily compatible), in order to prove that it is strictly concave it suffices
to verify the inequality `a • f x + b • f y < f (a • x + b • y)` for `x < y` and positive `a`, `b`.
The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order.  -/
LinearOrder.strictConcaveOn_of_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β]
  [inst_7 : LinearOrder E] {s : Set E} {f : E → β},
  Convex 𝕜 s →
    (∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)) →
      StrictConcaveOn 𝕜 s f
-- Mathlib.Algebra.Group.Equiv.Defs
/-- **Alias** of `EmbeddingLike.map_ne_zero_iff`. -/
AddEquivClass.map_ne_zero_iff : ∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M}, f x ≠ 0 ↔ x ≠ 0
-- Mathlib.Data.NNRat.BigOperators
NNRat.cast_multisetSum : ∀ {K : Type u_2} [inst : DivisionSemiring K] [CharZero K] (s : Multiset ℚ≥0), ↑s.sum = (Multiset.map NNRat.cast s).sum
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The complex moment-generating function of a random variable with Gaussian distribution
with mean `μ` and variance `v` is given by `z ↦ exp (z * μ + v * z ^ 2 / 2)`.  -/
ProbabilityTheory.complexMGF_gaussianReal : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {p : MeasureTheory.Measure Ω} {μ : ℝ} {v : NNReal} {X : Ω → ℝ},
  MeasureTheory.Measure.map X p = ProbabilityTheory.gaussianReal μ v →
    ∀ (z : ℂ), ProbabilityTheory.complexMGF X p z = Complex.exp (z * ↑μ + ↑↑v * z ^ 2 / 2)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.spectralRadius_pow_le : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (n : ℕ),
  n ≠ 0 → spectralRadius 𝕜 a ^ n ≤ spectralRadius 𝕜 (a ^ n)
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_set_mk : ∀ {K : Type u} [inst : DivisionRing K] (S : Subring K) (h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier),
  ↑{ toSubring := S, inv_mem' := h } = ↑S
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
/-- A limit kernel fork in the opposite category gives a colimit cokernel cofork
in the original category  -/
CategoryTheory.Limits.KernelFork.IsLimit.ofιUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K X Y : Cᵒᵖ} →
        (i : K ⟶ X) →
          {f : X ⟶ Y} →
            (w : CategoryTheory.CategoryStruct.comp i f = 0) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i w) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ i.unop ⋯)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l)[k']! = v
-- Lean.Environment
Lean.OLeanLevel.ofNat_ctorIdx : ∀ (x : Lean.OLeanLevel), Lean.OLeanLevel.ofNat x.ctorIdx = x
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_mono_left : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  {I J : Submodule R A} {N : Submodule R M}, I ≤ J → I • N ≤ J • N
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier_subset_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.cellFrontier n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑n)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.flat_and_surjective_SpecMap_iff : ∀ {R S : CommRingCat} (f : R ⟶ S),
  AlgebraicGeometry.Flat (AlgebraicGeometry.Spec.map f) ∧ AlgebraicGeometry.Surjective (AlgebraicGeometry.Spec.map f) ↔
    (CommRingCat.Hom.hom f).FaithfullyFlat
-- Mathlib.Topology.Order.MonotoneContinuity
OrderIso.coe_toHomeomorph : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [inst_4 : OrderTopology α] [inst_5 : OrderTopology β] (e : α ≃o β), ⇑e.toHomeomorph = ⇑e
-- Mathlib.ModelTheory.Order
_private.Mathlib.ModelTheory.Order.0.FirstOrder.Language.orderLHom.match_1.eq_1 : ∀ (motive : (x : ℕ) → FirstOrder.Language.order.Relations x → Sort u_1)
  (h_1 : Unit → motive 2 FirstOrder.Language.orderRel.le),
  (match 2, FirstOrder.Language.orderRel.le with
    | .(2), FirstOrder.Language.orderRel.le => h_1 ()) =
    h_1 ()
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.restrict_sub : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {H : Type u_6} [inst_10 : Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (φ : H →* G)
  (f g : ContIntertwiningMap π π'),
  ContIntertwiningMap.restrict φ (f - g) = ContIntertwiningMap.restrict φ f - ContIntertwiningMap.restrict φ g
-- Init.Data.UInt.Lemmas
UInt32.ofNatTruncate_bitVecToNat : ∀ (n : BitVec 32), UInt32.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.Data.Nat.Log
/-- An auxiliary definition for `Nat.log`.

For `b > 1`, `n ≠ 0`, `n < b ^ fuel`, `Nat.log.go n b fuel = (n / b ^ b.log n, b.log n)`.  -/
Nat.log.go : ℕ → ℕ → ℕ → ℕ × ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.ext_hom_hom : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {W₁ W₂ : CategoryTheory.Limits.Cowedge F}
  (e : W₁.pt ≅ W₂.pt)
  (he :
    autoParam
      (∀ (j : J),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π W₁ j) e.hom =
          CategoryTheory.Limits.Multicofork.π W₂ j)
      CategoryTheory.Limits.Cowedge.ext._auto_1),
  (CategoryTheory.Limits.Cowedge.ext e he).hom.hom = e.hom
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.ker_toZModPow : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ), RingHom.ker (PadicInt.toZModPow n) = Ideal.span {↑p ^ n}
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.comp_χ_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))}
  (m : F ⟶ G),
  CategoryTheory.CategoryStruct.comp m (CategoryTheory.Presheaf.χ m) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.isTerminalConst Cᵒᵖ CategoryTheory.Limits.Types.isTerminalPUnit).from F)
      (CategoryTheory.Presheaf.truth C)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- A strongly Cartesian morphism lying over an isomorphism is an isomorphism.  -/
CategoryTheory.Functor.IsStronglyCartesian.isIso_of_base_isIso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ]
  [CategoryTheory.IsIso f], CategoryTheory.IsIso φ
-- Lean.Data.JsonRpc
Lean.JsonRpc.instToJsonRequestID : Lean.ToJson Lean.JsonRpc.RequestID
-- Init.Data.List.Count
List.replicate_sublist_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α} {l : List α},
  (List.replicate n a).Sublist l ↔ n ≤ List.count a l
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E},
  VectorField.lieBracketWithin 𝕜 V W s = fun x => (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Diagnostics.mk.sizeOf_spec : ∀ (usedThmCounter triedThmCounter : Lean.PHashMap Lean.Meta.Origin ℕ) (congrThmCounter : Lean.PHashMap Lean.Name ℕ)
  (thmsWithBadKeys : Lean.PArray Lean.Meta.SimpTheorem),
  sizeOf
      { usedThmCounter := usedThmCounter, triedThmCounter := triedThmCounter, congrThmCounter := congrThmCounter,
        thmsWithBadKeys := thmsWithBadKeys } =
    1 + sizeOf usedThmCounter + sizeOf triedThmCounter + sizeOf congrThmCounter + sizeOf thmsWithBadKeys
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zag.symm : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ : J},
  CategoryTheory.Zag j₁ j₂ → CategoryTheory.Zag j₂ j₁
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
/-- `uliftYoneda` is dense: Every `X : Cᵒᵖ ⥤ Type max w v₁` is the colimit over
`CostructuredArrow.proj uliftYoneda X ⋙ uliftYoneda`.  -/
CategoryTheory.denseAtUliftYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) → CategoryTheory.uliftYoneda.{w, v₁, u₁}.DenseAt X
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  F.mapComp (CategoryTheory.CategoryStruct.id a) f =
    F.map₂Iso (CategoryTheory.Bicategory.leftUnitor f) ≪≫
      (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm ≪≫
        (CategoryTheory.Bicategory.whiskerRightIso (F.mapId a) (F.map f)).symm
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (l : List α),
  m₁.Equiv m₂ → (m₁.insertMany l).Equiv (m₂.insertMany l)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.zero_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] (X : C) {Y Z : C} [inst_3 : CategoryTheory.Preadditive C] (a : M) {b c : M}
  (β : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c), CategoryTheory.ShiftedHom.comp 0 β h = 0