mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_nsmul : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddMonoid Y]
  (D : Function.locallyFinsuppWithin U Y) (n : ℕ), ⇑(n • D) = n • ⇑D
-- Mathlib.RingTheory.Polynomial.Basic
Finsupp.mapDomain.addMonoidHom.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α → β),
  Finsupp.mapDomain.addMonoidHom f = { toFun := Finsupp.mapDomain f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
Lean.Meta.RefinedDiscrTree.MatchResult.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (elts : Std.TreeMap ℕ (Array (Array α)) compare),
  sizeOf { elts := elts } = 1 + sizeOf elts
-- Mathlib.Topology.Compactness.Compact
isCompact_univ : ∀ {X : Type u} [inst : TopologicalSpace X] [h : CompactSpace X], IsCompact Set.univ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.op_L₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.op.L₂ = S.L₁.op
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_zpow : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] (a : Quaternion R) (z : ℤ),
  Quaternion.normSq (a ^ z) = Quaternion.normSq a ^ z
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- The object part  -/
CategoryTheory.ProfunctorCore.obj : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D → C → D → Type w
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.antidiagonalTuple_one : ∀ (n : ℕ), Finset.Nat.antidiagonalTuple 1 n = {![n]}
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
setBasisOfLinearIndependentOfCardEqFinrank.eq_1 : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  [inst_3 : Nonempty ↑s] [inst_4 : Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val)
  (card_eq : s.toFinset.card = Module.finrank K V),
  setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯
-- Lean.Expr
/-- Given `a : Nat`, returns `Nat.succ a`  -/
Lean.mkNatSucc : Lean.Expr → Lean.Expr
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.instContinuousEvalConst : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousEvalConst (A →ₜ+ B) A B
-- Mathlib.Topology.Maps.Basic
IsOpenMap.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenMap id
-- Mathlib.Data.Finset.SymmDiff
/-- See `symmDiff_subset_sdiff` for the swapped version of this.  -/
Finset.symmDiff_subset_sdiff' : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t \ s ⊆ symmDiff s t
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability at filter in both endpoints.

If `f` is a measurable function integrable on `a..b`, `(la, la')` is an `intervalIntegral.FTCFilter`
pair around `a`, and `f` has a finite limit `c` almost surely at `la'`, then
`(∫ x in v..b, f x) - ∫ x in u..b, f x = -(v - u) • c + o(‖v - u‖)` as `u` and `v` tend to `la`.

This lemma could've been formulated using `HasStrictDerivAtFilter` if we had this definition.  -/
intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E}
  {c : E} {la la' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {u v : ι → ℝ} [intervalIntegral.FTCFilter a la la'],
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f la' MeasureTheory.volume →
      Filter.Tendsto f (la' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        Filter.Tendsto u lt la →
          Filter.Tendsto v lt la →
            (fun t => ((∫ (x : ℝ) in v t..b, f x) - ∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)
-- Init.Data.Vector.Lemmas
Vector.map_const : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {b : β},
  Vector.map (Function.const α b) xs = Vector.replicate n b
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_map : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N)
  (x : TrivSqZeroExt R' M), ((TrivSqZeroExt.map f) x).snd = f x.snd
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme}
  [P.IsStableUnderBaseChange] [P.IsMultiplicative] [P.RespectsIso],
  (CategoryTheory.MorphismProperty.Over.forget P ⊤ S).LocallyCoverDense
    (AlgebraicGeometry.Scheme.overGrothendieckTopology P S)
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.instInhabitedStatus : Inhabited Mathlib.Explode.Status
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A : C)
  [inst_4 : ∀ (B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F],
  (CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso F A).hom =
    CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → (B.ker = ⊥ ↔ B.flip.ker = ⊥)
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.mk_mul_mk : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] {a₁ a₂ b₁ b₂ : α},
  Lean.Grind.Ring.OfSemiring.Q.mk (a₁, a₂) * Lean.Grind.Ring.OfSemiring.Q.mk (b₁, b₂) =
    Lean.Grind.Ring.OfSemiring.Q.mk (a₁ * b₁ + a₂ * b₂, a₁ * b₂ + a₂ * b₁)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.leftInvOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Set.LeftInvOn (↑e.symm) (↑e) e.source
