mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.semilinearMapAddEquiv_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S)
  (g : ↑M →ₛₗ[f] ↑N),
  (ModuleCat.semilinearMapAddEquiv f M N) g = ModuleCat.ofHom { toFun := ⇑g, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊥` and `⊤` to the domain and codomain of a `LatticeHom`.  -/
LatticeHom.withBotWithTop : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] → LatticeHom α β → BoundedLatticeHom (WithBot (WithTop α)) (WithBot (WithTop β))
-- Mathlib.Data.Multiset.Pi
Multiset.Nodup.pi : ∀ {α : Type u_1} [inst : DecidableEq α] {β : α → Type u_2} {s : Multiset α} {t : (a : α) → Multiset (β a)},
  s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
-- Mathlib.Algebra.Ring.Action.Group
/-- **Alias** of `MulSemiringAction.toRingEquiv_apply_symm_apply`. -/
MulSemiringAction.toRingEquiv_symm_apply : ∀ (G : Type u_1) [inst : Group G] (R : Type u_2) [inst_1 : Semiring R] [inst_2 : MulSemiringAction G R] (x : G) (a : R),
  ((MulSemiringAction.toRingEquiv G R) x).symm a = x⁻¹ • a
-- Mathlib.Topology.Constructions
continuous_map_of_le : ∀ {α : Type u_5} [inst : TopologicalSpace α] {s t : Setoid α} (h : s ≤ t), Continuous (Setoid.map_of_le h)
-- Mathlib.Logic.Function.Conjugate
/-- The identity map commutes with any self-map.  -/
Function.Commute.id_left : ∀ {α : Type u_1} {f : α → α}, Function.Commute id f
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.instIsHausdorffMaximalIdeal : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  IsHausdorff (IsLocalRing.maximalIdeal R) R
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X M.X.X))
-- Mathlib.Tactic.Conv
Mathlib.Tactic.Conv.convRun_conv_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.IsFundamentalGroup.non_trivial' : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat}
  {inst_1 : CategoryTheory.GaloisCategory C} {G : Type u_1} {inst_2 : Group G}
  {inst_3 : (X : C) → MulAction G (F.obj X).obj} {inst_4 : TopologicalSpace G} {inst_5 : IsTopologicalGroup G}
  {inst_6 : CompactSpace G} [self : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G),
  (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_inj`. -/
SkewMonoidAlgebra.toFinsupp_inj : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a b : SkewMonoidAlgebra k G}, a.coeff = b.coeff ↔ a = b
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.copy_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : α → β) (hf : ↑e = f) (g : β → α) (hg : ↑e.symm = g)
  (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t), ↑(e.copy f hf g hg s hs t ht).symm = g
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittZSMul.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (n n_1 : ℤ),
  n = n_1 → ∀ (a a_1 : ℕ), a = a_1 → WittVector.wittZSMul p n a = WittVector.wittZSMul p_1 n_1 a_1
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.exists_not_self_orthogonal : ∀ {F : Type u_1} [inst : Field F] {m : Type u_2} [inst_1 : Fintype m] (v : Projectivization F (m → F)),
  ∃ w, ¬v.orthogonal w
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The profinite completion is left adjoint to the forgetful functor.  -/
ProfiniteGrp.ProfiniteCompletion.adjunction : ProfiniteGrp.profiniteCompletion ⊣ CategoryTheory.forget₂ ProfiniteGrp.{u_1} GrpCat
-- Mathlib.Data.Option.Basic
Option.elim_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β) {f : γ → α} {x : α} {i : Option γ},
  (i.elim (h x) fun j => h (f j)) = h (i.elim x f)
