mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` holds for localization away maps, then so does `Locally P`.  -/
RingHom.locally_holdsForLocalizationAway : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.hasLimits : CategoryTheory.Limits.HasLimits Profinite
-- Mathlib.Order.Filter.IndicatorFunction
tendsto_indicator_biUnion_finset : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Zero β] (s : ι → Set α) (f : α → β) (a : α),
  Filter.Tendsto (fun n => (⋃ i ∈ n, s i).indicator f a) Filter.atTop (pure ((Set.iUnion s).indicator f a))
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMapWithin_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M},
  (∀ x ∈ s, f x = f₁ x) →
    ∀ (p : TangentBundle I M), p.proj ∈ s → tangentMapWithin I I' f s p = tangentMapWithin I I' f₁ s p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- Monomorphisms are stable under pullback in the second argument.  -/
CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) [CategoryTheory.Mono g],
  CategoryTheory.Mono t.fst
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.mk.sizeOf_spec : ∀ (s : String.Slice) (offset : String.Pos.Raw) (hinv : offset ≤ s.rawEndPos),
  sizeOf { s := s, offset := offset, hinv := hinv } = 1 + sizeOf s + sizeOf offset + sizeOf hinv
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.subset_vadd_finset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s t : Finset β}
  {a : α}, s ⊆ a +ᵥ t ↔ -a +ᵥ s ⊆ t
-- Mathlib.MeasureTheory.PiSystem
/-- Predicate saying that a given set is contained in the Dynkin system.  -/
MeasurableSpace.DynkinSystem.Has : {α : Type u_4} → MeasurableSpace.DynkinSystem α → Set α → Prop
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.quotientDiag_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (V : OpenSubgroup (CategoryTheory.Aut F)) {U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U)))
  {X Y : CategoryTheory.SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)} (a : X ⟶ Y),
  (CategoryTheory.PreGaloisCategory.quotientDiag✝ V h u).map a =
    (CategoryTheory.PreGaloisCategory.quotientToEndObjectHom✝ V h u) a
-- Lean.Declaration
Lean.Declaration.opaqueDecl.injEq : ∀ (val val_1 : Lean.OpaqueVal), (Lean.Declaration.opaqueDecl val = Lean.Declaration.opaqueDecl val_1) = (val = val_1)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.mkInitial : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → IO σ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The Fourier transform satisfies `∫ 𝓕 f • g = ∫ f • 𝓕 g`, i.e., it is self-adjoint.  -/
SchwartzMap.integral_fourier_smul_eq : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] [CompleteSpace F] (f : SchwartzMap V ℂ) (g : SchwartzMap V F),
  ∫ (ξ : V), (FourierTransform.fourier f) ξ • g ξ = ∫ (x : V), f x • (FourierTransform.fourier g) x
-- Mathlib.Data.Matrix.Mul
dotProduct_single : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonUnitalNonAssocSemiring α]
  (v : m → α) (x : α) (i : m), v ⬝ᵥ Pi.single i x = v i * x
-- Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Linarith.LinarithConfig.mk.injEq : ∀ (discharger : Lean.Elab.Tactic.TacticM Unit) (exfalso : Bool) (transparency : Lean.Meta.TransparencyMode)
  (splitHypotheses splitNe minimize : Bool) (preprocessors : List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor)
  (oracle : Mathlib.Tactic.Linarith.CertificateOracle) (discharger_1 : Lean.Elab.Tactic.TacticM Unit) (exfalso_1 : Bool)
  (transparency_1 : Lean.Meta.TransparencyMode) (splitHypotheses_1 splitNe_1 minimize_1 : Bool)
  (preprocessors_1 : List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor)
  (oracle_1 : Mathlib.Tactic.Linarith.CertificateOracle),
  ({ discharger := discharger, exfalso := exfalso, transparency := transparency, splitHypotheses := splitHypotheses,
        splitNe := splitNe, minimize := minimize, preprocessors := preprocessors, oracle := oracle } =
      { discharger := discharger_1, exfalso := exfalso_1, transparency := transparency_1,
        splitHypotheses := splitHypotheses_1, splitNe := splitNe_1, minimize := minimize_1,
        preprocessors := preprocessors_1, oracle := oracle_1 }) =
    (discharger = discharger_1 ∧
      exfalso = exfalso_1 ∧
        transparency = transparency_1 ∧
          splitHypotheses = splitHypotheses_1 ∧
            splitNe = splitNe_1 ∧ minimize = minimize_1 ∧ preprocessors = preprocessors_1 ∧ oracle = oracle_1)
-- Mathlib.Data.Set.Operations
Set.mapsTo_preimage : ∀ {α : Type u} {β : Type v} (f : α → β) (t : Set β), Set.MapsTo f (f ⁻¹' t) t
-- Mathlib.Topology.Category.CompHaus.Basic
/-- Every `CompHausLike` admits a functor to `CompHaus`.  -/
compHausLikeToCompHaus : (P : TopCat → Prop) → CategoryTheory.Functor (CompHausLike P) CompHaus
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_ne_top_iff : ∀ {a : ENNReal} {n : ℕ}, a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.inv₀_of_disjoint` -/
TendstoLocallyUniformlyOn.fun_inv₀_of_disjoint : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X] {s : Set X}
  {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    (∀ x ∈ s, Disjoint (Filter.map f (nhdsWithin x s)) (nhds 0)) →
      TendstoLocallyUniformlyOn (fun i i_1 => (F i i_1)⁻¹) (fun i => (f i)⁻¹) l s
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : Set β} {f : α → β},
  Set.MapsTo f (⋃ i, s i) t ↔ ∀ (i : ι), Set.MapsTo f (s i) t
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.tensor_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} {P : Type u_6} [inst_8 : AddCommMonoid P] [inst_9 : Module A P] {π : Representation A G P}
  (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) (v : V) (w : U), (f.tensor g) (v ⊗ₜ[A] w) = f v ⊗ₜ[A] g w
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂).getKey? k = none
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.coeff_homogeneousComponent : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ),
  MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent n) φ) =
    if Finsupp.degree d = n then MvPolynomial.coeff d φ else 0
