mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.BitVec.Lemmas
/-- The absolute value of `x : BitVec w` is naively a case split on the sign of `x`.
However, recall that when `x = intMin w`, `-x = x`.
Thus, the full value of `abs x` is computed by the case split:
- If `x : BitVec w` is `intMin`, then its absolute value is also `intMin w`, and
  thus `toInt` will equal `intMin.toInt`.
- Otherwise, if `x` is negative, then `x.abs.toInt = (-x).toInt`.
- If `x` is positive, then it is equal to `x.abs.toInt = x.toInt`.
 -/
BitVec.toInt_abs_eq_ite : ∀ {w : ℕ} {x : BitVec w},
  x.abs.toInt = if x = BitVec.intMin w then (BitVec.intMin w).toInt else if x.msb = true then -x.toInt else x.toInt
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.ext_threefold' : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P : Type u_9} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid P] [inst_5 : AddCommMonoid P₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ P₂] [inst_9 : Module R P] {g h : TensorProduct R M (TensorProduct R N P) →ₛₗ[σ₁₂] P₂},
  (∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] (y ⊗ₜ[R] z)) = h (x ⊗ₜ[R] (y ⊗ₜ[R] z))) → g = h
-- Init.Data.Range.Polymorphic.UInt
UInt16.succ?_ofBitVec : ∀ {x : BitVec 16}, Std.PRange.succ? { toBitVec := x } = UInt16.ofBitVec <$> Std.PRange.succ? x
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} {s₁ e₁ : s.Pos}
  {s₂ e₂ : t.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat s₁ e₁ →
    ∀ (h₁ : s.copy = t.copy), s₁.cast h₁ = s₂ → e₁.cast h₁ = e₂ → String.Slice.Pattern.Model.IsLongestMatchAt pat s₂ e₂
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.pow_apply_mem_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {n : ℕ} {x : α},
  (f ^ n) x ∈ f.support ↔ x ∈ f.support
-- Mathlib.Data.Int.Bitwise
/-- `m >>> n` produces an integer whose binary representation
is obtained by right-shifting the binary representation of `m` by `n` places  -/
Int.instShiftRight_mathlib : ShiftRight ℤ
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [inst_4 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_5 :
    ∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_6 :
    ∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂))
      (CategoryTheory.Functor.LaxMonoidal.μ Φ.presheafFiber G₁ G₂) =
    Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂)
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Ico_intCast : ∀ (α : Type u_1) [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α],
  ⋃ n, Set.Ico (↑n) (↑n + 1) = Set.univ
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {c : NNReal} {f : ↥(MeasureTheory.Lp E p μ)}
  {g : ↥(MeasureTheory.Lp F p μ)}, (∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊) → ‖f‖₊ ≤ c * ‖g‖₊
-- Std.Data.HashMap.Basic
/-- The notation `m[a]?` is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
 -/
