mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.smul_comm : ∀ {α : Type u_1} {𝕜' : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] [inst_4 : NormedRing 𝕜'] [inst_5 : Module 𝕜' E]
  [inst_6 : Module 𝕜' 𝕜] [inst_7 : IsBoundedSMul 𝕜' E] [IsBoundedSMul 𝕜' 𝕜] [SMulCommClass 𝕜' 𝕜 E] (c : 𝕜')
  (f : ↥(MeasureTheory.Lp 𝕜 p μ)) (g : ↥(MeasureTheory.Lp E q μ)), c • f • g = f • c • g
-- Mathlib.Algebra.Ring.Defs
/-- A `Semiring` which `IsMulCommutative` is a `CommSemiring`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instCommSemiring : {R : Type v} → [inst : Semiring R] → [IsMulCommutative R] → CommSemiring R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.ofList_eq_insertMany! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {l : List (α × β)},
  Std.DTreeMap.Internal.Impl.Const.ofList l =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! Std.DTreeMap.Internal.Impl.empty l)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.add : ∀ {α : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {f g : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport (f + g)
-- Mathlib.Data.Finset.Slice
Set.sized_singleton : ∀ {α : Type u_1} {s : Finset α} {r : ℕ}, Set.Sized r {s} ↔ s.card = r
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations. See also
`Bundle.Trivialization.coordChangeHomeomorph` for a version bundled as `F ≃ₜ F`.  -/
Bundle.Trivialization.coordChange : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] → Bundle.Trivialization F proj → Bundle.Trivialization F proj → B → F → F
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.MeasurePreserving (⇑(NumberField.mixedEmbedding.euclidean.toMixed K)) MeasureTheory.volume
    MeasureTheory.volume
-- Batteries.Data.Vector.Lemmas
Vector.scanl_map : ∀ {γ : Type u_1} {β : Type u_2} {α : Type u_3} {n : ℕ} {init : γ} {f : γ → β → γ} {g : α → β} {as : Vector α n},
  Vector.scanl f init (Vector.map g as) = Vector.scanl (fun x1 x2 => f x1 (g x2)) init as
-- Mathlib.Topology.Separation.Regular
/-- Given two separable points `x` and `y`, we can find neighbourhoods
`x ∈ V₁ ⊆ U₁` and `y ∈ V₂ ⊆ U₂`, with the `Vₖ` closed and the `Uₖ` open,
such that the `Uₖ` are disjoint.  -/
disjoint_nested_nhds_of_not_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {x y : X},
  ¬Inseparable x y →
    ∃ U₁ ∈ nhds x,
      ∃ V₁ ∈ nhds x,
        ∃ U₂ ∈ nhds y,
          ∃ V₂ ∈ nhds y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
-- Mathlib.Algebra.Module.GradedModule
SetLike.gdistribMulAction : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {A : Type u_4} →
      {M : Type u_5} →
        {σ : Type u_6} →
          {σ' : Type u_7} →
            [inst : AddMonoid ιA] →
              [inst_1 : AddAction ιA ιM] →
                [inst_2 : Semiring A] →
                  (𝓐 : ιA → σ') →
                    [inst_3 : SetLike σ' A] →
                      (𝓜 : ιM → σ) →
                        [inst_4 : AddMonoid M] →
                          [inst_5 : DistribMulAction A M] →
                            [inst_6 : SetLike σ M] →
                              [inst_7 : AddSubmonoidClass σ M] →
                                [inst_8 : SetLike.GradedMonoid 𝓐] →
                                  [SetLike.GradedSMul 𝓐 𝓜] →
                                    DirectSum.GdistribMulAction (fun i => ↥(𝓐 i)) fun i => ↥(𝓜 i)
-- Mathlib.Computability.Encoding
Computability.Encoding.card_le_card_list : ∀ {α : Type u} {Γ : Type v} (e : Computability.Encoding α Γ),
  Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk (List Γ))
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- A family of `MvPowerSeries` is summable if their order tends to infinity.  -/
MvPowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_3}
  {f : ι → MvPowerSeries σ R} [inst_2 : LinearOrder ι] [LocallyFiniteOrderBot ι],
  Filter.Tendsto (fun i => (f i).order) Filter.atTop (nhds ⊤) → Summable f
-- Lean.Server.Requests
Lean.Server.RequestError.message : Lean.Server.RequestError → String
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundariesToCocycles₁_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{max u u_1, u, u} k G}
  (x : ↥(groupCohomology.coboundaries₁ A)), ⇑((groupCohomology.coboundariesToCocycles₁ A) x) = ↑x
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.smul_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F},
  f =o[𝕜; l] g → ∀ (c : α → 𝕜), (fun x => c x • f x) =o[𝕜; l] fun x => c x • g x
-- Mathlib.Order.Disjoint
Complementeds.coe_inj : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {a b : Complementeds α}, ↑a = ↑b ↔ a = b
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.apply_coe_mem_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (K : Subgroup G) (x : ↥K),
  f ↑x ∈ Subgroup.map f K
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- Given a signed measure `s` and a measure `μ`, `s.singularPart μ` is the signed measure
such that `s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s` and
`s.singularPart μ` is mutually singular with respect to `μ`.  -/
MeasureTheory.SignedMeasure.singularPart : {α : Type u_1} →
  {m : MeasurableSpace α} → MeasureTheory.SignedMeasure α → MeasureTheory.Measure α → MeasureTheory.SignedMeasure α
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.CMExtension.equivMaximalRealSubfield_apply : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : NumberField.IsTotallyReal F] [inst_2 : Field K]
  [inst_3 : CharZero K] [inst_4 : Algebra.IsIntegral ℚ K] [inst_5 : NumberField.IsTotallyComplex K]
  [inst_6 : Algebra F K] [inst_7 : Algebra.IsQuadraticExtension F K] (x : F),
  ↑((NumberField.CMExtension.equivMaximalRealSubfield F K) x) = (algebraMap F K) x
