mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Lemmas
ISize.ofNat_lt_iff_lt : ∀ {a b : ℕ},
  a < 2 ^ (System.Platform.numBits - 1) →
    b < 2 ^ (System.Platform.numBits - 1) → (ISize.ofNat a < ISize.ofNat b ↔ a < b)
-- Init.Data.List.Lemmas
List.getLast?_append : ∀ {α : Type u_1} {l l' : List α}, (l ++ l').getLast? = l'.getLast?.or l.getLast?
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instContinuousConstSMul : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] {M : Type u_5} [inst_8 : Monoid M] [inst_9 : DistribMulAction M F]
  [inst_10 : SMulCommClass 𝕜 M F] [inst_11 : ContinuousConstSMul M F],
  ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.Data.Sym.Sym2
Sym2.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} (x : Sym2 α),
  Sym2.map g (Sym2.map f x) = Sym2.map (g ∘ f) x
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.toSucc_injectivity : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C]
  [inst_4 : CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  {X Y : C} (f : X ⟶ Y),
  W f →
    ∀ (g₁ g₂ : Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂ →
        CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.OrthogonalReflection.toSucc W Z) =
          CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.OrthogonalReflection.toSucc W Z)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.HasBasis.uniformity_of_nhds_one_swapped : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Sort u_3} {p : ι → Prop}
  {U : ι → Set α}, (nhds 1).HasBasis p U → (uniformity α).HasBasis p fun i => {x | x.1 / x.2 ∈ U i}
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.isSymm_toBilin'_iff_isSymm : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M : Matrix n n R₁}, (Matrix.toBilin' M).IsSymm ↔ M.IsSymm
-- Init.System.IO
/-- Returns the current working directory of the calling process.  -/
IO.Process.getCurrentDir : IO System.FilePath
-- Mathlib.Analysis.Asymptotics.LinearGrowth
/-- See `linearGrowthInf_add_le'` for a version with swapped argument `u` and `v`.  -/
LinearGrowth.linearGrowthInf_add_le : ∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthSup u ≠ ⊥ ∨ LinearGrowth.linearGrowthInf v ≠ ⊤ →
    LinearGrowth.linearGrowthSup u ≠ ⊤ ∨ LinearGrowth.linearGrowthInf v ≠ ⊥ →
      LinearGrowth.linearGrowthInf (u + v) ≤ LinearGrowth.linearGrowthSup u + LinearGrowth.linearGrowthInf v
-- Mathlib.RingTheory.Noetherian.Basic
LinearMap.isNoetherian_iff_of_bijective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_3}
  {P : Type u_4} [inst_3 : Semiring S] [inst_4 : AddCommMonoid P] [inst_5 : Module S P] {σ : R →+* S}
  [RingHomSurjective σ] (l : M →ₛₗ[σ] P), Function.Bijective ⇑l → (IsNoetherian R M ↔ IsNoetherian S P)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_neg : ∀ {a : ISize} (h : System.Platform.numBits = 64), (-a).toBitVec64 h = -a.toBitVec64 h
-- Init.Data.SInt.Bitwise
Int16.and_comm : ∀ (a b : Int16), a &&& b = b &&& a
-- Mathlib.Tactic.ITauto
/-- `(p: A → B) (q: A) ⊢ B`  -/
Mathlib.Tactic.ITauto.Proof.app' : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Data.List.AList
AList.union_comm_of_disjoint : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ : AList β},
  s₁.Disjoint s₂ → (s₁ ∪ s₂).entries.Perm (s₂ ∪ s₁).entries
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.induction_on : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) {C : AdjoinRoot f → Prop} (x : AdjoinRoot f),
  (∀ (p : Polynomial R), C ((AdjoinRoot.mk f) p)) → C x
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.coe_of : ∀ (R : Type u) [inst : CommMonoid R], ↑(CommMonCat.of R) = R
-- Init.Data.BitVec.Basic
/-- Extracts the bits `start` to `start + len - 1` from a bitvector of size `n` to yield a
new bitvector of size `len`. If `start + len > n`, then the bitvector is zero-extended.
 -/