-- Mathlib.Analysis.SpecificLimits.Basic
Nat.tendsto_div_const_atTop : ∀ {n : ℕ}, n ≠ 0 → Filter.Tendsto (fun x => x / n) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₂ =
    CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_succ_cons : ∀ {α : Type u} {xs : List α} {hd x : α} {i : ℕ}, (hd :: xs).insertIdx (i + 1) x = hd :: xs.insertIdx i x
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.sub_scalar_sq_eq_discr : ∀ {K : Type u_1} [inst : Field K] {m : Matrix (Fin 2) (Fin 2) K} [NeZero 2],
  (m - (Matrix.scalar (Fin 2)) (m.trace / 2)) ^ 2 = (Matrix.scalar (Fin 2)) (m.discr / 4)
-- Aesop.Search.SearchM
Aesop.SearchM.instMonadRef : {Q : Type} → [inst : Aesop.Queue Q] → Lean.MonadRef (Aesop.SearchM Q)
-- Lean.Data.Lsp.Basic
Lean.Lsp.ResolveSupport.mk.inj : ∀ {properties properties_1 : Array String},
  { properties := properties } = { properties := properties_1 } → properties = properties_1
-- Init.Meta.Defs
Lean.isIdRest : Char → Bool
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.contract_mid : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (self : CliffordAlgebra.EvenHom Q A)
  (m₁ m₂ m₃ : M), (self.bilin m₁) m₂ * (self.bilin m₂) m₃ = Q m₂ • (self.bilin m₁) m₃
-- Mathlib.RingTheory.LinearDisjoint
/-- Linear disjointness is symmetric in a commutative ring.  -/
Subalgebra.linearDisjoint_comm : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S}, A.LinearDisjoint B ↔ B.LinearDisjoint A
-- Mathlib.Data.Vector.Basic
List.Vector.get_set_of_ne : ∀ {α : Type u_1} {n : ℕ} {v : List.Vector α n} {i j : Fin n}, i ≠ j → ∀ (a : α), (v.set i a).get j = v.get j
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The intersection of two sub-dp-ideals is a sub-dp-ideal.  -/
DividedPowers.SubDPIdeal.instMin : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → Min hI.SubDPIdeal
-- Mathlib.Algebra.Group.Hom.Basic
MulHom.mul_apply : ∀ {M : Type u_8} {N : Type u_9} [inst : Mul M] [inst_1 : CommSemigroup N] (f g : M →ₙ* N) (x : M), (f * g) x = f x * g x
-- Mathlib.Order.Bounded
Set.bounded_le_iff_bounded_lt : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [NoMaxOrder α],
  Set.Bounded (fun x1 x2 => x1 ≤ x2) s ↔ Set.Bounded (fun x1 x2 => x1 < x2) s
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φH : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C}
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  [inst_6 : F.PreservesRightHomologyOf S] [inst_7 : G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : F ⟶ G),
  (CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ).φH = τ.app h.H
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_of_mem_CNF : ∀ {b o e c : Ordinal.{u_1}}, (e, c) ∈ Ordinal.CNF b o → (Ordinal.CNF.coeff b o) e = c
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Fintype.bilinearCombination_apply : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {S : Type u_4} [inst_4 : Semiring S] [inst_5 : Module S M] [inst_6 : SMulCommClass R S M]
  (v : α → M), (Fintype.bilinearCombination R S) v = Fintype.linearCombination R v
