mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- **Alias** of `linearIndependent_finSucc'`. -/
linearIndependent_fin_succ' : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  {v : Fin (n + 1) → V},
  LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ Submodule.span K (Set.range (Fin.init v))
-- Mathlib.Algebra.Group.Units.Hom
Units.map_bijective : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] {f : M →* N},
  Function.Bijective ⇑f → Function.Bijective ⇑(Units.map f)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.not_revMatchesAt_revSkipWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String.Slice} (pos : s.Pos),
  ¬String.Slice.Pattern.Model.RevMatchesAt pat (pos.revSkipWhile pat)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- For `B : BoxIntegral.Box`, the set of indices of `unitPartition.box` that are subsets of `B`.
This is a finite set. These boxes cover `B` if it has integral vertices, see
`unitPartition.prepartition_isPartition`.  -/
BoxIntegral.unitPartition.admissibleIndex : {ι : Type u_1} → (n : ℕ) → [NeZero n] → [Fintype ι] → BoxIntegral.Box ι → Finset (ι → ℤ)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.Limits.HasZeroObject D] {F : CategoryTheory.Functor C D},
  CategoryTheory.Limits.IsZero F → ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)
-- Mathlib.Algebra.Quaternion
Quaternion.instCoeTC : {R : Type u_3} → [inst : CommRing R] → CoeTC R (Quaternion R)
-- Mathlib.Algebra.Group.Submonoid.Defs
ZeroMemClass.zero.eq_1 : ∀ {A : Type u_3} {M₁ : Type u_4} [inst : SetLike A M₁] [inst_1 : Zero M₁] [hA : ZeroMemClass A M₁] (S' : A),
  ZeroMemClass.zero S' = { zero := ⟨0, ⋯⟩ }
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, the images of the components of
the natural transformation `H ⟶ F` under `G` are the components of the composition of counit of the
second adjunction with the unit of the first adjunction.  -/
CategoryTheory.Adjunction.Triple.map_rightToLeft_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  (X : C), G.map (t.rightToLeft.app X) = CategoryTheory.CategoryStruct.comp (t.adj₂.counit.app X) (t.adj₁.unit.app X)
-- Mathlib.Analysis.Convex.PathConnected
Path.cast_segment : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] {a b c d : E} (hac : c = a) (hbd : d = b),
  (Path.segment a b).cast hac hbd = Path.segment c d
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.mk.inj : ∀ {Γ : Type u_1} {R : Type u_2} {inst : PartialOrder Γ} {inst_1 : Zero R} {coeff : Γ → R}
  {isPWO_support' : (Function.support coeff).IsPWO} {coeff_1 : Γ → R}
  {isPWO_support'_1 : (Function.support coeff_1).IsPWO},
  { coeff := coeff, isPWO_support' := isPWO_support' } = { coeff := coeff_1, isPWO_support' := isPWO_support'_1 } →
    coeff = coeff_1
-- Mathlib.Order.Hom.Lattice
InfHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Min β] [inst_2 : Min γ] (g : SupHom βᵒᵈ γᵒᵈ)
  (f : SupHom αᵒᵈ βᵒᵈ), InfHom.dual.symm (g.comp f) = (InfHom.dual.symm g).comp (InfHom.dual.symm f)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.AltParamInfo.mk.sizeOf_spec : ∀ (numFields numOverlaps : ℕ) (hasUnitThunk : Bool),
  sizeOf { numFields := numFields, numOverlaps := numOverlaps, hasUnitThunk := hasUnitThunk } =
    1 + sizeOf numFields + sizeOf numOverlaps + sizeOf hasUnitThunk
-- Init.Data.List.Lemmas
List.contains_flatten : ∀ {α : Type u_1} [inst : BEq α] {l : List (List α)} {x : α}, l.flatten.contains x = l.any fun l => l.contains x
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.coe_neg : ∀ {α : Type u} [inst : Neg α] (a : α), ↑(-a) = -↑a
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- The scalar multiplication on an object of `ModuleCat R` considered as
a morphism of rings from `R` to the endomorphisms of the underlying abelian group.  -/
ModuleCat.smul : {R : Type u} →
  [inst : Ring R] →
    (M : ModuleCat R) → R →+* CategoryTheory.End ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M)