-- Mathlib.Algebra.Group.Semiconj.Units
SemiconjBy.units_of_val : ∀ {M : Type u_1} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y → SemiconjBy a x y
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.one_le_card : ∀ {o : Ordinal.{u_1}}, 1 ≤ o.card ↔ 1 ≤ o
-- Mathlib.Algebra.Module.TransferInstance
/-- Transport a module instance via an isomorphism of the underlying abelian groups.
This has better definitional properties than `Equiv.module` since here
the abelian group structure remains unmodified.  -/
AddEquiv.module : {α : Type u_2} →
  {β : Type u_3} →
    (A : Type u_4) →
      [inst : Semiring A] → [inst_1 : AddCommMonoid α] → [inst_2 : AddCommMonoid β] → [Module A β] → α ≃+ β → Module A α
-- Lean.Data.PersistentArray
_private.Lean.Data.PersistentArray.0.Lean.PersistentArray.foldlMAux : {α : Type u} → {m : Type v → Type w} → [Monad m] → {β : Type v} → (β → α → m β) → Lean.PersistentArrayNode α → β → m β
-- Mathlib.RingTheory.WittVector.Identities
WittVector.coeff_p_one : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p], (↑p).coeff 1 = 1
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_eq_zero_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, inner 𝕜 x y = 0 ↔ inner 𝕜 y x = 0
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodComm_apply : ∀ (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  ⇑(MulEquiv.coprodComm M N) = ⇑(Monoid.Coprod.swap M N)
-- Init.Data.BitVec.Basic
/-- The empty bitvector.  -/
BitVec.nil : BitVec 0
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.iUnion_pnat_ptsOfPeriod : ∀ {α : Type u_1} (f : α → α), ⋃ n, Function.ptsOfPeriod f ↑n = Function.periodicPts f
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.le_expGrowthSup_iff : ∀ {u : ℕ → ENNReal} {a : EReal}, a ≤ ExpGrowth.expGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in Filter.atTop, (b * ↑n).exp ≤ u n
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.piEquivL_symm_apply : ∀ (𝕜 : Type u_6) [inst : NormedField 𝕜] {E : Type u_7} {ι : Type u_8} (F : ι → Type u_9) [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : (i : ι) → AddCommGroup (F i)]
  [inst_5 : (i : ι) → Module 𝕜 (F i)] [inst_6 : (i : ι) → TopologicalSpace (F i)]
  [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] (𝔖 : Set (Set E))
  (T : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (e : E) (i : ι),
  ((UniformConvergenceCLM.piEquivL 𝕜 F 𝔖).symm T i) e = T e i
-- Mathlib.Order.Lattice
pairwise_iff_gt : ∀ {α : Type u} [inst : LinearOrder α] {p : α → α → Prop} [Std.Symm p], Pairwise p ↔ ∀ ⦃a b : α⦄, b < a → p a b
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleAlgebra.ext_iff : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieAdmissibleRing L} {x y : LieAdmissibleAlgebra R L},
  x = y ↔ SMul.smul = SMul.smul
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoToFun_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (x : E),
  stereoToFun v x = (2 / (1 - ((innerSL ℝ) v) x)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto x
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Normed commutative ring structure on the product of finitely many non-unital normed
commutative rings, using the sup norm.  -/
Pi.nonUnitalNormedCommRing : {ι : Type u_3} →
  {R : ι → Type u_4} → [Fintype ι] → [(i : ι) → NonUnitalNormedCommRing (R i)] → NonUnitalNormedCommRing ((i : ι) → R i)
-- Lean.Server.References
/-- Definition range of matched identifier.  -/
Lean.Server.References.MatchedDefinition.range : {α : Type} → Lean.Server.References.MatchedDefinition α → Lean.Lsp.Range
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.freeGroupoidFunctor_id : ∀ {V : Type u} [inst : Quiver V], Quiver.freeGroupoidFunctor (𝟭q V) = CategoryTheory.Functor.id (Quiver.FreeGroupoid V)
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Lcomplement : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
  IsLprojection X P → IsLprojection X (1 - P)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
/-- **Alias** of `Ideal.setOfPred_isPrincipal_wellFoundedOn_gt`.

---

The ascending chain condition on principal ideals holds in a `WfDvdMonoid` domain.  -/
Ideal.setOf_isPrincipal_wellFoundedOn_gt : ∀ {α : Type u_1} [inst : CommSemiring α] [WfDvdMonoid α] [IsDomain α],
  {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.preimage_Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b : β),
  ⇑e ⁻¹' Set.Ioi b = Set.Ioi (e.symm b)
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- A structure containing the data of sequential limit in `Profinite` of finite sets.  -/
LightDiagram : Type (u + 1)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.instLawfulBackwardPatternModelForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.Model.LawfulBackwardPatternModel p
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- An orthonormal set in a finite-dimensional `InnerProductSpace` is maximal, if and only if it
is a basis.  -/
maximal_orthonormal_iff_basis_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v : Set E} [FiniteDimensional 𝕜 E],
  Orthonormal 𝕜 Subtype.val → ((∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ⇑b = Subtype.val)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] {S₁ S₂ : NonUnitalStarSubalgebra R A}, S₁.toNonUnitalSubalgebra ≤ S₂.toNonUnitalSubalgebra ↔ S₁ ≤ S₂
-- Mathlib.RingTheory.Ideal.Operations
/-- `Associates (Ideal R)` almost never has decidable equality.
We add a global instance that `Associates (Ideal R)` has decidable
equality, coming from the choice axiom, so that we don't have to provide
`[DecidableEq (Associates (Ideal R))]` arguments in lemma statements.  -/
Ideal.instDecidableEqAssociates : {R : Type u_1} → [inst : CommSemiring R] → DecidableEq (Associates (Ideal R))
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_absolutelyContinuous : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [inst : ProbabilityTheory.IsSFiniteKernel κ] (f : α → β → ENNReal) (a : α),
  ((κ.withDensity f) a).AbsolutelyContinuous (κ a)
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedQueryString.mk.injEq : ∀ {r : UInt8 → Bool} (toByteArray : ByteArray) (valid : Std.Http.URI.IsAllowedEncodedQueryChars r toByteArray)
  (toByteArray_1 : ByteArray) (valid_1 : Std.Http.URI.IsAllowedEncodedQueryChars r toByteArray_1),
  ({ toByteArray := toByteArray, valid := valid } = { toByteArray := toByteArray_1, valid := valid_1 }) =
    (toByteArray = toByteArray_1)
-- Mathlib.Topology.FiberBundle.Basic
/-- The projection from a fiber bundle with a nonempty fiber to its base is a surjective
map.  -/
FiberBundle.surjective_proj : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  [Nonempty F], Function.Surjective Bundle.TotalSpace.proj
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB4StarOfSize.ofShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasProducts C}
  [self : CategoryTheory.AB4StarOfSize.{w, v, u} C] (α : Type w),
  CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete α) C
