mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Group.Basic
Pi.continuousNeg : ∀ {ι : Type u_1} {C : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (C i)] [inst_1 : (i : ι) → Neg (C i)]
  [∀ (i : ι), ContinuousNeg (C i)], ContinuousNeg ((i : ι) → C i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_eq_of_sin_eq : ∀ {x y : ℝ}, Real.sin x = y → x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → Real.arcsin y = x
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂Grp_obj_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldr_loop_zero : ∀ {n : ℕ} {α : Sort u_1} (f : Fin n → α → α) (x : α), Fin.foldr.loop n f 0 ⋯ x = x
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.map_g : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms], (S.map F).g = F.map S.g
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instAddCommMonoidHom : {R : Type u} → [inst : Semiring R] → {M N : SemimoduleCat R} → AddCommMonoid (M ⟶ N)
-- Mathlib.Algebra.BrauerGroup.Defs
/-- Any member of `CSA` is central.  -/
CSA.isCentral : ∀ {K : Type u} [inst : Field K] (self : CSA K), Algebra.IsCentral K ↑self.toAlgCat
-- Mathlib.Topology.ContinuousMap.Lattice
ContinuousMap.coe_abs : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] [inst_4 : Lattice β] [inst_5 : TopologicalLattice β] (f : C(α, β)), ⇑|f| = |⇑f|
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.instStructureWithConstantsElemWithConstants : {L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] →
      (A : Set M) →
        {N : Type w'} →
          [inst_1 : L.Structure N] → (f : L.Embedding M N) → (L.withConstants ↑A).Structure (f.withConstants A)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.real_smul_neg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
  ∀ r < 0, r • j = -((-r).toNNReal • j)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projections converge pointwise to the identity map.  -/
SchauderBasis.tendsto_proj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (x : X),
  Filter.Tendsto (fun n => (b.proj n) x) Filter.atTop (nhds x)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.map_obj_hom' : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.map α β).obj X).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (α.app X.left) (F.map X.hom)) (β.app X.right)
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.abLeftHomologyData_K_coe : ∀ (S : CategoryTheory.ShortComplex Ab), ↑S.abLeftHomologyData.K = ↥(AddCommGrpCat.Hom.hom S.g).ker
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_le_iff : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_3} [inst : (i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i}
  {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j},
  i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j => q (i.succAbove j)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_isLongestMatchAt : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  pat ≠ "" →
    (String.Slice.Pattern.Model.MatchesAt pat pos ↔
      ∃ (h : String.Pos.Raw.IsValidForSlice s (pos.offset.increaseBy pat.utf8ByteSize)),
        String.Slice.Pattern.Model.IsLongestMatchAt pat pos (s.pos (pos.offset.increaseBy pat.utf8ByteSize) h))
-- Mathlib.RingTheory.Polynomial.Quotient
Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] (p q : Polynomial R),
  q.Monic → (p %ₘ q = 0 ↔ (Ideal.Quotient.mk (Ideal.span {q})) p = 0)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substInv.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)],
  P.substInv = PowerSeries.mk P.substInvFun
-- Mathlib.Data.Set.Finite.Lattice
/-- A finset is bounded above.  -/
Finset.bddAbove : ∀ {α : Type u} [inst : SemilatticeSup α] [Nonempty α] (s : Finset α), BddAbove ↑s
-- Mathlib.Analysis.Asymptotics.Lemmas
ContinuousOn.isBigO_principal : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace α] {s : Set α} {f : α → E} {c : F}
  [inst_1 : SeminormedAddGroup E] [inst_2 : Norm F],
  ContinuousOn f s → IsCompact s → ‖c‖ ≠ 0 → f =O[Filter.principal s] fun x => c
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The single object pre-`1`-hypercover obtained from taking coproducts of the components.  -/
CategoryTheory.PreOneHypercover.sigmaOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        {c : CategoryTheory.Limits.Cofan E.X} →
          CategoryTheory.Limits.IsColimit c →
            {d : CategoryTheory.Limits.Cofan E.Y'} →
              CategoryTheory.Limits.IsColimit d → CategoryTheory.PreOneHypercover S
-- Mathlib.Analysis.Calculus.Deriv.ZPow
iter_deriv_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜) (k : ℕ),
  deriv^[k] (fun y => y ^ m) x = (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `MonoidAlgebra.single m r` for `m : M`, `r : R` is the element `rm : R[M]`.  -/
MonoidAlgebra.single : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → R → MonoidAlgebra R M
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeComp_inv_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H) (X : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Limits.Cone.postcomposeComp α β).inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Analysis.Normed.Group.Real
Real.nnnorm_natCast : ∀ (n : ℕ), ‖↑n‖₊ = ↑n
-- Mathlib.Analysis.Normed.Algebra.Exponential
SemiconjBy.exp_right : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {x a b : 𝔸},
  SemiconjBy x a b → SemiconjBy x (NormedSpace.exp a) (NormedSpace.exp b)