-- Lean.DocString.Types
Lean.Doc.instInhabitedListItem.default : {α : Type u} → Lean.Doc.ListItem α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.ofList_singleton : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α} {v : β k},
  Std.DTreeMap.ofList [⟨k, v⟩] cmp = ∅.insert k v
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ioc_right_eq_Ioc_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a ≤ b → insert (Order.succ b) (Set.Ioc a b) = Set.Ioc a (Order.succ b)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        {D : I → Type u₂} →
          [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
            [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)] →
              (F : (i : I) → CategoryTheory.Functor (D i) (C i)) →
                [(i : I) → (F i).Monoidal] → (CategoryTheory.Functor.pi F).Monoidal
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_iff_keys_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.keys = t₂.keys)
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.cast_cast : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (γ : Path.Homotopic.Quotient x y) {x' y' : X} (hx : x' = x)
  (hy : y' = y) {x'' y'' : X} (hx' : x'' = x') (hy' : y'' = y'), (γ.cast hx hy).cast hx' hy' = γ.cast ⋯ ⋯
-- Init.Data.UInt.Lemmas
UInt32.toFin_toUInt64 : ∀ (n : UInt32), n.toUInt64.toFin = Fin.castLE UInt32.toFin_toUInt64._proof_1 n.toFin
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_inf : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S T : Subsemigroup N) (f : M →ₙ* N),
  Subsemigroup.comap f (S ⊓ T) = Subsemigroup.comap f S ⊓ Subsemigroup.comap f T
-- Mathlib.Order.Filter.CountablyGenerated
/-- We say that a filter `l` has a countable basis `s : ι → Set α` bounded by `p : ι → Prop`,
if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`, and the set
defined by `p` is countable.  -/
Filter.HasCountableBasis : {α : Type u_1} → {ι : Type u_4} → Filter α → (ι → Prop) → (ι → Set α) → Prop
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_sInter : ∀ {α : Type u_1} [inst : Preorder α] {S : Set (Set α)}, (∀ s ∈ S, s.OrdConnected) → (⋂₀ S).OrdConnected
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_iff_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {k : α}, k ∈ t ↔ t.contains k = true
-- Mathlib.Analysis.Complex.Circle
Circle.exp_natCast_mul : ∀ (x : ℝ) (n : ℕ), Circle.exp (↑n * x) = Circle.exp x ^ n
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAtFilter.neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → HasDerivAtFilter (-f) (-f') L
-- Mathlib.CategoryTheory.Shift.Basic
/-- compatibility with the left addition with 0  -/
CategoryTheory.ShiftMkCore.zero_add_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (self : CategoryTheory.ShiftMkCore C A) (n : A) (X : C),
  (self.add 0 n).hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((self.F n).map (self.zero.inv.app X))
-- Mathlib.Order.CompleteLattice.Basic
IsLUB.iSup_eq : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α}, IsLUB (Set.range f) a → ⨆ j, f j = a
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_adj' : ∀ {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph V) (u v : W),
  (SimpleGraph.map f G).Adj u v ↔ u ≠ v ∧ ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.VarSet : Type
-- Mathlib.RingTheory.Ideal.Prod
Ideal.prod_eq_top_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} {J : Ideal S},
  I.prod J = ⊤ ↔ I = ⊤ ∧ J = ⊤
-- Mathlib.Order.Interval.Finset.Defs
/-- `Finset.uIcc a b` is the set of elements lying between `a` and `b`, with `a` and `b` included.
Note that we define it more generally in a lattice as `Finset.Icc (a ⊓ b) (a ⊔ b)`. In a
product type, `Finset.uIcc` corresponds to the bounding box of the two elements.  -/
Finset.uIcc : {α : Type u_1} → [inst : Lattice α] → [LocallyFiniteOrder α] → α → α → Finset α
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
GrpCat.tensorObj_eq : ∀ (G H : GrpCat), CategoryTheory.MonoidalCategoryStruct.tensorObj G H = GrpCat.of (↑G × ↑H)
-- Init.Data.Nat.Lemmas
Nat.two_pow_pred_add_two_pow_pred : ∀ {w : ℕ}, 0 < w → 2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w
-- Mathlib.Geometry.Manifold.HasGroupoid
Structomorph.mem_groupoid : ∀ {H : Type u} [inst : TopologicalSpace H] {G : StructureGroupoid H} {M : Type u_5} {M' : Type u_6}
  [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace M'] [inst_3 : ChartedSpace H M] [inst_4 : ChartedSpace H M']
  (self : Structomorph G M M') (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
  c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (self.toOpenPartialHomeomorph.trans c') ∈ G
-- Mathlib.Order.Category.BddOrd
BddOrd.instCategory : CategoryTheory.Category.{u, u + 1} BddOrd
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_singleton_one : ∀ (R : Type uR) (A : Type uA) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], R[1] = ⊥
-- Mathlib.RingTheory.PowerSeries.Trunc
/-- Split off the first `n` coefficients.  -/
PowerSeries.eq_X_pow_mul_shift_add_trunc : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (f : PowerSeries R),
  f = (PowerSeries.X ^ n * PowerSeries.mk fun i => (PowerSeries.coeff (i + n)) f) + ↑((PowerSeries.trunc n) f)
-- Lean.Data.Lsp.Basic
Lean.Lsp.VersionedTextDocumentIdentifier.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (version? : Option ℕ),
  sizeOf { uri := uri, version? := version? } = 1 + sizeOf uri + sizeOf version?
-- Mathlib.Tactic.DepRewrite
/-- Only insert casts on proofs.

In this mode, it is *not* permitted to cast subterms of proofs that are not themselves proofs.  -/
Mathlib.Tactic.DepRewrite.CastMode.proofs : Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.mk : {M : Type u_10} →
  {N : Type u_11} →
    [inst : MulOne M] →
      [inst_1 : MulOne N] →
        (toOneHom : OneHom M N) → (∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y) → M →* N
-- Std.Do.SPred.SPred
Std.Do.SPred.conjunction_cons : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {env : List (Std.Do.SPred σs)},
  Std.Do.SPred.conjunction (P :: env) = spred(P ∧ Std.Do.SPred.conjunction env)
-- Mathlib.Data.ENNReal.Basic
ENNReal.top_ne_ofNat : ∀ {n : ℕ} [inst : n.AtLeastTwo], ⊤ ≠ OfNat.ofNat n
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.toBoundedContinuousFunctionCLM.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F],
  TestFunction.toBoundedContinuousFunctionCLM 𝕜 =
    TestFunction.mkCLM 𝕜 (fun x => { toFun := ⇑x, continuous_toFun := ⋯, map_bounded' := ⋯ }) ⋯ ⋯ ⋯
-- Mathlib.Algebra.Order.Module.Defs
monotone_smul_left_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulMono α β], 0 ≤ a → Monotone fun x => a • x
-- Mathlib.Algebra.Group.EvenFunction
/-- If `f` is even and `g` is odd, then `f ∘ g` is even.  -/
Function.Even.comp_odd : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} [inst_1 : Neg β] {f : β → γ},
  Function.Even f → ∀ {g : α → β}, Function.Odd g → Function.Even (f ∘ g)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.zero_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R), 0 * φ = 0
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.gradedMonoid_eq_of_cast : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {a b : GradedMonoid fun n => PiTensorProduct R fun x => M} (h : a.fst = b.fst),
  (TensorPower.cast R M h) a.snd = b.snd → a = b
-- Mathlib.Algebra.Algebra.Equiv
LinearEquiv.conjAlgEquiv_symm_apply_apply : ∀ (R : Type u_1) {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₁]
  [inst_7 : Module S M₂] [inst_8 : SMulCommClass S R M₁] [inst_9 : SMulCommClass S R M₂] [inst_10 : SMul R S]
  [inst_11 : IsScalarTower R S M₁] [inst_12 : IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) (f : M₂ →ₗ[S] M₂) (x : M₁),
  ((LinearEquiv.conjAlgEquiv R e).symm f) x = e.symm (f (e x))
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.instInhabited : (α : Type u_2) → [inst : TopologicalSpace α] → [inst_1 : Preorder α] → Inhabited (EsakiaHom α α)
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.resolveDottedIdentFn.go : Lean.Name →
  List Lean.Level →
    Lean.Expr →
      Lean.Expr →
        Array Lean.Exception → Lean.Elab.TermElabM (List (Lean.Expr × Lean.Syntax × List Lean.Syntax × List Lean.Level))
-- Mathlib.Algebra.Lie.SerreConstruction
_private.Mathlib.Algebra.Lie.SerreConstruction.0.CartanMatrix.Relations.termF : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
AlgebraicTopology.DoldKan.MorphComponents.preComp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X X' : CategoryTheory.SimplicialObject C} {n : ℕ}
  {Z : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z) (g : X' ⟶ X),
  f.preComp g =
    { a := CategoryTheory.CategoryStruct.comp (g.app (Opposite.op { len := n + 1 })) f.a,
      b := fun i => CategoryTheory.CategoryStruct.comp (g.app (Opposite.op { len := n })) (f.b i) }
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- The algebra isomorphism between multivariable power series in `Fin (n + 1)` and
power series over multivariable power series in `Fin n`.  -/
MvPowerSeries.finSuccEquiv : (R : Type u_2) →
  [inst : CommSemiring R] → (n : ℕ) → MvPowerSeries (Fin (n + 1)) R ≃ₐ[R] PowerSeries (MvPowerSeries (Fin n) R)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_mul_sublist : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : FreeGroup α), (x * y).toWord.Sublist (x.toWord ++ y.toWord)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation.parameters? : Lean.Lsp.SignatureInformation → Option (Array Lean.Lsp.ParameterInformation)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.map_smulₛₗ₂ : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x : E)
  (y : F), (f (c • x)) y = σ₁₃ c • (f x) y
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hurwitzZetaEven_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.hurwitzZetaEven (-a) s = HurwitzZeta.hurwitzZetaEven a s
-- Mathlib.Control.ULiftable
/-- for specific state types, this function helps to create a uliftable instance  -/
StateT.uliftable' : {s : Type u₀} →
  {s' : Type u₁} →
    {m : Type u₀ → Type v₀} →
      {m' : Type u₁ → Type v₁} → [ULiftable m m'] → s ≃ s' → ULiftable (StateT s m) (StateT s' m')
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_cons_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.getEntry k (⟨k, v⟩ :: l) ⋯ = ⟨k, v⟩
-- Init.Core
ForInStep.yield.inj : ∀ {α : Type u} {a a_1 : α}, ForInStep.yield a = ForInStep.yield a_1 → a = a_1
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a translation-invariant pseudodistance.  -/
SeminormedAddCommGroup.ofAddDist : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : AddCommGroup E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 0 x) → (∀ (x y z : E), dist x y ≤ dist (z + x) (z + y)) → SeminormedAddCommGroup E
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.symm_apply_eq : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N), e.symm n = m ↔ n = e m
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given `F : C ⥤ D ⥤ D`, `X : C`, `e : F.obj X ≅ 𝟭 D` and `Y : GradedObject J D`,
this is the isomorphism `((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a ≅ Y a.2`
when `a : I × J` is such that `a.1 = 0`.  -/
CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) →
                    (X : C) →
                      (F.obj X ≅ CategoryTheory.Functor.id D) →
                        (Y : CategoryTheory.GradedObject J D) →
                          (a : I × J) →
                            a.1 = 0 →
                              (((CategoryTheory.GradedObject.mapBifunctor F I J).obj
                                      ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
                                  Y a ≅
                                Y a.2)
-- Mathlib.Algebra.Group.Basic
mul_inv_eq_of_eq_mul : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = c * b → a * b⁻¹ = c
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_inv : ∀ {u : ℕ → EReal}, LinearGrowth.linearGrowthSup (-u) = -LinearGrowth.linearGrowthInf u
-- Mathlib.Topology.PartitionOfUnity
/-- Index of a bump function such that `f i =ᶠ[𝓝 x] 1`.  -/
BumpCovering.ind : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → BumpCovering ι X s → (x : X) → x ∈ s → ι
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsStarConvexSet.sub : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Convexity.ConvexSpace R M]
  [Convexity.IsModuleConvexSpace R M] {x y : M} {s t : Set M},
  Convexity.IsStarConvexSet R x s → Convexity.IsStarConvexSet R y t → Convexity.IsStarConvexSet R (x - y) (s - t)
-- Mathlib.SetTheory.Lists
/-- Sends `a : α` to the corresponding atom in `Lists α`.  -/
Lists.atom : {α : Type u_1} → α → Lists α
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
/-- The forget functor `AddGrpCat.{u} ⥤ Type u` is corepresentable.  -/
AddGrpCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (AddGrpCat.of (ULift.{u, 0} ℤ))) ≅ CategoryTheory.forget AddGrpCat
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.emptyWithCapacity : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → ℕ → aig.RefVec 0
-- Mathlib.Data.NNReal.Defs
NNReal.le_of_forall_lt_one_mul_le : ∀ {x y : NNReal}, (∀ a < 1, a * x ≤ y) → x ≤ y
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofRealLI_apply : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.ofRealLI = RCLike.ofReal
-- Aesop.Builder.Constructors
Aesop.RuleBuilderOptions.constructorsIndexTransparency : Aesop.RuleBuilderOptions → Lean.Meta.TransparencyMode
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.mem_quasiIso_iff : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : CategoryTheory.CategoryWithHomology C] (f : K ⟶ L), HomologicalComplex.quasiIso C c f ↔ QuasiIso f
-- Mathlib.MeasureTheory.Covering.OneDim
Real.Icc_mem_vitaliFamily_at_left : ∀ {x y : ℝ}, x < y → Set.Icc x y ∈ (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).setsAt y
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.linearMapPi_symm_apply : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)] (S : Type u_1)
  [inst_5 : Semiring S] [inst_6 : (i : ι) → Module S (φ i)] [inst_7 : ∀ (i : ι), SMulCommClass R S (φ i)]
  (f : M₂ →ₗ[R] (i : ι) → φ i) (i : ι), (LinearEquiv.linearMapPi S).symm f i = LinearMap.proj i ∘ₗ f
-- Lean.ResolveName
/-- Given a name `n`, returns a list of possible interpretations for global constants.

Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty.
For identifiers taken from syntax, use `resolveGlobalConst` instead, which respects preresolved names.  -/
_private.Lean.ResolveName.0.Lean.resolveGlobalConstCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadError m] → Lean.Name → m (List Lean.Name)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.symm_mk_mul : ∀ {M : Type u_1} [inst : Mul M] (a b : Mᵈᵐᵃ), DomMulAct.mk.symm (a * b) = DomMulAct.mk.symm b * DomMulAct.mk.symm a
-- Init.Data.Random
/-- Auxiliary function for randomNatVal.
Generate random values until we exceed the target magnitude.
`genLo` and `genMag` are the generator lower bound and magnitude.
The parameter `r` is the "remaining" magnitude.
 -/
_private.Init.Data.Random.0.randNatAux : {gen : Type u} → [RandomGen gen] → ℕ → ℕ → ℕ → ℕ × gen → ℕ × gen
-- Mathlib.Algebra.Order.Floor.Semifield
Nat.floor_div_natCast : ∀ {K : Type u_2} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorSemiring K]
  (a : K) (n : ℕ), ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
-- Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
SymmetricAlgebra.counitAlgHom_eq : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Bialgebra.counitAlgHom R (SymmetricAlgebra R M) = SymmetricAlgebra.algebraMapInv
-- Mathlib.Data.List.MinMax
List.getElem_le_maximum_of_length_pos : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {i : ℕ} (w : i < l.length) (h : optParam (0 < l.length) ⋯),
  l[i] ≤ List.maximum_of_length_pos h