-- Mathlib.GroupTheory.PresentedGroup
/-- The canonical inclusion map from the disjoint union of types to the free product of the relations
 -/
PresentedGroup.toCoprod : {α : Type u_1} →
  {β : Type u_2} →
    (rels₁ : Set (FreeGroup α)) →
      (rels₂ : Set (FreeGroup β)) → α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)
-- Mathlib.Analysis.Meromorphic.Basic
/-- `Meromorphic` is invariant under translation.  -/
Meromorphic.meromorphic_comp_add_const_iff_meromorphic : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜}, Meromorphic (f ∘ fun x => x + c) ↔ Meromorphic f
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_cases : ∀ (n m : ℤ), n.tdiv m = if 0 ≤ n then if 0 ≤ m then n / m else -(n / -m) else if 0 ≤ m then -(-n / m) else -n / -m
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), CategoryTheory.Sieve.functorPullback F ⊤ = ⊤
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundariesOfIsCoboundary₁_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] {f : G → A} (hf : groupCohomology.IsCoboundary₁ f)
  (a : G), ↑(groupCohomology.coboundariesOfIsCoboundary₁ hf) a = f a
-- Mathlib.Algebra.GroupWithZero.Submonoid.Instances
MonoidWithZeroHom.instMulZeroOneClassSubtypeMemSubmonoidMrange : {G : Type u_1} →
  {H : Type u_2} →
    [inst : MulZeroOneClass G] → [inst_1 : MulZeroOneClass H] → (f : G →*₀ H) → MulZeroOneClass ↥(MonoidHom.mrange f)
-- Mathlib.Tactic.Convert
Convert.ExpensiveConfig.mk.injEq : ∀ (toConfig toConfig_1 : Congr!.Config),
  ({ toConfig := toConfig } = { toConfig := toConfig_1 }) = (toConfig = toConfig_1)
