mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Prod
_private.Mathlib.MeasureTheory.VectorMeasure.Prod.0.MeasureTheory.VectorMeasure.prod.eq_1 : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  (μ : MeasureTheory.VectorMeasure X E) (ν : MeasureTheory.VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G),
  μ.prod ν B = if h : μ.HasProd ν B then ⋯.choose else 0
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.instBEqSeq.beq.match_1.eq_2 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (a : Lean.Grind.AC.Var) (a_1 : Lean.Grind.AC.Seq)
  (b : Lean.Grind.AC.Var) (b_1 : Lean.Grind.AC.Seq)
  (h_1 : (a b : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var a) (Lean.Grind.AC.Seq.var b))
  (h_2 :
    (a : Lean.Grind.AC.Var) →
      (a_2 : Lean.Grind.AC.Seq) →
        (b : Lean.Grind.AC.Var) →
          (b_2 : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons a a_2) (Lean.Grind.AC.Seq.cons b b_2))
  (h_3 : (x x_1 : Lean.Grind.AC.Seq) → motive x x_1),
  (match Lean.Grind.AC.Seq.cons a a_1, Lean.Grind.AC.Seq.cons b b_1 with
    | Lean.Grind.AC.Seq.var a, Lean.Grind.AC.Seq.var b => h_1 a b
    | Lean.Grind.AC.Seq.cons a a_2, Lean.Grind.AC.Seq.cons b b_2 => h_2 a a_2 b b_2
    | x, x_1 => h_3 x x_1) =
    h_2 a a_1 b b_1
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Pos.Raw.set.match_1.splitter : (motive : String → String.Pos.Raw → Char → Sort u_1) →
  (x : String) →
    (x_1 : String.Pos.Raw) →
      (x_2 : Char) → ((s : String) → (i : String.Pos.Raw) → (c : Char) → motive s i c) → motive x x_1 x_2
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.FactorSet.prod.eq_def : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] (x : Associates.FactorSet α),
  x.prod =
    match x with
    | none => 0
    | some s => (Multiset.map Subtype.val s).prod
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.normalize_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Multiset α),
  normalize s.gcd = s.gcd
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldlM_eq_foldlM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.TreeMap.Raw.foldlM (fun d a x => f d a) init t = List.foldlM f init t.keys
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.takeWhile : ∀ {l m r : List Char} (p : Char → Bool) {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s →
    Substring.Raw.ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r) (s.takeWhile p)
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The proposition that `normUnit` respects multiplication of non-zero elements.  -/
StrongNormalizationMonoid.normUnit_mul : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : StrongNormalizationMonoid α] {a b : α},
  a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