Std.HashMap.get? : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Option β
-- Lean.Util.SCC
Lean.SCC.Data.onStack : Lean.SCC.Data → Bool
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instLawfulMonad : LawfulMonad FreeAddGroup
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.cellFrontier_one_eq`. -/
Topology.CWComplex.cellFrontier_one_eq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (e : Topology.RelCWComplex.cell C 1),
  Topology.RelCWComplex.cellFrontier 1 e = ↑(Topology.RelCWComplex.map 1 e) '' {-1, 1}
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- Linear disjointness is symmetric if elements in the module commute.  -/
Submodule.LinearDisjoint.symm_of_commute : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → (∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n) → N.LinearDisjoint M
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.ext_iff : ∀ {X Y : FinBddDistLat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X.toDistLat), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Data.Int.Bitwise
Int.lnot_bit : ∀ (b : Bool) (n : ℤ), (Int.bit b n).lnot = Int.bit (!b) n.lnot
-- Mathlib.CategoryTheory.Monad.Coequalizer
/-- The cofork constructed is a colimit. This shows that any algebra is a (reflexive) coequalizer of
free algebras.
 -/
CategoryTheory.Monad.beckAlgebraCoequalizer : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      (X : T.Algebra) → CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.beckAlgebraCofork X)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_lt_aleph0 : ∀ {α : Type u} [Finite α], Cardinal.mk α < Cardinal.aleph0
-- Mathlib.FieldTheory.Minpoly.Finite
minpoly.natDegree_le : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] [Module.Finite A B] (x : B)
  [Module.Free A B], (minpoly A x).natDegree ≤ Module.finrank A B
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.findAux.eq_def : ∀ (s : String) (p : Char → Bool) (stopPos pos : String.Pos.Raw),
  String.Legacy.findAux s p stopPos pos =
    if h : pos < stopPos then
      if p (String.Pos.Raw.get s pos) = true then pos
      else
        have this := ⋯;
        String.Legacy.findAux s p stopPos (String.Pos.Raw.next s pos)
    else pos
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_lt_sinh : ∀ {x y : ℝ}, Real.sinh x < Real.sinh y ↔ x < y
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isSupported_iff_of_quasiIso : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : ∀ (i : ι'), K.HasHomology i]
  [inst_3 : ∀ (i : ι'), L.HasHomology i] [QuasiIso φ], K.IsSupported e ↔ L.IsSupported e
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_right_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x) {y : N}, y ∈ hf.localInverse.source → f (↑hf.localInverse.toPartialEquiv y) = y
-- Mathlib.Tactic.FBinop
/-- An `fbinop%` node.
`ref` is the original syntax that expanded into `binop%`.
`f` is the constant for the binary operator  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.binop : Lean.Syntax → Lean.Expr → FBinopElab.Tree✝ → FBinopElab.Tree✝ → FBinopElab.Tree✝
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.coe_support : ∀ {G : Type u_1} [inst : AddGroup G] (M : AddSubmonoid G), ↑M.support = ↑M ∩ -↑M
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.coeff_eq_sum : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F},
  Set.InjOn v ↑s →
    ∀ {P : Polynomial F},
      P.degree < ↑s.card → P.coeff (s.card - 1) = ∑ i ∈ s, Polynomial.eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- The length of the support of a Hamiltonian path equals the number of vertices of the graph.  -/
SimpleGraph.Walk.IsHamiltonian.length_support : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [inst_1 : Fintype α],
  p.IsHamiltonian → p.support.length = Fintype.card α
-- Init.Data.Dyadic.Basic
Dyadic.neg_zero : -0 = 0
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Join.Basic
/-- A pair of functors ((C ⥤ E), (D ⥤ E')) induces a functor `C ⋆ D ⥤ E ⋆ E'`.  -/
CategoryTheory.Join.mapPair : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                CategoryTheory.Functor C E →
                  CategoryTheory.Functor D E' →
                    CategoryTheory.Functor (CategoryTheory.Join C D) (CategoryTheory.Join E E')
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.s_as_blocks : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R],
  LieAlgebra.Orthogonal.S l R = Matrix.fromBlocks 1 0 0 (-1)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_coeff_isHomogeneous : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) (i j : ℕ),
  i + j = Module.finrank R M → ∀ [Nontrivial R], ((φ.polyCharpoly b).coeff i).IsHomogeneous j
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- `LinearMap.single` as an isometry.  -/
QuadraticMap.Isometry.single : {ι : Type u_1} →
  {R : Type u_2} →
    {P : Type u_7} →
      {Mᵢ : ι → Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] →
            [inst_2 : AddCommMonoid P] →
              [inst_3 : (i : ι) → Module R (Mᵢ i)] →
                [inst_4 : Module R P] →
                  [inst_5 : Fintype ι] →
                    [DecidableEq ι] → (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) → (i : ι) → Q i →qᵢ QuadraticMap.pi Q
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The largest ideal sheaf contained in a family of ideals.  -/
AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals : {X : AlgebraicGeometry.Scheme} → ((U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) → X.IdealSheafData
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.getSelector : Lean.MetaM (Option Lean.LibrarySuggestions.Selector)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Occasionally useful for rewriting in the backwards direction.  -/
CategoryTheory.MorphismProperty.Arrow.forget_comp_leftFunc_map : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q W : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W} (f : A ⟶ B),
  ((CategoryTheory.MorphismProperty.Arrow.forget P Q W).comp CategoryTheory.Arrow.leftFunc).map f = f.left
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
reduceDIte : Lean.Meta.Simp.Simproc
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under addition.  -/
Dioph.add_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v + g v
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.State.toOmit : Lean.Elab.ConfigEval.State✝ → Array (Lean.Ident × Lean.Name)
-- Mathlib.Logic.Basic
BEx.imp_left : ∀ {α : Sort u_1} {r p q : α → Prop}, (∀ (x : α), p x → q x) → (∃ x, ∃ (_ : p x), r x) → ∃ x, ∃ (_ : q x), r x
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.agree'_refl : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} (x : F.M), PFunctor.M.Agree' n x x
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.mem_nonZeroDivisors_of_trailingCoeff : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R},
  p.trailingCoeff ∈ nonZeroDivisors R → p ∈ nonZeroDivisors (Polynomial R)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- `AddSubmonoidWithOneClass S R` says `S` is a type of subsets `s ≤ R` that contain `0`, `1`,
