mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Rii α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Rii α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.toConvexCone.eq_1 : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (C : PointedCone R E),
  ↑C = { carrier := ↑C, smul_mem' := ⋯, add_mem' := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ordCompare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap.Raw α β compare},
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α}, compare ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.ulift : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  Module.Free R (ULift.{u_2, v} M)
-- Mathlib.Data.Nat.Init
Nat.leRecOn_succ' : ∀ {C : ℕ → Sort u_1} {n : ℕ} {h : n ≤ n + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  Nat.leRecOn h (fun {k} => next) x = next x
-- Mathlib.Algebra.Group.Conj
AddConjClasses.mem_carrier_iff_mk_eq : ∀ {α : Type u} [inst : AddMonoid α] {a : α} {b : AddConjClasses α}, a ∈ b.carrier ↔ AddConjClasses.mk a = b
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.isSeparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] [Nonempty D],
  CategoryTheory.IsSeparator (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.generator✝ F)
-- Mathlib.Data.Finset.Powerset
/-- The number of `n`-element subsets of `t` containing `s` equals
`Nat.choose (#t - #s) (n - #s)`.  -/
Finset.card_filter_powersetCard_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (n : ℕ),
  s ⊆ t → s.card ≤ n → {x ∈ Finset.powersetCard n t | s ⊆ x}.card = (t.card - s.card).choose (n - s.card)
-- Mathlib.Logic.Basic
Xor.eq_1 : ∀ (a b : Prop), Xor a b = (a ∧ ¬b ∨ b ∧ ¬a)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).leadingCoeff = -p.leadingCoeff
-- Mathlib.Algebra.Order.Interval.Basic
instZeroInterval : {α : Type u_2} → [inst : Preorder α] → [Zero α] → Zero (Interval α)
-- Mathlib.GroupTheory.GroupAction.Basic
/-- An additive action is pretransitive if and only if the quotient by
`AddAction.orbitRel` is a subsingleton.  -/
AddAction.pretransitive_iff_subsingleton_quotient : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.IsPretransitive G α ↔ Subsingleton (AddAction.orbitRel.Quotient G α)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_inf : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] (s t : TopologicalSpace.Compacts α),
  ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.Order.Fin.Basic
Fin.coe_min : ∀ {n : ℕ} (a b : Fin n), ↑(min a b) = min ↑a ↑b
-- Lean.Compiler.InlineAttrs
Lean.Compiler.getInlineAttribute? : Lean.Environment → Lean.Name → Option Lean.Compiler.InlineAttributeKind
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- The forgetful functor from commutative monoid objects to monoid objects.  -/
CategoryTheory.CommMon.forget₂Mon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.CommMon C) (CategoryTheory.Mon C)
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
CategoryTheory.Bundled.mk.injEq : ∀ {c : Type u → Type v} (α : Type u) (str : autoParam (c α) CategoryTheory.Bundled.str._autoParam) (α_1 : Type u)
  (str_1 : autoParam (c α_1) CategoryTheory.Bundled.str._autoParam),
  ({ α := α, str := str } = { α := α_1, str := str_1 }) = (α = α_1 ∧ str ≍ str_1)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.prod_inf_prod : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] [inst_7 : IsScalarTower R B B] [inst_8 : SMulCommClass R B B]
  {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B}, S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.comp_toRingHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [inst_6 : CommRing R''] [inst_7 : CommRing S'']
  [inst_8 : Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [inst_9 : Algebra R R'] [inst_10 : Algebra R' R'']
  [inst_11 : Algebra R R''] [inst_12 : Algebra S S'] [inst_13 : Algebra S' S''] [inst_14 : Algebra S S'']
  [inst_15 : IsScalarTower R R' R''] [inst_16 : IsScalarTower S S' S''] (f : P'.Hom P'') (g : P.Hom P'),
  (f.comp g).toRingHom = f.toRingHom.comp g.toRingHom
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.ι_coprodIsoDirectSum_hom : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : DecidableEq ι]
  [inst_2 : CategoryTheory.Limits.HasCoproduct Z] (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι Z i) (ModuleCat.coprodIsoDirectSum Z).hom =
    ModuleCat.ofHom (DirectSum.lof R ι (fun i => ↑(Z i)) i)
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.isoMk_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X}
  (h : f.obj.left ≅ g.obj.left)
  (w : autoParam (CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow) CategoryTheory.MonoOver.isoMk._auto_1),
  (CategoryTheory.MonoOver.isoMk h w).inv = CategoryTheory.MonoOver.homMk h.inv ⋯
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  (A : Set Gal(K/k)), A ∈ nhds 1 ↔ ∃ L, ↑L.fixingSubgroup ⊆ A
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.isAlgebraic : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], Algebra.IsAlgebraic ℚ K
-- Mathlib.Data.UInt
/-- The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other.  -/
UInt8.toChar : UInt8 → Char
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The sequence `stirlingSeq` is positive for `n > 0`.  -/
Stirling.stirlingSeq'_pos : ∀ (n : ℕ), 0 < Stirling.stirlingSeq (n + 1)
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- An open map `f : X ⟶ Y` induces an adjunction between `OpenNhds x` and `OpenNhds (f x)`.  -/
IsOpenMap.adjunctionNhds : {X Y : TopCat} →
  {f : X ⟶ Y} →
    (h : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) →
      (x : ↑X) → h.functorNhds x ⊣ TopologicalSpace.OpenNhds.map f x
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2_smul_single_i₁ : ∀ {F : Type u_1} [inst : Field F] {a : F} (ha : a ≠ 0),
  Matrix.SpecialLinearGroup.diag2 a ha • Pi.single 0 1 = a • Pi.single 0 1
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.DihedralGroup.mul.eq_1 : ∀ {n : ℕ} (a b : ZMod n), DihedralGroup.mul✝ (DihedralGroup.r a) (DihedralGroup.r b) = DihedralGroup.r (a + b)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- We state it as a simp lemma, which is regarded as an involved version of
`id_whiskerRight X Y : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)`.
 -/
CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom Y)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom h)
-- Std.Time.Format.Modifier
Std.Time.Modifier.v.sizeOf_spec : ∀ (presentation : Std.Time.ZoneName), sizeOf (Std.Time.Modifier.v presentation) = 1 + sizeOf presentation
-- Mathlib.Data.Fintype.EquivFin
Fintype.bijective_iff_injective_and_card : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Bijective f ↔ Function.Injective f ∧ Fintype.card α = Fintype.card β
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.getConfig : Lean.Meta.Try.Collector.M Lean.Try.Config
-- Aesop.Tree.Data
Aesop.Goal.setPreNormGoal : Lean.MVarId → Aesop.Goal → Aesop.Goal
-- Lean.Meta.MkIffOfInductiveProp
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.Shape.mk : List Bool → Option ℕ → Lean.Meta.Shape✝
-- Mathlib.Topology.Algebra.Group.Quotient
/-- A quotient of a locally compact group is locally compact.  -/
QuotientGroup.instLocallyCompactSpace : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] [LocallyCompactSpace G]
  (N : Subgroup G), LocallyCompactSpace (G ⧸ N)
-- Batteries.Control.AlternativeMonad
/-- Sequencing a `failure` call results in failure  -/
LawfulAlternative.failure_seq : ∀ {m : Type u_1 → Type u_2} {inst : Alternative m} [self : LawfulAlternative m] {α β : Type u_1} (x : m α),
  failure <*> x = failure
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGE_reverse`. -/
List.SortedGE.of_reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.reverse.SortedGE → l.SortedLE
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- There are `catalan n` Dyck words of semilength `n` (or length `2 * n`).  -/
DyckWord.card_dyckWord_semilength_eq_catalan : ∀ (n : ℕ), Fintype.card { p // p.semilength = n } = catalan n
-- Mathlib.Order.Monotone.Basic
StrictMono.wellFoundedGT : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} [WellFoundedGT β],
  StrictMono f → WellFoundedGT α
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddSemigroup.eq_zero_or_toFreeAddMonoid : ∀ {α : Type u_1} (x : FreeAddMonoid α), x = 0 ∨ ∃ y, FreeAddSemigroup.toFreeAddMonoid y = x
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_π_app_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A]
  (i : I),
  ↑((CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).π.app i) =
    CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.CategoryOfElements.π A)) i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_8 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (n : ℕ) (rhs : Std.Tactic.BVDecide.BVExpr n)
  (lhs : Std.Tactic.BVDecide.BVExpr w),
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftLeft rhs) =
    Std.Tactic.BVDecide.BVExpr.eval assign lhs <<< Std.Tactic.BVDecide.BVExpr.eval assign rhs
-- Mathlib.MeasureTheory.Measure.Prod
/-- Two finite measures on a product that are equal on products of sets are equal.  -/
MeasureTheory.Measure.ext_prod : ∀ {α : Type u_4} {β : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure (α × β)}
  [MeasureTheory.IsFiniteMeasure μ],
  (∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)) → μ = ν
-- Mathlib.Data.List.Permutation
/-- A list is a permutation of the pair `[a, b]` if and only if it is equal to `[a, b]` or to
`[b, a]`.  -/
List.perm_pair : ∀ {α : Type u_1} {a b : α} {l : List α}, l.Perm [a, b] ↔ l = [a, b] ∨ l = [b, a]
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
isIntegral_quotientMap_iff : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {I : Ideal S},
  (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral
-- Lean.Compiler.IR.Basic
Lean.IR.Param.borrow : Lean.IR.Param → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {l : List α} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.Const.insertManyIfNewUnit m l) k = ()
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- `Spec (𝒪ₓ(U)/I(U))`, the object to be glued into the closed subscheme.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → ↑X.affineOpens → AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.algebraMap_mk' : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} (T : Type u_1) [inst_1 : CommSemiring T] [inst_2 : Algebra R T]
  [inst_3 : IsLocalization S T] {A : Type u_3} [inst_4 : Semiring A] [inst_5 : Algebra R A] (a : R) (s : ↥S),
  (algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = LocalizedModule.mk ((algebraMap R A) a) s
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.congr_map : ∀ {U : Type u_1} {V : Type u_2} [inst : CategoryTheory.ReflQuiver U] [inst_1 : CategoryTheory.ReflQuiver V]
  (F : U ⥤rq V) {X Y : U} {f g : X ⟶ Y}, f = g → F.map f = F.map g
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcReleaseParams.mk : Lean.Lsp.DocumentUri → UInt64 → Array Lean.Json → Lean.Lsp.RpcReleaseParams
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- A special case of `integral_Ioi_of_hasDerivAt_of_tendsto` where we assume that `f` is C^1 with
compact support.  -/
HasCompactSupport.integral_Ioi_deriv_eq : ∀ {E : Type u_1} {f : ℝ → E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E],
  ContDiff ℝ 1 f → HasCompactSupport f → ∀ (b : ℝ), ∫ (x : ℝ) in Set.Ioi b, deriv f x = -f b
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.cone_pt : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) [inst_2 : CategoryTheory.IsCofiltered J], h.cone.pt = F.obj i₀
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [T2Space M] {a b : ℝ}
  [BoundarylessManifold I M],
  t₀ ∈ Set.Ioo a b →
    (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
      IsMIntegralCurveOn γ v (Set.Ioo a b) →
        IsMIntegralCurveOn γ' v (Set.Ioo a b) → γ t₀ = γ' t₀ → Set.EqOn γ γ' (Set.Ioo a b)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_neg'`.  -/