-- Mathlib.Algebra.Group.Basic
mul_self_zpow : ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℤ), a * a ^ n = a ^ (n + 1)
-- Aesop.Rule.Basic
Aesop.Rule.compareByName : {α : Type} → Aesop.Rule α → Aesop.Rule α → Ordering
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_ric_eq_zero : ∀ {n i : ℕ}, n < i → (*...=n).toArray[i]! = 0
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      CategoryTheory.Category.{max v₂ v, max u₂ u} (CategoryTheory.Grothendieck F)
-- Mathlib.Order.Partition.Basic
Partition.empty_notMem : ∀ {α : Type u_1} {u : Set α} {P : Partition u}, ∅ ∉ P
-- Mathlib.Topology.Compactness.LocallyCompact
Prod.locallyCompactSpace : ∀ (X : Type u_4) (Y : Type u_5) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyCompactSpace X]
  [LocallyCompactSpace Y], LocallyCompactSpace (X × Y)
-- Aesop.Search.SearchM
Aesop.NormSimpContext.mk.inj : ∀ {toContext : Lean.Meta.Simp.Context} {enabled useHyps : Bool} {configStx? : Option Lean.Term}
  {simprocs : Lean.Meta.Simp.SimprocsArray} {toContext_1 : Lean.Meta.Simp.Context} {enabled_1 useHyps_1 : Bool}
  {configStx?_1 : Option Lean.Term} {simprocs_1 : Lean.Meta.Simp.SimprocsArray},
  { toContext := toContext, enabled := enabled, useHyps := useHyps, configStx? := configStx?, simprocs := simprocs } =
      { toContext := toContext_1, enabled := enabled_1, useHyps := useHyps_1, configStx? := configStx?_1,
        simprocs := simprocs_1 } →
    toContext = toContext_1 ∧
      enabled = enabled_1 ∧ useHyps = useHyps_1 ∧ configStx? = configStx?_1 ∧ simprocs = simprocs_1
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- `f` has the derivative `f'` at the point `x` within the subset `s`.