and are closed under `(+)`  -/
AddSubmonoidWithOneClass : (S : Type u_1) → (R : outParam (Type u_2)) → [AddMonoidWithOne R] → [SetLike S R] → Prop
-- Mathlib.Data.Complex.Basic
Complex.conj_I : (starRingEnd ℂ) Complex.I = -Complex.I
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.continuous_mulExpNegMulSq : ∀ {ε : ℝ}, Continuous fun x => ε.mulExpNegMulSq x
-- Lean.ExtraModUses
Lean.instReprExtraModUse.repr : Lean.ExtraModUse → ℕ → Std.Format
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.Hom.toOrderHom.eq_1 : ∀ {a b : SimplexCategory} (f : a.Hom b), f.toOrderHom = f
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
MulOpposite.op_list_prod : ∀ {M : Type u_4} [inst : Monoid M] (l : List M), MulOpposite.op l.prod = (List.map MulOpposite.op l).reverse.prod
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_toAddSubgroup' : ∀ {A : Type u_2} [inst : AddGroup A] (S : Subgroup (Multiplicative A)) (a : A),
  a ∈ Subgroup.toAddSubgroup' S ↔ Multiplicative.ofAdd a ∈ S
-- Mathlib.Data.Set.PowersetCard
/-- The bijection between the product of `(n : ℕ)` and the finsets of `α` of cardinality `n` and
`Finset α`.  -/
Set.powersetCard.prodEquiv : {α : Type u_1} → (n : ℕ) × ↑(Set.powersetCard α n) ≃ Finset α
-- Mathlib.NumberTheory.Height.NumberField
NumberField.finite_setOfPred_prod_infinitePlace_iSup_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {n : ℕ},
  n ≠ 0 → ∀ (B : ℝ), {x | ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B}.Finite
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The actual `NonUnitalSubalgebra` obtained from an element of a type satisfying
`NonUnitalSubsemiringClass` and `SMulMemClass`.  -/
NonUnitalSubalgebra.ofClass : {S : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [inst_3 : SetLike S A] →
              [NonUnitalSubsemiringClass S A] → [SMulMemClass S R A] → S → NonUnitalSubalgebra R A
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (s : Set R),
  Int.fract ⁻¹' s = ⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Set.Ico 0 1)
-- Mathlib.Topology.Order.IntermediateValue
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `x ∈ s ∩ [a, b)` the set `s` includes some open
neighborhood of `x` within `(x, +∞)`, then `[a, b] ⊆ s`.  -/
IsClosed.Icc_subset_of_forall_mem_nhdsWithin : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} {s : Set α},
  IsClosed (s ∩ Set.Icc a b) → a ∈ s → (∀ x ∈ s ∩ Set.Ico a b, s ∈ nhdsWithin x (Set.Ioi x)) → Set.Icc a b ⊆ s
-- Mathlib.Topology.Algebra.Group.Basic
continuousInv_inf : ∀ {G : Type w} [inst : Inv G] {t₁ t₂ : TopologicalSpace G}, ContinuousInv G → ContinuousInv G → ContinuousInv G
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.commMonoidObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommMonCat) → (j : J) → CommMonoid ((F.comp (CategoryTheory.forget CommMonCat)).obj j)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- `rpow` version of `Finset.prod_pow` for `ℝ≥0`.  -/
NNReal.finsetProd_rpow : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ), ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.isIso_pi_iff : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  (f : X ⟶ Y), CategoryTheory.IsIso f ↔ ∀ (i : I), CategoryTheory.IsIso (f i)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.uvarPrefix : Lean.Name
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An AddSubgroup `H` is normal if whenever `n ∈ H`, then `g + n - g ∈ H` for every `g : A` 