-- Mathlib.Order.Hom.Bounded
/-- Copy of a `BotHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
BotHom.copy : {α : Type u_2} →
  {β : Type u_3} → [inst : Bot α] → [inst_1 : Bot β] → (f : BotHom α β) → (f' : α → β) → f' = ⇑f → BotHom α β
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.neg_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) (v : V₁), (-f) v = -f v
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_mul_pow_left : ∀ {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n m : ℕ), p ≠ q → padicValNat p (p ^ n * q ^ m) = n
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.mk.sizeOf_spec : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : CommRing A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {σ : A₁ →ₐ[R] A₂} {L₁ : Type u_8} {L₂ : Type u_9}
  [inst_5 : LieRing L₁] [inst_6 : Module A₁ L₁] [inst_7 : LieRingModule L₁ A₁] [inst_8 : LieAlgebra R L₁]
  [inst_9 : LieRing L₂] [inst_10 : Module A₂ L₂] [inst_11 : LieRingModule L₂ A₂] [inst_12 : LieAlgebra R L₂]
  [inst_13 : SizeOf R] [inst_14 : SizeOf A₁] [inst_15 : SizeOf A₂] [inst_16 : SizeOf L₁] [inst_17 : SizeOf L₂]
  (toLieHom : L₁ →ₗ⁅R⁆ L₂) (map_smul_apply' : ∀ (a : A₁) (x : L₁), toLieHom (a • x) = σ a • toLieHom x)
  (apply_lie' : ∀ (a : A₁) (x : L₁), σ ⁅x, a⁆ = ⁅toLieHom x, σ a⁆),
  sizeOf { toLieHom := toLieHom, map_smul_apply' := map_smul_apply', apply_lie' := apply_lie' } = 1 + sizeOf toLieHom
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.coe_one : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ⇑1 = 1
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_injective : Function.Injective Real.sigmoid
-- Std.Http.Data.URI.Basic
/-- Finds all values of a query parameter by raw key string. The key is percent-encoded before matching.
 -/
Std.Http.URI.Query.findAll : Std.Http.URI.Query → String → Array (Option Std.Http.URI.EncodedQueryParam)
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.divMonomial_add : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (a b : σ →₀ ℕ) (x : MvPolynomial σ R),
  x.divMonomial (a + b) = (x.divMonomial a).divMonomial b
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (iso : K ≅ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], (HomologicalComplex.homologyMapIso iso i).hom = HomologicalComplex.homologyMap iso.hom i
-- Init.Data.Vector.Lemmas
Vector.flatten_append : ∀ {α : Type u_1} {n m₁ m₂ : ℕ} {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂},
  (xss₁ ++ xss₂).flatten = Vector.cast ⋯ (xss₁.flatten ++ xss₂.flatten)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The inverse in a group object  -/
CategoryTheory.MonObj.«termι[_]» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instIsSMulApply : ∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Monoid S]
  [inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass S R N], IsSMulApply S (QuadraticMap R M N) M N
-- Init.Control.Lawful.MonadAttach.Instances
instWeaklyLawfulMonadAttachEStateM : ∀ {ε σ : Type u}, WeaklyLawfulMonadAttach (EStateM ε σ)
-- Mathlib.Order.Filter.CountablyGenerated
/-- The set of sets of the filter basis is countable.  -/
Filter.CountableFilterBasis.countable : ∀ {α : Type u_6} (self : Filter.CountableFilterBasis α), self.sets.Countable
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.toMatrix_sylvesterMap : ∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n),
  (LinearMap.toMatrix ((Polynomial.degreeLT.basis R m).prod (Polynomial.degreeLT.basis R n))
        (Polynomial.degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n)
-- Mathlib.Algebra.Field.Defs
/-- `a / b := a * b⁻¹`  -/
DivisionRing.div_eq_mul_inv : ∀ {K : Type u_2} [self : DivisionRing K] (a b : K), a / b = a * b⁻¹
-- Init.Data.String.TakeDrop
String.Internal.isPrefixOfImpl : String → String → Bool
-- Mathlib.Data.List.Sigma
List.dlookup_map : ∀ {α : Type u} {α' : Type u'} {β : α → Type v} {β' : α' → Type v'} [inst : DecidableEq α] [inst_1 : DecidableEq α']
  (l : List (Sigma β)) {f : α → α'},
  Function.Injective f →
    ∀ (g : (a : α) → β a → β' (f a)) (a : α),
      List.dlookup (f a) (List.map (Sigma.map f g) l) = Option.map (g a) (List.dlookup a l)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid.size_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α},
  (Ordnode.node s l x r).Valid → (Ordnode.node s l x r).size = l.size + r.size + 1
-- Mathlib.Order.SymmDiff
symmDiff_eq' : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), symmDiff a b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
-- Mathlib.Data.Vector.Basic
List.Vector.head_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : List.Vector α (n + 1))
  (hp : ∀ x ∈ v.toList, p x), (List.Vector.pmap f v hp).head = f v.head ⋯
-- Mathlib.Algebra.Lie.Sl2
/-- The subalgebra associated to an `sl₂` triple.  -/
IsSl2Triple.toLieSubalgebra : (R : Type u_1) →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → {h e f : L} → IsSl2Triple h e f → LieSubalgebra R L
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- `Polynomial.C` as an `AlgHom`.  -/
Polynomial.CAlgHom : {R : Type u} →
  {A : Type z} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A →ₐ[R] Polynomial A
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_indep_chart : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {e : OpenPartialHomeomorph M H} {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s : Set M},
  G.LocalInvariantProp G' P →
    e ∈ StructureGroupoid.maximalAtlas M G →
      f ∈ StructureGroupoid.maximalAtlas M' G' →
        ChartedSpace.LiftPropOn P g s →
          ∀ {y : H}, y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source) → P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) y
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_toMeasurable : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Set α),
  μ (MeasureTheory.toMeasurable μ s) = μ s
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `(F', α)` is a right Kan extension of `F` along `L` and `β : L ⋙ G ⟶ F` is
a natural transformation, this is the induced morphism `G ⟶ F'`.  -/
CategoryTheory.Functor.liftOfIsRightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : L.comp F' ⟶ F) →
                    [F'.IsRightKanExtension α] → (G : CategoryTheory.Functor D H) → (L.comp G ⟶ F) → (G ⟶ F')
-- Mathlib.Analysis.Convex.Join
Convex.convexJoin : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s t : Set E}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (convexJoin 𝕜 s t)
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedAddGroup.toNNNorm.eq_1 : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], SeminormedAddGroup.toNNNorm = { nnnorm := fun a => NNReal.mk ‖a‖ ⋯ }
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
/-- Euclid's lemma: if `a ∣ b * c` and `a` and `c` have no common prime factors, `a ∣ b`.
Compare `IsCoprime.dvd_of_dvd_mul_left`.  -/
UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b c : R},
  a ≠ 0 → (∀ ⦃d : R⦄, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
-- Lean.Meta.LazyDiscrTree
/-- `LazyDiscrTree` is a variant of the discriminator tree datatype
`DiscrTree` in Lean core that is designed to be efficiently
initializable with a large number of patterns.  This is useful
in contexts such as searching an entire Lean environment for
expressions that match a pattern.

Lazy discriminator trees achieve good performance by minimizing
the amount of work that is done up front to build the discriminator
tree.  When first adding patterns to the tree, only the root
discriminator key is computed and processing the remaining
terms is deferred until demanded by a match.
 -/
Lean.Meta.LazyDiscrTree : Type → Type
-- Mathlib.Algebra.Ring.Equiv
/-- If two rings are isomorphic, and the second doesn't have zero divisors,
then so does the first.  -/
MulEquiv.noZeroDivisors : ∀ {A : Type u_7} (B : Type u_8) [inst : MulZeroClass A] [inst_1 : MulZeroClass B] [NoZeroDivisors B] (e : A ≃* B),
  NoZeroDivisors A
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.instSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S), E.Small
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget₂Mon_comp_forget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.Grp.forget₂Mon C).comp (CategoryTheory.Mon.forget C) = CategoryTheory.Grp.forget C
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.extendScalars_σ : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (a : S), P.extendScalars.σ a = P.σ a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : SizeOf C]
  (F : CategoryTheory.Limits.MonoFactorisation f) (isImage : CategoryTheory.Limits.IsImage F),
  sizeOf { F := F, isImage := isImage } = 1 + sizeOf F + sizeOf isImage