BitVec.extractLsb' : {n : ℕ} → ℕ → (len : ℕ) → BitVec n → BitVec len
-- Init.Data.SInt.Lemmas
Int64.add_right_inj : ∀ {a b : Int64} (c : Int64), c + a = c + b ↔ a = b
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintTextEdit : Type
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
RCLike.measurable_re : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], Measurable ⇑RCLike.re
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
/-- **Alias** of `ENNReal.rpow_eq_exp_mul_log`. -/
EReal.ENNReal.rpow_eq_exp_mul_log : ∀ (x : ENNReal) (y : ℝ), x ^ y = (↑y * x.log).exp
-- Mathlib.CategoryTheory.Pi.Monoidal
/-- Equips the product of a family of closed monoidal categories with
a pointwise closed monoidal structure.  -/
CategoryTheory.Pi.monoidalClosed : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [(i : I) → CategoryTheory.MonoidalClosed (C i)] → CategoryTheory.MonoidalClosed ((i : I) → C i)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIco.eq_1 : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜], AddCircle.equivIco p a = QuotientAddGroup.equivIcoMod ⋯ a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = none ↔ k ∉ t
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to a `UInt16`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toUInt16 : Float.Model.UnpackedFloat → UInt16
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] [inst_4 : F.HasRightDerivedFunctor W],
  (F.totalRightDerived L W).IsRightDerivedFunctor (F.totalRightDerivedUnit L W) W
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₃ : Type u_16}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid N₃] [inst_7 : Module R M₁]
  [inst_8 : Module R M₂] [inst_9 : Module R M₃] [inst_10 : Module R N₃] (f₃ : M₃ →ₗ[R] N₃)
  (f₁₂ : M →ₗ[R] TensorProduct R M₁ M₂),
  ↑(TensorProduct.assoc R M₁ M₂ N₃) ∘ₗ TensorProduct.map f₁₂ f₃ =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f₃) ∘ₗ
      ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ TensorProduct.map f₁₂ LinearMap.id
-- Std.Http.Data.Status
Std.Http.Status.locked.sizeOf_spec : sizeOf Std.Http.Status.locked = 1
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C),
  (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.inv.app X).f = AlgebraicTopology.DoldKan.PInfty
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_add : ∀ (a b : BitVec 16), Int16.ofBitVec (a + b) = Int16.ofBitVec a + Int16.ofBitVec b
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_le_inj : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₁ a₂ : α} {g : κ → α} (e : ι → κ),
  Function.Injective e →
    (∀ c ∉ Set.range e, 1 ≤ g c) → (∀ (i : ι), f i ≤ g (e i)) → HasProd f a₁ → HasProd g a₂ → a₁ ≤ a₂
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.leftUnitor_inv_apply : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv) m = 1 ⊗ₜ[R] m
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.mk.inj : ∀ {x : Lean.Grind.CommRing.Var} {k : ℕ} {x_1 : Lean.Grind.CommRing.Var} {k_1 : ℕ},
  { x := x, k := k } = { x := x_1, k := k_1 } → x = x_1 ∧ k = k_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α} {f : β → β}, (t.modify k f).contains k' = t.contains k'