[Wikidata Q743179](https://www.wikidata.org/wiki/Q743179) -/
AddSubgroup.Normal : {A : Type u_2} → [inst : AddGroup A] → AddSubgroup A → Prop
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_containsThenInsert : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.containsThenInsert k v t htb).2.impl.toListModel.Perm
      (Std.Internal.List.insertEntry k v t.toListModel)
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  {ι : Type u_1} (b : ι → ↥B), ((Subalgebra.toSubmodule A).mulRightMap b).ker = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)
-- Mathlib.ModelTheory.Definability
/-- A function from a structure to itself is term-definable over a set `A` when the
value of the function is given by a term with constants `A`. Like `TermDefinable`
but specialized for unary functions in order to write `M → M` instead of `(Unit → M) → M`.  -/
Set.TermDefinable₁ : {M : Type w} → {A : Set M} → (L : FirstOrder.Language) → [L.Structure M] → (M → M) → Prop
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.strongHomClassEmpty : ∀ {M : Type w} {N : Type w'} [inst : FirstOrder.Language.empty.Structure M]
  [inst_1 : FirstOrder.Language.empty.Structure N] {F : Type u_3} [inst_2 : FunLike F M N],
  FirstOrder.Language.empty.StrongHomClass F M N
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdxD_eq_getD_keyAtIdx? : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {i : ℕ} {fallback : α},
  t.keyAtIdxD i fallback = (t.keyAtIdx? i).getD fallback
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, (t.erase k).get? k = none
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `IsLinearOrder` instance if available  -/
Lean.Meta.Grind.Arith.Linear.Struct.isLinearInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If a function `f` has a finite power series `p` around `x`, then the function
`z ↦ f (z - y)` has the same finite power series around `x + y`.  -/
HasFiniteFPowerSeriesOnBall.comp_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → ∀ (y : E), HasFiniteFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) n r
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_hom_comp_d_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ : ι}
  (h : p₁ = p₂) (p₃ : ι) {Z : V} (h_1 : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (CategoryTheory.CategoryStruct.comp (K.d p₂ p₃) h_1) =
    CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h_1
-- Init.Data.Vector.Lemmas
Vector.getElem_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {size : xs.size = n} {i : ℕ} (h : i < n), (Vector.mk xs size)[i] = xs[i]
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice : ∀ {pat : String} {s : String.Slice},
  String.Slice.Pattern.ForwardPattern.skipPrefix? pat s = String.Slice.Pattern.ForwardPattern.skipPrefix? pat.toSlice s
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_eq_zeroLocus_compl : ∀ {R : Type u} [inst : CommSemiring R] (r : R), ↑(PrimeSpectrum.basicOpen r) = (PrimeSpectrum.zeroLocus {r})ᶜ
-- Mathlib.Data.Set.Countable
Set.countable_iUnion : ∀ {α : Type u} {ι : Sort x} {t : ι → Set α} [Countable ι], (∀ (i : ι), (t i).Countable) → (⋃ i, t i).Countable
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- Negation of morphisms in a `NonPreadditiveAbelian` category.  -/
CategoryTheory.NonPreadditiveAbelian.hasNeg : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.NonPreadditiveAbelian C] → {X Y : C} → Neg (X ⟶ Y)
-- Mathlib.Order.Bounds.Defs
/-- A set is bounded below if there exists a lower bound.  -/
BddBelow : {α : Type u_1} → [LE α] → Set α → Prop
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_self`. -/
LinearOrderedField.inducedOrderRingIso_self : ∀ (β : Type u_3) [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β] [inst_2 : IsStrictOrderedRing β],
  ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β β = OrderRingIso.refl β
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instSMulPosReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : AddCommGroup β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : DistribMulAction α β] [SMulPosReflectLT α β],
  SMulPosReflectLT α βᵒᵈ
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_le_of_forall_enorm_le : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {m : MeasureTheory.Measure X},
  (∀ (E : Set X), MeasurableSet E → ‖μ E‖ₑ ≤ m E) → μ.variation ≤ m
-- Mathlib.Topology.Separation.Basic
Set.Finite.continuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T1Space X] [inst_2 : TopologicalSpace Y] {s : Set X},
  s.Finite → ∀ (f : X → Y), ContinuousOn f s
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits : ∀ {p : ℕ} (L : List ℕ) {h_nonempty : L ≠ []},
  L.getLast h_nonempty ≠ 0 →
    (∀ l ∈ L, l < p) → (p - 1) * ∑ i ∈ Finset.range L.length, Nat.ofDigits p L / p ^ i.succ = Nat.ofDigits p L - L.sum
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- `leftSection` splits `g`  -/
CategoryTheory.IsSplitCoequalizer.leftSection_bottom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp self.leftSection (CategoryTheory.CategoryStruct.comp g h) = h
-- Lean.Meta.Tactic.Simp.Main
/-- Auxiliary `dsimproc` for not visiting `Char` literal subterms.
 -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.doNotVisitCharLit : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Rat.Cast.Order
NNRat.ofNat_le_cast : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} {n : ℕ}
  [inst_3 : n.AtLeastTwo], OfNat.ofNat n ≤ ↑p ↔ OfNat.ofNat n ≤ p