-- Init.Data.Array.Lex.Lemmas
Array.le_toList : ∀ {α : Type u_1} [inst : LT α] {xs ys : Array α}, xs.toList ≤ ys.toList ↔ xs ≤ ys
-- Mathlib.Data.Multiset.AddSub
Multiset.subset_add_left : ∀ {α : Type u_1} {s t : Multiset α}, s ⊆ s + t
-- Mathlib.Order.CompactlyGenerated.Basic
exists_sSupIndep_of_sSup_atoms_eq_top : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α],
  sSup {a | IsAtom a} = ⊤ → ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Eta-expanded form of `MeasureTheory.VectorMeasure.Integrable.add` -/
MeasureTheory.VectorMeasure.Integrable.fun_add : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → μ.Integrable g → μ.Integrable fun i => f i + g i
-- Init.Data.UInt.Lemmas
USize.neg_mul : ∀ (a b : USize), -a * b = -(a * b)
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The function `y ↦ y * exp (-y)` is bounded above by `exp (-1)`.  -/
Real.mul_exp_neg_le_exp_neg_one : ∀ (y : ℝ), y * Real.exp (-y) ≤ Real.exp (-1)
-- Mathlib.CategoryTheory.Galois.Action
/-- Any (fiber) functor `F : C ⥤ FintypeCat` naturally factors via
the forgetful functor from `Action FintypeCat (Aut F)` to `FintypeCat`.  -/
CategoryTheory.PreGaloisCategory.functorToAction : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (F : CategoryTheory.Functor C FintypeCat) → CategoryTheory.Functor C (Action FintypeCat (CategoryTheory.Aut F))
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TrySuggestionEntry.name : Lean.Elab.Tactic.Try.TrySuggestionEntry → Lean.Name
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_append_toList_rco : ∀ {l m n : ℕ}, l ≤ m → m ≤ n → (l...m).toList ++ (m...n).toList = (l...n).toList
-- Mathlib.Algebra.BigOperators.Finprod
one_lt_finprod : ∀ {ι : Type u_3} {M : Type u_7} [inst : CommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M},
  (∀ (i : ι), 1 ≤ f i) → (∃ i, 1 < f i) → Function.HasFiniteMulSupport f → 1 < ∏ᶠ (i : ι), f i
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- `coevaluation_evaluation'` field of `ExactPairing Y X` in a braided category  -/
_private.Mathlib.CategoryTheory.Monoidal.Rigid.Braided.0.CategoryTheory.BraidedCategory.coevaluation_evaluation_braided' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : C} [inst_3 : CategoryTheory.ExactPairing X Y],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.CategoryStruct.comp (η_ X Y) (β_ Y X).inv))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y X).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (ε_ X Y))
          X)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.star_inner : ∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] (x y : E), star (inner A x y) = inner A y x