-- Mathlib.CategoryTheory.Category.PartialFun
/-- Forgetting that maps are total and making them total again by adding a point is the same as just
adding a point.  -/
typeToPartialFunIsoPartialFunToPointed : typeToPartialFun.comp partialFunToPointed ≅ typeToPointed
-- Init.Data.Array.Lemmas
Array.size_extract_loop : ∀ {α : Type u_1} {xs ys : Array α} {size start : ℕ},
  (Array.extract.loop xs size start ys).size = ys.size + min size (xs.size - start)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Complex.differentiableAt_log : ∀ {z : ℂ}, z ∈ Complex.slitPlane → DifferentiableAt ℂ Complex.log z
-- Lean.Meta.Match.Match
/-- Overlapped alternatives.
Stored as ordered pairs `(overlapping,overlapped) ∈ overlaps`.
Used during splitter generation to avoid going through all pairs of patterns.
 -/
Lean.Meta.Match.State.overlaps : Lean.Meta.Match.State → Lean.Meta.Match.Overlaps
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- The diffeomorphism given by scalar multiplication by an element of a group `G` acting
Cⁿ-differentiably on a manifold `M` is a diffeomorphism from `M` to itself. Its inverse is scalar
multiplication by `g⁻¹`.  -/
Diffeomorph.smul : {𝕜 : 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) →
                {H' : Type u_4} →
                  [inst_4 : TopologicalSpace H'] →
                    {E' : Type u_5} →
                      [inst_5 : NormedAddCommGroup E'] →
                        [inst_6 : NormedSpace 𝕜 E'] →
                          (I' : ModelWithCorners 𝕜 E' H') →
                            {G : Type u_8} →
                              [inst_7 : TopologicalSpace G] →
                                [inst_8 : ChartedSpace H G] →
                                  {M : Type u_9} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H' M] →
                                        [inst_11 : Group G] →
                                          [inst_12 : MulAction G M] →
                                            (n : WithTop ℕ∞) → [ContMDiffSMul I I' n G M] → G → Diffeomorph I' I' M M n
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (x : ↑X),
  TopCat.Presheaf.stalkFunctor C x =
    ((CategoryTheory.Functor.whiskeringLeft (TopologicalSpace.OpenNhds x)ᵒᵖ (TopologicalSpace.Opens ↑X)ᵒᵖ C).obj
          (TopologicalSpace.OpenNhds.inclusion x).op).comp
      CategoryTheory.Limits.colim
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_rotateRightAux_of_lt : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ}, i < r → (x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r))
-- Mathlib.Computability.Primrec.List
Primrec.list_idxOf : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : DecidableEq α], Primrec₂ List.idxOf
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_le_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], Cardinal.toENat c ≤ OfNat.ofNat n ↔ c ≤ OfNat.ofNat n
-- Mathlib.Data.Vector.Basic
List.Vector.ext_iff : ∀ {α : Type u_1} {n : ℕ} {v w : List.Vector α n}, v = w ↔ ∀ (m : Fin n), v.get m = w.get m
-- ProofWidgets.Component.Basic
ProofWidgets.instRpcEncodableInteractiveMessageProps : Lean.Server.RpcEncodable ProofWidgets.InteractiveMessageProps
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.not_isStrongLimit_zero : ¬Cardinal.IsStrongLimit 0
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableAux.mk.sizeOf_spec : ∀ {Γ₀ Γ₁ : Type} [inst : SizeOf Γ₀] [inst_1 : SizeOf Γ₁] (tm : Turing.FinTM2) (inputAlphabet : tm.Γ tm.k₀ ≃ Γ₀)
  (outputAlphabet : tm.Γ tm.k₁ ≃ Γ₁),
  sizeOf { tm := tm, inputAlphabet := inputAlphabet, outputAlphabet := outputAlphabet } =
    1 + sizeOf tm + sizeOf inputAlphabet + sizeOf outputAlphabet
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.vadd_subset_self : ∀ {S : Type u_1} {R : Type u_2} {M : Type u_3} [inst : SetLike S M] [inst_1 : VAdd R M] [VAddMemClass S R M] (r : R)
  (s : S), r +ᵥ ↑s ⊆ ↑s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_mem_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.insert k → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil_iff_support_eq : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, p.Nil ↔ p.support = [v]
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.trans_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsFibrant A] (P P' : HomotopicalAlgebra.PathObject A) [inst_3 : P'.IsGood],
  (P.trans P').p₀ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst P.p₁ P'.p₀) P.p₀
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.simpLoop.visitPostContinue : Lean.Expr → Lean.Meta.Simp.Config → Lean.Meta.Simp.Result → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldlM.eq_def : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} [inst : Monad m] (f : σ → α → m σ) (x : σ)
  (x_1 : RBTree.RBNode α),
  RBTree.RBNode.foldlM f x x_1 =
    match x, x_1 with
    | b, RBTree.RBNode.nil => pure b
    | b, RBTree.RBNode.node c l v r => do
      let __do_lift ← RBTree.RBNode.foldlM f b l
      let __do_lift ← f __do_lift v
      RBTree.RBNode.foldlM f __do_lift r
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_of_lt : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < b → Order.succ a ≤ b
-- Mathlib.Logic.Basic
or_congr_left' : ∀ {c a b : Prop}, (¬c → (a ↔ b)) → (a ∨ c ↔ b ∨ c)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_tensorHom : ∀ {R : Type u} [inst : CommRing R] {K L M N : ModuleCat R} (f : K ⟶ L) (g : M ⟶ N),
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    TensorProduct.map (ModuleCat.Hom.hom f) (ModuleCat.Hom.hom g)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceEquiv_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X),
  f.iteratedSliceEquiv.functor = f.iteratedSliceForward