-- Mathlib.Order.Cover
CovBy.Ioo_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b → Set.Ioo a b = ∅
-- Mathlib.CategoryTheory.Iso
CategoryTheory.inv.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [I : CategoryTheory.IsIso f], CategoryTheory.inv f = CategoryTheory.inv f_1
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.congrSimp?.forSide : Congr!.Config → Lean.MVarId → Lean.Expr → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.instAlgebraEnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type w} →
        [inst_2 : CommSemiring R] → [CategoryTheory.Linear R C] → (X : C) → Algebra R (CategoryTheory.End X)
-- Mathlib.ModelTheory.ElementaryMaps
/-- Lifts an elementary embedding to the expanded language with constants  -/
FirstOrder.Language.ElementaryEmbedding.liftWithConstants : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (f : L.ElementaryEmbedding M N) →
            (A : Set M) → (L.withConstants ↑A).ElementaryEmbedding M (f.toEmbedding.withConstants A)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_σ_self'_apply : ∀ {S : SSet} {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.castSucc →
    ∀ (x : S.obj (Opposite.op { len := n })),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S i)) x) =
        x
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x₁ y₁ : C} {x₂ y₂ : D} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x₁ g)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f y₂)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instLattice : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [Lattice β] → Lattice (l.Germ β)
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image : ∀ {M₁ : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [T2Space M₂] (f : M₁ → M₂),
  IsCompactOperator f ↔ ∃ V ∈ nhds 0, IsCompact (closure (f '' V))
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.lineal_le : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] (C : PointedCone R E), ↑C.lineal ≤ C
-- Lean.Elab.SyntheticMVars
/-- Synthetic metavariables associated with type class resolution can be postponed.
Motivation: this kind of metavariable are not synthetic opaque, and can be assigned by `isDefEq`.
Universe constraints can also be postponed.
 -/