-- Mathlib.Algebra.Category.Grp.Ulift
AddCommGrpCat.uliftFunctor_preservesLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J AddCommGrpCat.uliftFunctor
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.maxPowDividing.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → ∀ (I I_1 : Ideal R), I = I_1 → v.maxPowDividing I = v_1.maxPowDividing I_1
-- Mathlib.Algebra.Regular.Basic
/-- The "most used" implication of `add_and_add_iff`, with split
hypotheses, instead of `∧`.  -/
IsAddRegular.and_of_add_of_add : ∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R},
  IsAddRegular (a + b) → IsAddRegular (b + a) → IsAddRegular a ∧ IsAddRegular b
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.bayesRisk_of_isEmpty'' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [IsEmpty Θ] [Nonempty 𝓨], ProbabilityTheory.bayesRisk ℓ P π = 0
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- Inversion is `C^n` away from `0`.  -/
ContMDiffInv₀.contMDiffAt_inv₀ : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : Inv G} {inst_5 : Zero G} {inst_6 : TopologicalSpace G} {inst_7 : ChartedSpace H G}
  [self : ContMDiffInv₀ I n G] ⦃x : G⦄, x ≠ 0 → ContMDiffAt I I n (fun y => y⁻¹) x
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_filterMap : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Option (δ a)},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.filterMap f m)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_some_iff_exists_beq_and_mem_toArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β}, m.WF → (m[k]? = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ m.toArray)
-- Mathlib.Computability.NFA
NFA.mem_accepts_reverse : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α}, x ∈ M.reverse.accepts ↔ x.reverse ∈ M.accepts
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.prev.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.prev = { s := s, i := String.Pos.Raw.prev s i }
-- Mathlib.Order.Category.LinOrd
_private.Mathlib.Order.Category.LinOrd.0.LinOrd.Hom.mk.inj : ∀ {X Y : LinOrd} {hom' hom'_1 : ↑X →o ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℕ → Bool
-- Init.Data.SInt.Bitwise
Int8.not_not : ∀ {a : Int8}, ~~~~~~a = a
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instSMulAdjoinRoot : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      (f : Polynomial R) → [inst_1 : DistribSMul S R] → [IsScalarTower S R R] → SMul S (AdjoinRoot f)
-- Mathlib.Order.Hom.WithTopBot
OrderEmbedding.withBotMap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β),
  f.withBotMap = { toFun := WithBot.map ⇑f, inj' := ⋯, map_rel_iff' := ⋯ }