That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x` inside `s`.
 -/
HasDerivWithinAt : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type v} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] → [inst_3 : TopologicalSpace F] → [ContinuousSMul 𝕜 F] → (𝕜 → F) → F → Set 𝕜 → 𝕜 → Prop
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.exact₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Z : C}
  (P : CategoryTheory.ProjectiveResolution Z),
  { X₁ := P.complex.X 1, X₂ := P.complex.X 0, X₃ := ((ChainComplex.single₀ C).obj Z).X 0, f := P.complex.d 1 0,
      g := P.π.f 0, zero := ⋯ }.Exact
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- Eta-expanded form of `MeromorphicOn.logDeriv_prod_eventuallyEq`

---

The logarithmic derivative converts products into sums: away from a codiscrete subset of `U`, the
logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic
derivatives.
 -/
MeromorphicOn.logDeriv_fun_prod_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜'},
  (∀ i ∈ s, MeromorphicOn (F i) U) →
    (∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) →
      (logDeriv fun a => ∏ c ∈ s, F c a) =ᶠ[Filter.codiscreteWithin U] fun a => ∑ c ∈ s, logDeriv (F c) a
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.commute_T : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ) (f : LaurentPolynomial R), Commute (LaurentPolynomial.T n) f
-- Mathlib.Order.Types.Arithmetic
OrderType.instLeftDistribClass : LeftDistribClass OrderType.{u_1}
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_one : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → seminormFromConst' c f 1 = 1
-- Mathlib.RingTheory.Flat.Basic
IsTensorProduct.map_id_injective_of_flat_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_8}
  [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₁] [inst_8 : Module R M₂]
  [inst_9 : AddCommMonoid N₂] [inst_10 : Module R N₂] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f)
  {g : M₁ →ₗ[R] N₂ →ₗ[R] N} (hg : IsTensorProduct g) (i : M₂ →ₗ[R] N₂),
  Function.Injective ⇑i → ∀ [Module.Flat R M₁], Function.Injective ⇑(hf.map hg LinearMap.id i)
-- Batteries.Tactic.Lint.Frontend
/-- Formats a map of linter warnings grouped by filename with `-- filename` comments.
The first `drop_fn_chars` characters are stripped from the filename.
 -/
Batteries.Tactic.Lint.groupedByFilename : Std.HashMap Lean.Name Lean.MessageData → optParam Bool false → Lean.CoreM Lean.MessageData
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.erase₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.erase ⟨m, h⟩ a)).WF
-- Mathlib.Util.Superscript
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.partitionPoint.eq_def : ∀ {α : Type u} [inst : Inhabited α] (as : Array α) (leftOfPartition : α → Bool) (lo hi : ℕ),
  Mathlib.Tactic.Superscript.partitionPoint as leftOfPartition lo hi =
    if lo < hi then
      have m := (lo + hi) / 2;
      have a := as[m]!;
      if leftOfPartition a = true then Mathlib.Tactic.Superscript.partitionPoint as leftOfPartition (m + 1) hi
      else Mathlib.Tactic.Superscript.partitionPoint as leftOfPartition lo m
    else lo
-- Mathlib.Analysis.Convex.Strong
strongConcaveOn_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ},
  StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f
-- Mathlib.Topology.Category.FinTopCat
/-- Scoped topological space instance on objects of the category of finite types, assigning
the discrete topology.  -/
FintypeCatDiscrete.instTopologicalSpaceObjFinite : (X : FintypeCat) → TopologicalSpace X.obj
-- Mathlib.Algebra.Group.ULift
/-- The additive equivalence between `ULift α` and `α`.  -/
AddEquiv.ulift : {α : Type u} → [inst : Add α] → ULift.{u_1, u} α ≃+ α
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (F : C ⥤ₗ D),
  CategoryTheory.Functor.mapCommGrpFunctor.obj F = F.obj.mapCommGrp
-- Mathlib.Algebra.Group.Finsupp
/-- Coercion from a `Finsupp` to a function type is an `AddMonoidHom`.  -/
Finsupp.coeFnAddHom : {ι : Type u_1} → {M : Type u_3} → [inst : AddZeroClass M] → (ι →₀ M) →+ ι → M
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₁_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G)
  (p : CategoryTheory.OverPresheafAux.YonedaCollection F X),
  (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).snd =
    (CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.eqToHom ⋯)))
      ((CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op (CategoryTheory.CostructuredArrow.mk p.fst)))) p.snd)
-- Mathlib.Analysis.Convex.MetricSpace
/-- `dist(sx + (1-s)y, s'x + (1-s')y) = |s - s'| dist(x, y)`.