Left.add_neg' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, a < 0 → b < 0 → a + b < 0
-- Batteries.Control.LawfulMonadState
liftM_modifyGet : ∀ {σ α : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [inst : MonadStateOf σ m]
  [inst_1 : MonadLift m n] (f : σ → α × σ), liftM (modifyGet f) = modifyGet f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.length_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.toList.length = t.size
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialTermInfo.mk.sizeOf_spec : ∀ (toElabInfo : Lean.Elab.ElabInfo) (lctx : Lean.LocalContext) (expectedType? : Option Lean.Expr),
  sizeOf { toElabInfo := toElabInfo, lctx := lctx, expectedType? := expectedType? } =
    1 + sizeOf toElabInfo + sizeOf lctx + sizeOf expectedType?
-- Init.Data.UInt.Lemmas
USize.pow_succ : ∀ (x : USize) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α], r.isEmpty = true ↔ ∀ (a : α), a ∉ r
-- Mathlib.Analysis.Complex.Exponential
Real.exp_ne_zero : ∀ (x : ℝ), Real.exp x ≠ 0
-- Mathlib.Order.Interval.Finset.Defs
instFiniteSubtypeLtOfLocallyFiniteOrderBot : ∀ {α : Type u_1} [inst : Preorder α] {y : α} [LocallyFiniteOrderBot α], Finite { x // x < y }
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instSMulCommClass : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {a b : R} [inst : SMul S R] [inst_1 : SMul T R] [SMulCommClass S T R],
  SMulCommClass S T (QuadraticAlgebra R a b)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instSetLike : {G : Type u_1} → [inst : AddGroup G] → SetLike (FiniteIndexNormalAddSubgroup G) G
-- Init.Prelude
/-- Equality is transitive: if `a = b` and `b = c` then `a = c`.

Because this is in the `Eq` namespace, if you have variables or expressions
`h₁ : a = b` and `h₂ : b = c`, you can use `h₁.trans h₂ : a = c` as shorthand
for `Eq.trans h₁ h₂`.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
Eq.trans : ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality_obj_inl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  (A : CategoryTheory.Limits.BinaryBicone P Q),
  ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).inl = F.map A.inl