-- Lean.Meta.Instances
Lean.Meta.Instances.discrTree : Lean.Meta.Instances → Lean.Meta.InstanceTree
-- Aesop.Rule
Aesop.UnfoldRule.unfoldThm? : Aesop.UnfoldRule → Option Lean.Name
-- Mathlib.RingTheory.TensorProduct.Pi
TensorProduct.piScalarRight_symm_algebraMap : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (ι : Type u_3)
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] {N : Type u_4} [inst_5 : Semiring N] [inst_6 : Algebra R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (x : ι → R),
  (TensorProduct.piScalarRight R S N ι).symm ((algebraMap (ι → R) (ι → N)) x) = 1 ⊗ₜ[R] x
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.transport_ε_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G) {Z : D}
  (h : G.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε G) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
      (CategoryTheory.CategoryStruct.comp (i.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h)
-- Mathlib.Topology.Algebra.Constructions
AddUnits.continuous_iff : ∀ {M : Type u_1} {X : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace X]
  {f : X → AddUnits M}, Continuous f ↔ Continuous (AddUnits.val ∘ f) ∧ Continuous fun x => ↑(-f x)
-- Mathlib.Data.FinEnum
/-- The enumeration merely adds an ordering, leaving the cardinality as is.  -/
FinEnum.card_eq_fintypeCard : ∀ {α : Type u} [inst : FinEnum α] [inst_1 : Fintype α], FinEnum.card α = Fintype.card α
-- Mathlib.Analysis.Calculus.LHopital
deriv.lhopital_zero_atBot_on_Iio : ∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  DifferentiableOn ℝ f (Set.Iio a) →
    (∀ x ∈ Set.Iio a, deriv g x ≠ 0) →
      Filter.Tendsto f Filter.atBot (nhds 0) →
        Filter.Tendsto g Filter.atBot (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) Filter.atBot l →
            Filter.Tendsto (fun x => f x / g x) Filter.atBot l
-- Init.Data.String.Lemmas.Pattern.Find.String
_private.Init.Data.String.Lemmas.Pattern.Find.String.0.String.Slice.contains_string_eq_true_of_empty : ∀ {pat : String}, pat = "" → ∀ (s : String.Slice), s.contains pat = true
-- Mathlib.Data.Sym.Sym2
/-- Map an unordered pair to an unordered list.  -/
Sym2.toMultiset : {α : Type u_4} → Sym2 α → Multiset α
-- Lean.DocString.Types
Lean.Doc.Inline.image.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (alt url : String),
  sizeOf (Lean.Doc.Inline.image alt url) = 1 + sizeOf alt + sizeOf url
-- Mathlib.Combinatorics.SetFamily.FourFunctions
collapse_modular : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {a : α} {f₁ f₂ f₃ f₄ : Finset α → β} {u : Finset α} [ExistsAddOfLE β],
  a ∉ u →
    0 ≤ f₁ →
      0 ≤ f₂ →
        0 ≤ f₃ →
          0 ≤ f₄ →
            (∀ ⦃s : Finset α⦄,
                s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
              ∀ (𝒜 ℬ : Finset (Finset α)) ⦃s : Finset α⦄,
                s ⊆ u →
                  ∀ ⦃t : Finset α⦄,
                    t ⊆ u →
                      collapse✝ 𝒜 a f₁ s * collapse✝ ℬ a f₂ t ≤
                        collapse✝ (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse✝ (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rid_tmul : ∀ {R : Type uR} (A : Type uA) {M : Type uM} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] (r : R) (m : M),
  (TensorProduct.AlgebraTensorModule.rid R A M) (m ⊗ₜ[R] r) = r • m
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns `.true` if `c` is satisfied by the current partial model,
`.undef` if `c` contains unassigned variables, and `.false` otherwise.
 -/
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.satisfied : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.GoalM Lean.LBool
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
/-- If `NormedSpace.exp R x.fst` converges to `e`
then `(NormedSpace.exp R x).snd` converges to `e • x.snd`.  -/
TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm : ∀ (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field 𝕜] [CharZero 𝕜] [inst_2 : Ring R] [inst_3 : AddCommGroup M]
  [inst_4 : Algebra 𝕜 R] [inst_5 : Module 𝕜 M] [inst_6 : Module R M] [inst_7 : Module Rᵐᵒᵖ M]
  [inst_8 : SMulCommClass R Rᵐᵒᵖ M] [inst_9 : IsScalarTower 𝕜 R M] [inst_10 : IsScalarTower 𝕜 Rᵐᵒᵖ M]
  [inst_11 : TopologicalSpace R] [inst_12 : TopologicalSpace M] [inst_13 : IsTopologicalRing R]
  [inst_14 : IsTopologicalAddGroup M] [inst_15 : ContinuousSMul R M] [inst_16 : ContinuousSMul Rᵐᵒᵖ M]
  (x : TrivSqZeroExt R M),
  MulOpposite.op x.fst • x.snd = x.fst • x.snd →
    ∀ {e : R},
      HasSum (fun n => (NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst) e →
        HasSum (fun n => ((NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) n) fun x_1 => x).snd) (e • x.snd)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.eventually_add_right_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (t : G) {p : G → Prop}, (∀ᵐ (x : G) ∂μ, p (x + t)) ↔ ∀ᵐ (x : G) ∂μ, p x
-- Mathlib.Topology.Order.IsLUB
isLUB_iff_of_subset_of_subset_closure : ∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {s t : Set α},
  s ⊆ t → t ⊆ closure s → ∀ {x : α}, IsLUB s x ↔ IsLUB t x
-- Mathlib.Algebra.RingQuot
RingQuot.add_quot : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop) {a b : R},
  { toQuot := Quot.mk (RingQuot.Rel r) a } + { toQuot := Quot.mk (RingQuot.Rel r) b } =
    { toQuot := Quot.mk (RingQuot.Rel r) (a + b) }
-- Mathlib.Analysis.Normed.Group.Uniform
antilipschitzWith_iff_exists_mul_le_norm' : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] {f : 𝓕},
  (∃ K, AntilipschitzWith K ⇑f) ↔ ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_sub : ∀ {a b : UInt64}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.eval.eq_def : ∀ (x : Turing.ToPartrec.Cont),
  x.eval =
    match x with
    | Turing.ToPartrec.Cont.halt => pure
    | Turing.ToPartrec.Cont.cons₁ fs as k => fun v => do
      let ns ← fs.eval as
      k.eval (v.headI :: ns)
    | Turing.ToPartrec.Cont.cons₂ ns k => fun v => k.eval (ns.headI :: v)
    | Turing.ToPartrec.Cont.comp f k => fun v => f.eval v >>= k.eval
    | Turing.ToPartrec.Cont.fix f k => fun v => if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
threeAPFree_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] (x : E) (r : ℝ),
  ThreeAPFree (Metric.sphere x r)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.modifyKey.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)),
  Std.Internal.List.Const.modifyKey k f l =
    match Std.Internal.List.getValue? k l with
    | none => l
    | some v => Std.Internal.List.replaceEntry k (f v) l