See `dist_convexCombPair_convexCombPair_le`
for the version where the weights are fixed and the points change.  -/
Convexity.dist_convexCombPair_convexCombPair : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {s t s' t' : ℝ}
  (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) (x y : X),
  dist (Convexity.convexCombPair s t hs ht h x y) (Convexity.convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.monoOfLE.congr_simp : ∀ {X : SSet} [inst : X.Nonsingular] {x y : X.N} (h : x ≤ y), SSet.N.monoOfLE h = SSet.N.monoOfLE h
-- Init.Data.Nat.Sqrt.Lemmas
_private.Init.Data.Nat.Sqrt.Lemmas.0.Nat.AM_GM : ∀ {a b : ℕ}, 4 * a * b ≤ (a + b) * (a + b)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey?.bind t.getKey? = t.maxKey?
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_ne_top : ∀ {α : Type u} [inst : Add α] {x y : WithTop α}, x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
-- Mathlib.GroupTheory.Submonoid.Center
Subsemigroup.centerToMulOpposite_apply_coe : ∀ {M : Type u_2} [inst : Mul M] (r : ↥(Subsemigroup.center M)),
  ↑(Subsemigroup.centerToMulOpposite r) = MulOpposite.op ↑r
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] [inst_4 : NormedAddCommGroup W]
  [inst_5 : InnerProductSpace 𝕜 W] [inst_6 : CompleteSpace W] {F : Type u_4}
  [inst_7 : EquivLike F (V →L[𝕜] V) (W →L[𝕜] W)] [NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)]
  [StarHomClass F (V →L[𝕜] V) (W →L[𝕜] W)] [ContinuousMapClass F (V →L[𝕜] V) (W →L[𝕜] W)],
  OrderIsoClass F (V →L[𝕜] V) (W →L[𝕜] W)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.link.match_3.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r' : Std.DTreeMap.Internal.Impl α β) (szr : ℕ) (k'' : α) (v'' : β k'')
  (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    Std.DTreeMap.Internal.Impl.Tree α β (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
      Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size))
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ })
  (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced)
  (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size),
  x = { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } →
    (match x with
      | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) ≍
      h_1 ℓ hℓ₁ hℓ₂
-- Lean.Elab.Tactic.Conv.Simp
Lean.Elab.Tactic.Conv.evalDSimp : Lean.Elab.Tactic.Tactic
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.weakEquivalence_toHoCat_map_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.FibrantObject C} (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.FibrantObject.toHoCat.map f) ↔
    HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.Order.CompleteLattice.Basic
sSup_lowerBounds_eq_sInf : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), sSup (lowerBounds s) = sInf s