-- Lean.Data.PersistentArray
Lean.PersistentArray.branching : USize
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
IsSelfAdjoint.sq_spectrumRestricts : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A},
  IsSelfAdjoint a → SpectrumRestricts (a ^ 2) ⇑ContinuousMap.realToNNReal
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.IntegrableOn.iUnion_finite : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} [Finite ι] {t : ι → Set X},
  (∀ (i : ι), MeasurableSet (t i)) → (∀ (i : ι), μ.IntegrableOn f (t i)) → μ.IntegrableOn f (⋃ i, t i)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} {h : X ⟶ P.P}
  {h₀ :
    autoParam (CategoryTheory.CategoryStruct.comp h P.p₀ = f)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀._autoParam}
  {h₁ :
    autoParam (CategoryTheory.CategoryStruct.comp h P.p₁ = g)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁._autoParam}
  {h_1 : X ⟶ P.P}
  {h₀_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h_1 P.p₀ = f)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀._autoParam}
  {h₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h_1 P.p₁ = g)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁._autoParam},
  { h := h, h₀ := h₀, h₁ := h₁ } = { h := h_1, h₀ := h₀_1, h₁ := h₁_1 } → h = h_1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `c ≠ 0`. See `mul_div_mul_left`.  -/
le_mul_div_mul_left : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : Preorder G₀] {a b c : G₀}, a / b ≤ 0 → a / b ≤ c * a / (c * b)
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.forall_monoidHom_apply_eq_one_iff : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G) (x : G),
  (∀ (φ : G →* Mˣ), (∀ y ∈ H, φ y = 1) → φ x = 1) ↔ x ∈ H
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mk.inj : ∀ {R : Type u} {M : Type v} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  {toAddSubmonoid : AddSubmonoid M}
  {smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier}
  {toAddSubmonoid_1 : AddSubmonoid M}
  {smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier},
  { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' } =
      { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 } →
    toAddSubmonoid = toAddSubmonoid_1
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coePNat_nat : ∀ (v : PrimeMultiset), Multiset.map PNat.val v.toPNatMultiset = v.toNatMultiset
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_eq_zero : ∀ {n : ℕ} (x : ZMod n), x.valMinAbs = 0 ↔ x = 0
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {s : Set α} {a : α}, IsLocalMinOn f s a → ∀ {g : β → γ}, Antitone g → IsLocalMaxOn (g ∘ f) s a
-- Mathlib.Algebra.Order.Group.PosPart
negPart_def : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] (a : α), a⁻ = -a ⊔ 0
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_symm_toLinearEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ⇑e.toLinearEquiv.symm = ⇑e.symm
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_associator_inv_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 : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y Z : C) {Z_1 : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) h))))
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.map_comp_ιMulti : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {n : ℕ} (f : M →ₗ[R] N),
  (ExteriorAlgebra.map f).toLinearMap.compAlternatingMap (ExteriorAlgebra.ιMulti R n) =
    (ExteriorAlgebra.ιMulti R n).compLinearMap f
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- `C a` is the constant SkewPolynomial `a`. `C` is provided as an additive homomorphism.  -/
SkewPolynomial.C : {R : Type u_1} → [inst : Semiring R] → R →+ SkewPolynomial R
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- Given `X : DerivedCategory C` and `n : ℤ`, this property means
that `X` is `≥ n` for the canonical t-structure.  -/
DerivedCategory.IsGE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [inst_2 : HasDerivedCategory C] → DerivedCategory C → ℤ → Prop
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkBEqNatInstance : Lean.Expr
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_subset_uIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.uIoc a b ⊆ Set.uIcc a b
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
/-- The generating function of `Nat.Partition.restricted n p` is
$$
\prod_{i \in p} \sum_{j = 0}^{\infty} X^{ij}
$$  -/
Nat.Partition.hasProd_powerSeriesMk_card_restricted : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R] [inst_2 : CommSemiring R] [IsTopologicalSemiring R]
  (p : ℕ → Prop) [inst_4 : DecidablePred p],
  HasProd (fun i => if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1)
    (PowerSeries.mk fun n => ↑(Nat.Partition.restricted n p).card)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.adjoint_mapL : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] [inst_9 : CompleteSpace E]
  [inst_10 : CompleteSpace G] [inst_11 : CompleteSpace (TensorProduct 𝕜 E G)] [inst_12 : CompleteSpace F]
  [inst_13 : CompleteSpace H] [inst_14 : CompleteSpace (TensorProduct 𝕜 F H)] (f : E →L[𝕜] F) (g : G →L[𝕜] H),
  ContinuousLinearMap.adjoint (TensorProduct.mapL f g) =
    TensorProduct.mapL (ContinuousLinearMap.adjoint f) (ContinuousLinearMap.adjoint g)