-- Mathlib.Data.ENat.Basic
ENat.toNat_mul : ∀ (a b : ℕ∞), (a * b).toNat = a.toNat * b.toNat
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyItem.fromJson : Lean.Json → Except String Lean.Lsp.CallHierarchyItem
-- Lean.Exception
Lean.MonadRecDepth.withRecDepth : {m : Type → Type} → [self : Lean.MonadRecDepth m] → {α : Type} → ℕ → m α → m α
-- Mathlib.Data.Multiset.Fintype
Multiset.cast_apply_fst : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} (h : s = t) (x : s.ToType), ((Multiset.cast h) x).fst = x.fst
-- Mathlib.Algebra.Algebra.Tower
AlgHom.restrictScalars_injective : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B],
  Function.Injective (AlgHom.restrictScalars R)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.exradius signs = (s.exsphere signs).radius
-- Init.Control.Lawful.MonadAttach.Instances
instLawfulMonadAttachStateTOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [LawfulMonadAttach m], LawfulMonadAttach (StateT σ m)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(-∞, a)`.
When a function has a limit `m` at `-∞`, and its derivative is integrable, then the
integral of the derivative on `(-∞, a)` is `f a - m`. Version assuming differentiability
on `(-∞, a)` and continuity at `a⁻`.

Note that such a function always has a limit at minus infinity,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic`.  -/
MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto : ∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E],
  ContinuousWithinAt f (Set.Iic a) a →
    (∀ x ∈ Set.Iio a, HasDerivAt f (f' x) x) →
      MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume →
        Filter.Tendsto f Filter.atBot (nhds m) → ∫ (x : ℝ) in Set.Iic a, f' x = f a - m
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.or : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_conjTranspose : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Star R] [ContinuousStar R] {A : X → Matrix m n R}, Continuous A → Continuous fun x => (A x).conjTranspose
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_le_centralizer_centralizer : ∀ {R' : Type u_1} [inst : Semiring R'] (s : Set R'),
  Subsemiring.closure s ≤ Subsemiring.centralizer ↑(Subsemiring.centralizer s)
-- Mathlib.RingTheory.Etale.Locus
Algebra.basicOpen_subset_etaleLocus_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {f : A},
  ↑(PrimeSpectrum.basicOpen f) ⊆ Algebra.etaleLocus R A ↔ Algebra.FormallyEtale R (Localization.Away f)
-- Mathlib.Data.Set.Function
Function.LeftInverse.leftInvOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse f g → ∀ (s : Set β), Set.LeftInvOn f g s
-- Mathlib.Topology.Bornology.Basic
Bornology.eventually_ne_cobounded : ∀ {α : Type u_2} [inst : Bornology α] (a : α), ∀ᶠ (x : α) in Bornology.cobounded α, x ≠ a
-- Mathlib.Geometry.Euclidean.Projection
/-- Subtracting a point in the given subspace from the
`orthogonalProjection` produces a result in the direction of the
given subspace.  -/
EuclideanGeometry.orthogonalProjection_vsub_mem_direction : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ s),
  ↑((EuclideanGeometry.orthogonalProjection s) p₂ -ᵥ ⟨p₁, hp₁⟩) ∈ s.direction
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
/-- The morphism property on the category of topological spaces given by open embeddings.  -/
TopCat.isOpenEmbedding : CategoryTheory.MorphismProperty TopCat
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.inv_δₗ : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.LeftLinear C] (c : C) (d : D),
  CategoryTheory.inv (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d) = CategoryTheory.Functor.LaxLeftLinear.μₗ F c d
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.toLE : {α : Type u} → [self : Std.PreorderPackage α] → LE α
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
LinearMap.spectrum_toMatrix' : ∀ {R : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R]
  (f : (n → R) →ₗ[R] n → R), spectrum R (LinearMap.toMatrix' f) = spectrum R f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.category_id_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (B : CategoryTheory.Limits.Cone F),
  (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt
-- Mathlib.Algebra.Order.Ring.Archimedean
_private.Mathlib.Algebra.Order.Ring.Archimedean.0.ArchimedeanClass.zero_add' : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] (x : ArchimedeanClass R),
  0 + x = x
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.numSiblings : Aesop.Script.StepTree → Std.HashMap Lean.MVarId ℕ
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_nonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : TopologicalSpace.Compacts α}, (↑s).Nonempty ↔ s ≠ ⊥
-- Mathlib.Algebra.BigOperators.Intervals
/-- The two ways of summing over `(i, j)` in the range `a ≤ i < j < b` are equal.  -/
Finset.sum_Ico_Ico_comm' : ∀ {M : Type u_4} [inst : AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M),
  ∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico (i + 1) b, f i j = ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a j, f i j
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.contains.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (c : Std.DTreeMap.Internal.Cell α β k),
  c.contains = c.inner.isSome
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.getKeyLT k t ho he = Std.DTreeMap.Internal.Impl.getKeyLT k_1 t_1 ⋯ ⋯
-- Lean.Parser.Types
Lean.Parser.ParserModuleContext.currNamespace : Lean.Parser.ParserModuleContext → Lean.Name
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_add_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Multiset α), s ∪ t + u = s + u ∪ (t + u)
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.mk.injEq : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (toSlashInvariantForm : SlashInvariantForm Γ k)
  (holo' : MDiff ⇑toSlashInvariantForm)
  (zero_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm.toFun k)
  (toSlashInvariantForm_1 : SlashInvariantForm Γ k) (holo'_1 : MDiff ⇑toSlashInvariantForm_1)
  (zero_at_cusps'_1 : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm_1.toFun k),
  ({ toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := zero_at_cusps' } =
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := zero_at_cusps'_1 }) =
    (toSlashInvariantForm = toSlashInvariantForm_1)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.mk.sizeOf_spec : ∀ (env : Lean.Environment) (cmdEnv? : Option Lean.Environment) (fileMap : Lean.FileMap) (mctx : Lean.MetavarContext)
  (options : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (ngen : Lean.NameGenerator),
  sizeOf
      { env := env, cmdEnv? := cmdEnv?, fileMap := fileMap, mctx := mctx, options := options,
        currNamespace := currNamespace, openDecls := openDecls, ngen := ngen } =
    1 + sizeOf env + sizeOf cmdEnv? + sizeOf fileMap + sizeOf mctx + sizeOf options + sizeOf currNamespace +
        sizeOf openDecls +
      sizeOf ngen
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited β] {a : α}, Std.ExtDTreeMap.Const.get! t a = t.get! a
-- Mathlib.Analysis.Normed.Group.Basic
norm_lt_of_mem_ball' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r → ‖b‖ < ‖a‖ + r
-- Mathlib.Algebra.DirectSum.AddChar
AddChar.directSum_apply : ∀ {ι : Type u_1} {R : Type u_2} {G : ι → Type u_3} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommGroup (G i)]
  [inst_2 : CommMonoid R] (ψ : (i : ι) → AddChar (G i) R) (a : DirectSum ι fun i => G i),
  (AddChar.directSum ψ) a = (DirectSum.toAddMonoid fun i => AddChar.toAddMonoidHomEquiv (ψ i)) a
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.Subgroup.conjMulDistribMulAction : {G : Type u_3} → [inst : Group G] → {H : Subgroup G} → [H.Normal] → MulDistribMulAction (ConjAct G) ↥H
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.ulift.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X),
  𝒰.ulift = { I₀ := ↥X, X := fun x => 𝒰.X (𝒰.idx x), f := fun x => 𝒰.f (𝒰.idx x), mem₀ := ⋯ }
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.cases'.match_1.eq_2 : ∀ {n : ℕ} (motive : Fin2 n.succ → Sort u_1) (n_1 : Fin2 n) (h_1 : Unit → motive Fin2.fz)
  (h_2 : (n_2 : Fin2 n) → motive n_2.fs),
  (match n_1.fs with
    | Fin2.fz => h_1 ()
    | n.fs => h_2 n) =
    h_2 n_1
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.lift.congr_simp : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  (f f_1 : (k : ℕ) → S →+* TruncatedWittVector p k R) (e_f : f = f_1)
  (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁),
  WittVector.lift f f_compat = WittVector.lift f_1 ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_eq_coe : ∀ {α : Type u} [inst : Add α] {a b : WithTop α} {c : α}, a + b = ↑c ↔ ∃ a' b', ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
-- Mathlib.Combinatorics.SimpleGraph.Tutte
SimpleGraph.IsTutteViolator.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (u : Set V),
  G.IsTutteViolator u = (u.ncard < (⊤.deleteVerts u).coe.oddComponents.ncard)
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.isCartanSubalgebra : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [Fintype ι] [IsDomain R] [CharZero R]
  [Module.IsTorsionFree R L] [IsNoetherian R L], H.IsCartanSubalgebra
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∈ t → (cmp t.minKey! k).isLE = true
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.toUnfoldThms : Lean.Meta.SimpTheorems → Lean.PHashMap Lean.Name (Array Lean.Name)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_array : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
  (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- The product of a family of groupoids is isomorphic
to the product object in the category of Groupoids  -/
CategoryTheory.Grpd.piIsoPi : (J : Type u) → (f : J → CategoryTheory.Grpd) → CategoryTheory.Grpd.of ((j : J) → ↑(f j)) ≅ ∏ᶜ f
-- Lean.Parser.Do
Lean.Parser.doElemParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.Order.InitialSeg
PrincipalSeg.coe_fn_mk : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (t : β)
  (o : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b t),
  ⇑{ toRelEmbedding := f, top := t, mem_range_iff_rel' := o }.toRelEmbedding = ⇑f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
-- Mathlib.GroupTheory.GroupAction.Pointwise
preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : AddMonoid M]
  [inst_1 : AddMonoid N] [inst_2 : AddAction M α] [inst_3 : AddAction N β] [inst_4 : FunLike F α β]
  [AddActionSemiHomClass F σ α β] {c : M} (f : F),
  IsAddUnit c → IsAddUnit (σ c) → ∀ (t : Set β), ⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a} {k : α}, (Std.DTreeMap.map f t).contains k = t.contains k
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instIsBotZeroClass : ∀ {α : Type u_1} [inst : LE α], IsBotZeroClass (WithZero α)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_union_of_not_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.isZero_zero : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroObject V], CategoryTheory.Limits.IsZero HomologicalComplex.zero