-- Mathlib.Order.Notation
bot_nonempty : ∀ (α : Type u_1) [Bot α], Nonempty α
-- Mathlib.Topology.Compactness.Compact
/-- A filter is disjoint from the cocompact filter if and only if it contains a compact set.  -/
Filter.disjoint_cocompact_right : ∀ {X : Type u} [inst : TopologicalSpace X] (f : Filter X), Disjoint f (Filter.cocompact X) ↔ ∃ K ∈ f, IsCompact K
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last.sizeOf_spec : ∀ (hs : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof)) (decVars : Array Lean.FVarId),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last hs decVars) = 1 + sizeOf hs + sizeOf decVars
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε₂_def : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [inst_1 : c.TensorSigns] (x : I × I),
  TotalComplexShape.ε₂ c c c x =
    match x with
    | (p, snd) => c.ε p
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember : Type
-- Mathlib.Tactic.NormNum.Eq
Mathlib.Meta.NormNum.NNRat.invOf_denom_swap : ∀ {α : Type u_1} [inst : Semiring α] (n₁ n₂ : ℕ) (a₁ a₂ : α) [inst_1 : Invertible a₁] [inst_2 : Invertible a₂],
  ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.biproductComparison_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] (j : J),
  CategoryTheory.CategoryStruct.comp (F.biproductComparison f) (CategoryTheory.Limits.biproduct.π (F.obj ∘ f) j) =
    F.map (CategoryTheory.Limits.biproduct.π f j)
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- A CW complex is finite if it is finite dimensional and of finite type.  -/
Topology.RelCWComplex.Finite : {X : Type u_1} → [inst : TopologicalSpace X] → (C : Set X) → {D : Set X} → [Topology.RelCWComplex C D] → Prop
-- Mathlib.Order.OrderIsoNat
RelEmbedding.not_wellFounded : ∀ {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r] (f : (fun x1 x2 => x1 > x2) ↪r r), ¬WellFounded r
-- Mathlib.Algebra.Category.BoolRing
/-- Constructs an isomorphism of Boolean rings from a ring isomorphism between them.  -/
BoolRing.Iso.mk : {α β : BoolRing} → ↑α ≃+* ↑β → (α ≅ β)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.brecOn_1.eq : ∀ {motive_1 : Aesop.Frontend.RuleExpr → Sort u} {motive_2 : Array Aesop.Frontend.RuleExpr → Sort u}
  {motive_3 : List Aesop.Frontend.RuleExpr → Sort u} (t : Array Aesop.Frontend.RuleExpr)
  (F_1 : (t : Aesop.Frontend.RuleExpr) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_2 t → motive_3 t),
  Aesop.Frontend.RuleExpr.brecOn_1 t F_1 F_2 F_3 = F_2 t (Aesop.Frontend.RuleExpr.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
UniformCauchySeqOn.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn f' l s → UniformCauchySeqOn (f * f') l s
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
/-- We don't want to keep carrying the `StructId` around.  -/
Lean.Meta.Grind.Arith.Linear.LinearM : Type → Type
-- Mathlib.ModelTheory.Definability
Set.empty_definable_iff : ∀ {M : Type w} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {s : Set (α → M)},
  ∅.Definable L s ↔ ∃ φ, s = Set.ofPred φ.Realize
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withBotCongr_refl : ∀ {α : Type u_1} [inst : PartialOrder α], (OrderIso.refl α).withBotCongr = OrderIso.refl (WithBot α)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_dvd_of_le_left : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (L : Subgroup G), H ≤ K → K.relIndex L ∣ H.relIndex L
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.mk : {α β σ : Type} →
  autoParam Lean.Name Lean.PersistentEnvExtensionDescrCore.name._autoParam →
    IO σ →
      (Array (Array α) → Lean.ImportM σ) →
        (σ → β → σ) →
          (Lean.Environment → σ → Lean.OLeanEntries (Array α)) →
            (σ → Std.Format) →
              Lean.EnvExtension.AsyncMode → Option (Lean.ReplayFn σ) → Lean.PersistentEnvExtensionDescrCore α β σ
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.hasFDerivAtFilter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {L : Filter (E × E)},
  HasFDerivAt f f' x → L ≤ nhds x ×ˢ pure x → HasFDerivAtFilter f f' L
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.Nonsingular.of_iso : ∀ {X Y : SSet} (e : X ≅ Y) [X.Nonsingular], Y.Nonsingular
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.bialgebra : {R : Type u} → [inst : CommRing R] → (self : CommBialgCat R) → Bialgebra R ↑self
-- Lean.CoreM
Lean.Core.SavedState.mk.sizeOf_spec : ∀ (toState : Lean.Core.State) (passedHeartbeats : ℕ),
  sizeOf { toState := toState, passedHeartbeats := passedHeartbeats } = 1 + sizeOf toState + sizeOf passedHeartbeats
-- Mathlib.Order.Directed
Std.Total.to_isDirected : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Total r], IsDirected α r
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_interSmaller : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  (m₁ m₂ : Std.DTreeMap.Internal.Impl α β),
  m₁.WF → (m₁.interSmaller m₂).toListModel.Perm (Std.Internal.List.interSmaller m₁.toListModel m₂.toListModel)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.whiskerRight_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ : CategoryTheory.Center C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Center C) (U : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.f Y.fst)
        U)
      ((X₂.tensorObj Y).snd.β U).hom =
    CategoryTheory.CategoryStruct.comp ((X₁.tensorObj Y).snd.β U).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.f Y.fst))