-- Mathlib.Order.Lex
ofLex_toLex : ∀ {α : Type u_1} (a : α), ofLex (toLex a) = a
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_succ : ∀ (a : Cardinal.{u}), Cardinal.lift.{v, u} (Order.succ a) = Order.succ (Cardinal.lift.{v, u} a)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.rightUnshift_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ)
  (hn : n' + a = n), ↑(γ.rightUnshift n hn) = (↑γ).rightUnshift n hn
-- Mathlib.Topology.Algebra.GroupWithZero
continuousOn_div : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] [ContinuousMul G₀],
  ContinuousOn (fun p => p.1 / p.2) {p | p.2 ≠ 0}
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.one_add_X_pow_sub_X_pow : ∀ {S : Type u_1} [inst : CommRing S] (d : ℕ),
  (1 + Polynomial.X) ^ d - Polynomial.X ^ d = ∑ i ∈ Finset.range d, d.choose i • Polynomial.X ^ i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is an additive group object and `F` is monoidal,
then `Hom(X, G) → Hom(F X, F G)` preserves negation.  -/
CategoryTheory.Functor.map_neg' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] {X G : C} (f : X ⟶ G) [inst_5 : CategoryTheory.AddGrpObj G],
  F.map (-f) = -F.map f
-- Mathlib.LinearAlgebra.Dual.BaseChange
_private.Mathlib.LinearAlgebra.Dual.BaseChange.0.IsBaseChange.toDualBaseChangeAux.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j j_1 : V →ₗ[R] W} (e_j : j = j_1) (ibc : IsBaseChange A j),
  IsBaseChange.toDualBaseChangeAux✝ ibc = IsBaseChange.toDualBaseChangeAux✝ ⋯
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_apply_zero : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1), (AffineMap.lineMap p₀ p₁) 0 = p₀
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_PInfty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f AlgebraicTopology.DoldKan.PInfty =
    s.toKaroubiNondegComplexIsoN₁.hom.f
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Node.collision.congr_simp : ∀ {α : Type u} {β : Type v} (ks ks_1 : Array α) (e_ks : ks = ks_1) (vs vs_1 : Array β) (e_vs : vs = vs_1)
  (h : ks.size = vs.size),
  Lean.PersistentHashMap.Node.collision ks vs h = Lean.PersistentHashMap.Node.collision ks_1 vs_1 ⋯
-- Init.Grind.ToIntLemmas
Lean.Grind.IntInterval.hi?.eq_3 : ∀ (hi : ℤ), (Lean.Grind.IntInterval.io hi).hi? = some hi
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.gen.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) (S : Set α) (V : Set (β × β)),
  UniformOnFun.gen 𝔖 S V = {uv | ∀ x ∈ S, ((UniformOnFun.toFun 𝔖) uv.1 x, (UniformOnFun.toFun 𝔖) uv.2 x) ∈ V}
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.of_subsingleton_dom : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {f : α → β} [inst : TopologicalSpace β] [Subsingleton α],
  MeasureTheory.StronglyMeasurable f
-- Mathlib.RingTheory.Coprime.Basic
/-- The proposition that `x` and `y` are coprime, defined to be the existence of `a` and `b` such
that `a * x + b * y = 1`. Note that elements with no common divisors are not necessarily coprime,
e.g., the multivariate polynomials `x₁` and `x₂` are not coprime.  -/
IsCoprime : {R : Type u} → [CommSemiring R] → R → R → Prop
-- Mathlib.Topology.MetricSpace.Algebra
IsBoundedSMul.dist_smul_pair' : ∀ {α : Type u_1} {β : Type u_2} {inst : PseudoMetricSpace α} {inst_1 : PseudoMetricSpace β} {inst_2 : Zero α}
  {inst_3 : Zero β} {inst_4 : SMul α β} [self : IsBoundedSMul α β] (x : α) (y₁ y₂ : β),
  dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyLT!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLT! k = t₂.getKeyLT! k