-- Mathlib.Topology.Bases
/-- The topology is generated by sets from `s`.  -/
TopologicalSpace.IsTopologicalBasis.eq_generateFrom : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis s → t = TopologicalSpace.generateFrom s
-- Batteries.Data.AssocList
List.length_toAssocList : ∀ {α : Type u_1} {β : Type u_2} (l : List (α × β)), l.toAssocList.length = l.length
-- Mathlib.Data.List.Infix
List.singleton_infix_singleton_iff : ∀ {α : Type u_1} {x y : α}, [x] <:+: [y] ↔ x = y
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α n},
  T.Iff φ ψ → T.Iff φ.not ψ.not
-- Mathlib.SetTheory.ZFC.PSet
PSet.brecOn.eq : ∀ {motive : PSet.{u} → Sort u_1} (t : PSet.{u}) (F_1 : (t : PSet.{u}) → PSet.below t → motive t),
  PSet.brecOn t F_1 = F_1 t (PSet.brecOn.go t F_1).2
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `fallback` if no such key exists.
 -/
Std.TreeMap.getKeyLTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α → α
-- Mathlib.Data.Finset.Option
Option.toFinset_none : ∀ {α : Type u_1}, none.toFinset = ∅
-- Mathlib.Order.Filter.Germ.Basic
/-- Given a germ `f : Germ l β` and a function `g : γ → α`, where `l : Filter α`, if `g` tends
to `l` along `lc : Filter γ`, then the composition `f ∘ g` is well-defined as a germ at `lc`.  -/
Filter.Germ.compTendsto : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {l : Filter α} → l.Germ β → {lc : Filter γ} → (g : γ → α) → Filter.Tendsto g lc l → lc.Germ β
-- Mathlib.Analysis.Normed.Group.Uniform
dist_self_mul_left : ∀ {E : Type u_2} [inst : SeminormedGroup E] (a b : E), dist (b * a) b = ‖a‖
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.carrier : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → AlgebraicGeometry.PresheafedSpace C → TopCat
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso_hom_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom =
        CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w).hom.fst = eₗ.hom
-- Init.Data.Slice.Array.Lemmas
Subarray.sliceFoldl_eq_foldl : ∀ {β : Type u_1} {init : β} {α : Type u} {s : Subarray α} {f : β → α → β},
  Std.Slice.foldl f init s = Std.Slice.foldl f init s
-- Mathlib.Data.Nat.Nth
Nat.nth_lt_nth' : ∀ {p : ℕ → Prop} {m n : ℕ}, m < n → (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → Nat.nth p m < Nat.nth p n