-- Mathlib.RingTheory.Valuation.DiscreteValuativeRel
ValuativeRel.nonempty_orderIso_withZeroMul_int_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R],
  Nonempty (ValuativeRel.ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔
    ValuativeRel.IsDiscrete R ∧ ValuativeRel.IsNontrivial R ∧ MulArchimedean (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.hasCoeAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → CoeTC (OpenAddSubgroup G) (AddSubgroup G)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C},
  (∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P.isoClosure T.obj₂) →
    P.IsTriangulatedClosed₂
-- Mathlib.Algebra.Ring.Subring.Basic
RingEquiv.restrict_symm_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2}
  [inst_2 : SetLike σR R] [inst_3 : SetLike σS S] [inst_4 : SubsemiringClass σR R] [inst_5 : SubsemiringClass σS S]
  (e : R ≃+* S) (s' : σR) (s : σS) (h : ∀ (x : R), x ∈ s' ↔ e x ∈ s) (a : ↥s), ↑((e.restrict s' s h).symm a) = e.symm ↑a
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toTopologicalSpace_top : ∀ {α : Type u} [inst : Group α], ⊤.toTopologicalSpace = ⊤
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_iff_integrableOn_Icc_of_le : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  a ≤ b →
    autoParam (‖f a‖ₑ ≠ ⊤) intervalIntegrable_iff_integrableOn_Icc_of_le._auto_1 →
      (IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Icc a b) μ)
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.mk.injEq : ∀ {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₂]
  (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⁆) (toLieHom_1 : L₁ →ₗ⁅R⁆ L₂)
  (map_smul_apply'_1 : ∀ (a : A₁) (x : L₁), toLieHom_1 (a • x) = σ a • toLieHom_1 x)
  (apply_lie'_1 : ∀ (a : A₁) (x : L₁), σ ⁅x, a⁆ = ⁅toLieHom_1 x, σ a⁆),
  ({ toLieHom := toLieHom, map_smul_apply' := map_smul_apply', apply_lie' := apply_lie' } =
      { toLieHom := toLieHom_1, map_smul_apply' := map_smul_apply'_1, apply_lie' := apply_lie'_1 }) =
    (toLieHom = toLieHom_1)
-- Mathlib.Algebra.Ring.Pi
Pi.evalNonUnitalRingHom_apply : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → NonUnitalNonAssocSemiring (f i)] (i : I) (g : (i : I) → f i),
  (Pi.evalNonUnitalRingHom f i) g = g i
-- Mathlib.LinearAlgebra.Trace
dualTensorHomEquivOfBasis.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (b b_1 : Module.Basis ι R M),
  b = b_1 →
    ∀ {inst_5 : DecidableEq ι} [inst_6 : DecidableEq ι] [inst_7 : Fintype ι],
      dualTensorHomEquivOfBasis b = dualTensorHomEquivOfBasis b_1
-- Mathlib.Data.List.Basic
List.getElem_set_of_ne : ∀ {α : Type u} {l : List α} {i j : ℕ}, i ≠ j → ∀ (a : α) (hj : j < (l.set i a).length), (l.set i a)[j] = l[j]
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Because we use binary encoding, we define `trNat` in terms of `trNum`, using `Num`, which are
binary natural numbers. (We could also use `Nat.binaryRecOn`, but `Num` and `PosNum` make for
easy inductions.)  -/
Turing.PartrecToTM2.trNat : ℕ → List Turing.PartrecToTM2.Γ'
-- Mathlib.Topology.Semicontinuity.Basic
/-- An upper semicontinuous function attains its upper bound on a nonempty compact set.  -/
UpperSemicontinuousOn.exists_isMaxOn : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} [inst_1 : LinearOrder β] {f : α → β} {s : Set α},
  s.Nonempty → IsCompact s → UpperSemicontinuousOn f s → ∃ a ∈ s, IsMaxOn f s a
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.measurableSet_spanningSets : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (i : ℕ),
  MeasurableSet (MeasureTheory.spanningSets μ i)
-- Mathlib.Algebra.Module.Defs
neg_smul_neg : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R) (x : M),
  -r • -x = r • x
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.coeff_mapDomainLinearEquiv : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e : M ≃ N) (x : MonoidAlgebra S M),
  ((MonoidAlgebra.mapDomainLinearEquiv R S e) x).coeff = Finsupp.equivMapDomain e x.coeff
-- Mathlib.Analysis.Complex.Trigonometric
/-- The complex hyperbolic tangent function, defined as `sinh z / cosh z`  -/
Complex.tanh : ℂ → ℂ
-- Mathlib.Algebra.Group.Units.Equiv
Units.mulLeft.eq_1 : ∀ {M : Type u_3} [inst : Monoid M] (u : Mˣ),
  u.mulLeft = { toFun := fun x => ↑u * x, invFun := fun x => ↑u⁻¹ * x, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.comp_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y Z : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is continuously differentiable up to `n` if it admits derivatives up to
order `n`, which are continuous. Contrary to the case of definitions in domains (where derivatives
might not be unique) we do not need to localize the definition in space or time.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`.

For `n = ω`, we require the function to be analytic. The precise
definition we give (all the derivatives should be analytic) is more involved to work around issues
when the space is not complete, but it is equivalent when the space is complete.
 -/
ContDiff : (𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          {F : Type uF} → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → WithTop ℕ∞ → (E → F) → Prop
-- Init.Data.String.Lemmas.FindPos
String.Slice.lt_offset_posGT : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p < s.rawEndPos}, p < (s.posGT p h).offset
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.Return.result : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} → Std.Tactic.BVDecide.Return aig → aig.ExtendingEntrypoint
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_singleton : ∀ {α : Type u_2} [inst : Mul α] {s : Set α} {b : α}, s * {b} = (fun x => x * b) '' s