-- Aesop.Stats.Basic
Aesop.ForwardClusterStateStats.mk.inj : ∀ {slots : ℕ} {instantiationStats : Array Aesop.ForwardInstantiationStats} {slots_1 : ℕ}
  {instantiationStats_1 : Array Aesop.ForwardInstantiationStats},
  { slots := slots, instantiationStats := instantiationStats } =
      { slots := slots_1, instantiationStats := instantiationStats_1 } →
    slots = slots_1 ∧ instantiationStats = instantiationStats_1
-- Init.Data.String.Substring
Substring.Raw.Internal.beqImpl : Substring.Raw → Substring.Raw → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forIn (fun k v => f ⟨k, v⟩) init t = forIn t.toArray init f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_eq_getD_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t.minKeyD fallback = t.keysArray.getD 0 fallback
-- Mathlib.Algebra.Order.Round
round_two_inv : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α], round 2⁻¹ = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.containsThenInsertIfNew! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β},
  l.WF → (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! k v l).2.WF
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Fintype.linearCombination.eq_1 : ∀ {α : 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] (v : α → M),
  Fintype.linearCombination R v = { toFun := fun f => ∑ i, f i • v i, map_add' := ⋯, map_smul' := ⋯ }
-- Init.Data.Rat.Lemmas
Rat.add_comm : ∀ (a b : ℚ), a + b = b + a
-- Mathlib.Analysis.Normed.Field.Ultra
/-- To prove that a normed division ring is nonarchimedean, it suffices to prove that the norm
of the image of any natural is less than or equal to one.  -/
IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one : ∀ {R : Type u_1} [inst : NormedDivisionRing R], (∀ (n : ℕ), ‖↑n‖ ≤ 1) → IsUltrametricDist R
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instOneCoeOfOneMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → One (R i)] →
              [∀ (i : ι), OneMemClass (S i) (R i)] → One (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddCommGroup.toPseudoMetricSpace : {E : Type u_8} → [self : SeminormedAddCommGroup E] → PseudoMetricSpace E
-- Batteries.Recycling.RBTree.Depth
_private.Batteries.Recycling.RBTree.Depth.0.RBTree.RBNode.depth.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c a v b => h_2 c a v b) =
    h_1 ()
-- Init.Data.SInt.Lemmas
Int16.le_total : ∀ (a b : Int16), a ≤ b ∨ b ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mkIso_inv_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right)
  (base : ψ.base ≅ ψ'.base)
  (left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left.hom F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_1)
  (right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right.hom G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_3),
  (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).inv.left = left.inv
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualLift_of_subtype : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Subspace K V}
  {φ : Module.Dual K ↥W} (w : ↥W), (W.dualLift φ) ↑w = φ w
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_ofNat : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (n : ℕ) [inst_2 : n.AtLeastTwo],
  Polynomial.map f (OfNat.ofNat n) = OfNat.ofNat n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.denote_blastGetLsbD : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig) (assign : α → Bool),
  ⟦assign, { aig := aig, ref := Std.Tactic.BVDecide.BVPred.blastGetLsbD aig target }⟧ =
    if h : target.idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get target.idx h }⟧ else false
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.nonzero_image_of_nonzero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasImage f], f ≠ 0 → CategoryTheory.Limits.image.ι f ≠ 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.getElem_toList_eq : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least).get ⋯
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to negative infinity along a nontrivial filter `l`,
then `fun x ↦ f x * r` tends to infinity if and only if `r < 0`.  -/
Filter.tendsto_mul_const_atTop_iff_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ r < 0)