Lean.Elab.Term.PostponeBehavior.partial : Lean.Elab.Term.PostponeBehavior
-- Mathlib.RingTheory.Ideal.Prod
/-- Classification of prime ideals in product rings: the prime ideals of `R × S` are precisely the
ideals of the form `p × S` or `R × p`, where `p` is a prime ideal of `R` or `S`.  -/
Ideal.ideal_prod_prime : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal (R × S)),
  I.IsPrime ↔ (∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_some_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  t.getKey? k = some k' ↔ ∃ (h : k ∈ t), t.getKey k h = k'
-- Lean.Data.SMap
Lean.SMap.foldStage2 : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → {σ : Type w} → (σ → α → β → σ) → σ → Lean.SMap α β → σ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_ofList_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β} [inst_4 : Inhabited β],
      List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.HashMap.Raw.ofList l)[k']! = v
-- Mathlib.Computability.Partrec
Partrec.nat_iff : ∀ {f : ℕ →. ℕ}, Partrec f ↔ Nat.Partrec f
-- Init.Data.Array.Lex.Lemmas
Array.le_trans : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {xs ys zs : Array α},
  xs ≤ ys → ys ≤ zs → xs ≤ zs
-- Batteries.Data.String.Legacy
/-- Folds a function over a string from the right, accumulating a value starting with `init`. The
accumulated value is combined with each character in reverse order, using `f`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.

Examples:
 * `"coffee tea water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2`
 * `"coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3`
 * `"coffee tea water".foldr (fun c s => c.push s) "" = "retaw dna aet eeffoc"`
 -/
String.Legacy.foldr : {α : Type u} → (Char → α → α) → α → String → α
-- Init.Data.String.Basic
ByteArray.validateUTF8_eq_false_iff : ∀ {b : ByteArray}, b.validateUTF8 = false ↔ ¬b.IsValidUTF8
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Internal.ofToSliceWithProof.match_1.eq_1 : ∀ {s : String} (motive : { p // p ≠ s.toSlice.endPos } → Sort u_1) (p : s.toSlice.Pos) (h : p ≠ s.toSlice.endPos)
  (h_1 : (p : s.toSlice.Pos) → (h : p ≠ s.toSlice.endPos) → motive ⟨p, h⟩),
  (match ⟨p, h⟩ with
    | ⟨p, h⟩ => h_1 p h) =
    h_1 p h
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- The `k`-th iterated derivative of a continuous multilinear map `f` at the point `x`. It is a
continuous multilinear map of `k` vectors `v₁, ..., vₖ` (with the same type as `x`), mapping them
to `∑ f (x₁, (v_{i₁})₂, x₃, ...)`, where at each index `j` one uses either `xⱼ` or one
of the `(vᵢ)ⱼ`, and each `vᵢ` has to be used exactly once.
The sum is parameterized by the embeddings of `Fin k` in the index type `ι` (or, equivalently,
by the subsets `s` of `ι` of cardinality `k` and then the bijections between `Fin k` and `s`).

The fact that this is indeed the iterated Fréchet derivative is proved in
`ContinuousMultilinearMap.iteratedFDeriv_eq`.
 -/
ContinuousMultilinearMap.iteratedFDeriv : {𝕜 : Type u} →
  {ι : Type v} →
    {E₁ : ι → Type wE₁} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E₁ i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  [Fintype ι] →
                    ContinuousMultilinearMap 𝕜 E₁ G → (k : ℕ) → ((i : ι) → E₁ i) → ((i : ι) → E₁ i) [×k]→L[𝕜] G
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the closed `r`-ball
around zero `{x | v.restrict x ≤ r}` is clopen in the valuative topology.  -/
Valuation.isClopen_closedBall : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  {r : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, r ≠ 0 → IsClopen {x | v.restrict x ≤ r}
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.discharge? : Lean.Meta.Simp.Methods → Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_comp : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] (Q : QuadraticMap R M N) {N' : Type u_8}
  [inst_10 : AddCommGroup N'] [inst_11 : Module R N'] (f : N' →ₗ[R] M),
  (QuadraticMap.associatedHom S) (Q.comp f) = LinearMap.compl₁₂ ((QuadraticMap.associatedHom S) Q) f f
-- Mathlib.Data.Finset.Density
Finset.dens_inter_add_dens_union : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α),
  (s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens
-- Mathlib.Topology.Closure
Set.Finite.interior_biInter : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type u_1} {s : Set ι},
  s.Finite → ∀ (f : ι → Set X), interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i)
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.quotient_liftOn_mk : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {β : Sort u_2} (f : α → β)
  (h : ∀ (a b : α), (QuotientAddGroup.leftRel s) a b → f a = f b) (x : α), Quotient.liftOn' (↑x) f h = f x
-- Mathlib.Order.OmegaCompletePartialOrder
/-- A function `f` between `ω`-complete partial orders is `ωScottContinuous` if it is
Scott continuous over chains.  -/
OmegaCompletePartialOrder.ωScottContinuous : {α : Type u_2} → {β : Type u_3} → [OmegaCompletePartialOrder α] → [OmegaCompletePartialOrder β] → (α → β) → Prop
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.ObjectProperty.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty D) (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  (hF : ∀ (X : C), P (F.obj X)), P.lift F hF = P.lift F_1 ⋯
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f → IsBoundedLinearMap 𝕜 fun e => -f e
-- Init.Data.UInt.Lemmas
USize.mul_one : ∀ (a : USize), a * 1 = a
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [inst_2 : CategoryTheory.IsIso h.unit]
  (X : C), h.whiskerLeftLCounitIsoOfIsIsoUnit.hom.app X = h.counit.app (L.obj X)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.length_takeUntil_le_length : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).length ≤ p.length
-- Mathlib.Order.SupIndep
Sigma.snd.hcongr_3 : ∀ (α α' : Type u),
  α = α' →
    ∀ (β : α → Type v) (β' : α' → Type v),
      β ≍ β' → ∀ (self : Sigma β) (self' : Sigma β'), self ≍ self' → self.snd ≍ self'.snd
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- An antisymmetric bilinear form on an oriented real inner product space of dimension 2 (usual
notation `ω`). When evaluated on two vectors, it gives the oriented area of the parallelogram they
span.  -/
Orientation.areaForm : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → [Fact (Module.finrank ℝ E = 2)] → Orientation ℝ E (Fin 2) → E →ₗ[ℝ] E →ₗ[ℝ] ℝ