-- Mathlib.Algebra.Group.Torsion
two_nsmul_eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] [IsAddTorsionFree M] {a : M}, 2 • a = 0 ↔ a = 0
-- Std.Http.Data.URI.Config
Std.Http.URI.Config.mk.inj : ∀
  {maxSchemeLength maxHostLength maxUserInfoLength maxSegmentLength maxQueryLength maxFragmentLength maxPathSegments
    maxTotalPathLength maxQueryParams maxSchemeLength_1 maxHostLength_1 maxUserInfoLength_1 maxSegmentLength_1
    maxQueryLength_1 maxFragmentLength_1 maxPathSegments_1 maxTotalPathLength_1 maxQueryParams_1 : ℕ},
  { maxSchemeLength := maxSchemeLength, maxHostLength := maxHostLength, maxUserInfoLength := maxUserInfoLength,
        maxSegmentLength := maxSegmentLength, maxQueryLength := maxQueryLength, maxFragmentLength := maxFragmentLength,
        maxPathSegments := maxPathSegments, maxTotalPathLength := maxTotalPathLength,
        maxQueryParams := maxQueryParams } =
      { maxSchemeLength := maxSchemeLength_1, maxHostLength := maxHostLength_1,
        maxUserInfoLength := maxUserInfoLength_1, maxSegmentLength := maxSegmentLength_1,
        maxQueryLength := maxQueryLength_1, maxFragmentLength := maxFragmentLength_1,
        maxPathSegments := maxPathSegments_1, maxTotalPathLength := maxTotalPathLength_1,
        maxQueryParams := maxQueryParams_1 } →
    maxSchemeLength = maxSchemeLength_1 ∧
      maxHostLength = maxHostLength_1 ∧
        maxUserInfoLength = maxUserInfoLength_1 ∧
          maxSegmentLength = maxSegmentLength_1 ∧
            maxQueryLength = maxQueryLength_1 ∧
              maxFragmentLength = maxFragmentLength_1 ∧
                maxPathSegments = maxPathSegments_1 ∧
                  maxTotalPathLength = maxTotalPathLength_1 ∧ maxQueryParams = maxQueryParams_1
-- Mathlib.CategoryTheory.Simple
/-- If `X` has subobject lattice `{⊥, ⊤}`, then `X` is simple.  -/
CategoryTheory.simple_of_isSimpleOrder_subobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C) [IsSimpleOrder (CategoryTheory.Subobject X)],
  CategoryTheory.Simple X
-- Mathlib.Data.ZMod.Basic
ZMod.castHom_self : ∀ {n : ℕ}, ZMod.castHom ⋯ (ZMod n) = RingHom.id (ZMod n)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_nonneg : ∀ (x : ℝ), 0 ≤ √x
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listEncode.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (t₁ t₂ : L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.equal t₁ t₂).listEncode = [Sum.inl ⟨x, t₁⟩, Sum.inl ⟨x, t₂⟩]