mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNegEquiv_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (a : ↥S.leftNeg),
  (S.leftNegEquiv hS) a = (↑S.fromCommLeftNeg).toFun a
-- Init.Data.Vector.Range
Vector.reverse_range' : ∀ {s n : ℕ}, (Vector.range' s n).reverse = Vector.map (fun x => s + n - 1 - x) (Vector.range n)
-- Mathlib.Data.Subtype
Subtype.instHasEquiv_mathlib : {α : Sort u_1} → [HasEquiv α] → (p : α → Prop) → HasEquiv (Subtype p)
-- ProofWidgets.Presentation.Expr
/-- Name of the presenter to use.  -/
ProofWidgets.GetExprPresentationParams.name : ProofWidgets.GetExprPresentationParams → Lean.Name
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.of_rank_eq_zero : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Module.rank K V = 0 → FiniteDimensional K V
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- Divide a cusp form by the discriminant to get a modular form of weight `k - 12`.  -/
CuspForm.divDiscriminant : {k : ℤ} →
  CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k → ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Sequential characterization of upper hemicontinuity**:
A set-valued function `f : α → Set β` is upper hemicontinuous at `x₀ : α` if for every pair
of sequences `x : ℕ → α` and `y : ℕ → β` such that `x` tends to `x₀` and `y n ∈ f (x n)` and
`y` tends to `y₀ : β`, then `y₀ ∈ f x₀`. This requires that there is some (sequentially) compact
set containing all `f x'` for `x'` sufficiently close to `x`.

This is a partial converse of `UpperHemicontinuousAt.mem_of_tendsto`.  -/
UpperHemicontinuousAt.of_sequences : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x₀ : α}
  [(nhds x₀).IsCountablyGenerated] {K : Set β},
  IsSeqCompact K →
    (∀ᶠ (x : α) in nhds x₀, f x ⊆ K) →
      (∀ (x : ℕ → α),
          Filter.Tendsto x Filter.atTop (nhds x₀) →
            ∀ (y : ℕ → β),
              (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Filter.Tendsto y Filter.atTop (nhds y₀) → y₀ ∈ f x₀) →
        UpperHemicontinuousAt f x₀
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.lift.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A],
  SymmetricAlgebra.lift =
    (TensorAlgebra.lift R).trans ((Equiv.subtypeUnivEquiv ⋯).symm.trans (TensorAlgebra.symRingCon R M).liftₐEquiv)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.foldM_eq_foldlM_keys : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF → ∀ {f : δ → α → m' δ} {init : δ}, Std.HashMap.Raw.foldM (fun d a x => f d a) init m = List.foldlM f init m.keys
-- Batteries.Classes.Order
Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : DecidableEq α] [inst_3 : LE α],
  (∀ (x : α), ¬x < x) →
    (∀ {x y z : α}, x < y → y < z → x < z) →
      (∀ {x y : α}, ¬x < y → y ≤ x) →
        (∀ {x y : α}, x ≤ y → y ≤ x → x = y) → Std.LawfulLTCmp fun x1 x2 => compareOfLessAndEq x1 x2
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Typecheck a `MulHom` as a morphism in `Semigrp`.  -/
Semigrp.ofHom : {X Y : Type u} → [inst : Semigroup X] → [inst_1 : Semigroup Y] → (X →ₙ* Y) → (Semigrp.of X ⟶ Semigrp.of Y)
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the reverse direction of `AddCommGroup.ModEq.sub_iff_left`. -/
AddCommGroup.ModEq.sub : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a₁ a₂ b₁ b₂ : G},
  a₁ ≡ b₁ [PMOD p] → a₂ ≡ b₂ [PMOD p] → a₁ - a₂ ≡ b₁ - b₂ [PMOD p]
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- A typeclass describing the property that explicit pullbacks along inclusion maps into disjoint
unions is stable under the property `P`.
 -/
CompHausLike.HasExplicitPullbacksOfInclusions : (P : TopCat → Prop) → [CompHausLike.HasExplicitFiniteCoproducts P] → Prop
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.mk.injEq : ∀ {α : Type} (state : Std.Mutex (Std.Bounded.State✝ α)) (id : ℕ) (state_1 : Std.Mutex (Std.Bounded.State✝ α))
  (id_1 : ℕ), ({ state := state, id := id } = { state := state_1, id := id_1 }) = (state = state_1 ∧ id = id_1)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.rankOne_hom'_def`. -/
NumberField.rankOne_hom'_def : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R],
  Valuation.RankLeOne.hom' Valued.v =
    (WithZeroMulInt.toNNReal ⋯).comp
      (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt Valued.v).toMonoidWithZeroHom
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.selectPoly.eq_1 : ∀ (P : ℕ → Prop) (n : ℕ), WittVector.selectPoly P n = if P n then MvPolynomial.X n else 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.leftSMul_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ModObj.leftSMul M X)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X X) =
    CategoryTheory.SemiCartesianMonoidalCategory.snd M X
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.mk.sizeOf_spec : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (toHom : X.Hom Y.toPresheafedSpace)
  (prop : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom.stalkMap x))),
  sizeOf { toHom := toHom, prop := prop } = 1 + sizeOf toHom
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- An additive semigroup with a partial order and satisfying `AddRightCancelSemigroup`
(`a + c < b + c → a < b`) is a `AddRightCancelSemigroup`.  -/
Contravariant.toAddRightCancelSemigroup : {α : Type u_1} → [inst : AddSemigroup α] → [inst_1 : PartialOrder α] → [AddRightReflectLE α] → AddRightCancelSemigroup α
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- If
* `p : ι' → MvPolynomial ι K` is a family of polynomials (which in practice will be homogeneous
  of the same degree `N`),
* `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
* `x : ι → K` is such that for all `k : ι`,
  `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,

then the multiplicative height of `fun j ↦ (p j).eval x` is bounded below by an (explicit) positive
constant depending only on `q` times the `N`th power of the multiplicative height of `x`.  -/
Height.mulHeight_eval_ge : ∀ {K : Type u_6} [inst : Field K] {ι : Type u_7} {ι' : Type u_8} [inst_1 : Fintype ι']
  [inst_2 : Height.AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K},
  (∀ (a : ι × ι'), (q a).IsHomogeneous M) →
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
      (∀ (k : ι), ∑ j, (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) →
        (↑(Nat.card ι') ^ Height.totalWeight K * max (Height.mulHeightBound q) 1)⁻¹ * Height.mulHeight x ^ N ≤
          Height.mulHeight fun j => (MvPolynomial.eval x) (p j)
-- Mathlib.LinearAlgebra.Dimension.Constructions
Subalgebra.rank_bot : ∀ {F : Type u_2} {E : Type u_3} [inst : CommRing F] [IsDomain F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  [StrongRankCondition F] [Module.IsTorsionFree F E] [Nontrivial E], Module.rank F ↥⊥ = 1
-- Mathlib.Algebra.Group.Subgroup.Basic
Group.conjugatesOfSet.eq_1 : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Group.conjugatesOfSet s = ⋃ a ∈ s, conjugatesOf a
-- Mathlib.Topology.ContinuousOn
ContinuousAt.congr_of_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {x : α},
  ContinuousAt f x → g =ᶠ[nhds x] f → ContinuousAt g x
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The right adjoint of the adjunction which induces the comonad `(U, ε_ U, δ_ U)`.  -/
CategoryTheory.Cokleisli.Adjunction.toCokleisli : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Comonad C) → CategoryTheory.Functor C (CategoryTheory.Cokleisli U)
-- Mathlib.LinearAlgebra.Matrix.ToLin
endVecRingEquivMatrixEnd.eq_1 : ∀ (ι : Type u_1) [inst : Fintype ι] [inst_1 : DecidableEq ι] (A : Type u_3) [inst_2 : Semiring A] (M : Type u_4)
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M],
  endVecRingEquivMatrixEnd ι A M =
    { toFun := fun f i j => { toFun := fun x => f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ },
      invFun := fun m => { toFun := fun x i => ∑ j, (m i j) (x j), map_add' := ⋯, map_smul' := ⋯ }, left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these
functions tends to the integral of the upper bound, then the sequence of functions converges
almost everywhere to the upper bound.  -/
MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone : ∀ {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α},
  AEMeasurable F μ →
    Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ)) →
      (∀ᵐ (a : α) ∂μ, Monotone fun i => f i a) →
        (∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) →
          ∫⁻ (a : α), F a ∂μ ≠ ⊤ → ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (F a))
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_inf : ∀ {α : Type u_1} [inst : DecidableEq α] (f g : α →₀ ℕ),
  Finsupp.toMultiset (f ⊓ g) = Finsupp.toMultiset f ∩ Finsupp.toMultiset g
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.ext_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.Equiv M N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_sub : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (x y : M →₀ R),
  MonoidAlgebra.ofCoeff (x - y) = MonoidAlgebra.ofCoeff x - MonoidAlgebra.ofCoeff y
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is differentiable at every `x` in `[a, b]` and
its derivative is integrable on `[a, b]`, then `∫ y in a..b, deriv f y` equals `f b - f a`.

See also `integral_deriv_of_contDiffOn_Icc` for a similar theorem assuming that `f` is `C^1`.  -/
intervalIntegral.integral_deriv_eq_sub : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f : ℝ → E},
  (∀ x ∈ Set.uIcc a b, DifferentiableAt ℝ f x) →
    IntervalIntegrable (deriv f) MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, deriv f y = f b - f a
-- Mathlib.Algebra.Divisibility.Basic
RightDvd.mul_const : ∀ {α : Type u_1} [inst : Semigroup α] {b c : α} (a : α), b ∣ᵣ c → b * a ∣ᵣ c * a
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- The function sending an element `x : L` to the maximum of the norms of its coefficients
with respect to the `K`-basis `B` of `L`.  -/
Module.Basis.norm : {K : Type u_1} →
  {L : Type u_2} →
    [inst : NormedField K] →
      [inst_1 : Ring L] →
        [inst_2 : Algebra K L] → {ι : Type u_3} → [Fintype ι] → [Nonempty ι] → Module.Basis ι K L → L → ℝ
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.State : Type
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- An auxiliary lemma used to prove that the same point can't belong to more than
`2 ^ Fintype.card ι` closed boxes of a prepartition.  -/
BoxIntegral.Prepartition.injOn_setOfPred_mem_Icc_setOfPred_lower_eq : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (x : ι → ℝ),
  Set.InjOn (fun J => {i | J.lower i = x i}) {J | J ∈ π ∧ x ∈ BoxIntegral.Box.Icc J}
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_biUnion_finset : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} {T : Finset ι},
  (↑T).Pairwise (Function.onFun Disjoint s) →
    (∀ (i : ι), MeasurableSet (s i)) → μ.restrict (⋃ i ∈ T, s i) = MeasureTheory.Measure.sum fun i => μ.restrict (s ↑i)
-- Lean.Meta.Basic
/-- Configuration with key produced by `Config.toKey`.  -/
Lean.Meta.ConfigWithKey : Type
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_cert.eq_1 : ∀ (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.norm_eq_cert lhs rhs p = p.beq' (lhs.sub rhs).norm
-- Std.Http.Protocol.H1.Parser
/-- Parses a request line and returns the recognized HTTP method and version when available.

request-line = method SP request-target SP HTTP-version
 -/
Std.Http.Protocol.H1.parseRequestLineRawVersion : Std.Http.Protocol.H1.Config →
  Std.Internal.Parsec.ByteArray.Parser (Std.Http.Method × Std.Http.RequestTarget × Option Std.Http.Version)
-- Lean.Parser.Command
/-- Right-hand side of a `:=` in a declaration, a term.  -/
Lean.Parser.Command.declBody : Lean.Parser.Parser
-- Init.Data.SInt.Lemmas
Int16.ofInt_sub : ∀ (a b : ℤ), Int16.ofInt (a - b) = Int16.ofInt a - Int16.ofInt b
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  (∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)) →
    ∀ {ι : Type w} (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ),
      HasCardinalLT ι κ →
        ∃ m u,
          (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
            ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
              CategoryTheory.CategoryStruct.comp ((D i₁).isTerminal.lift hj₁) (u i₁) =
                CategoryTheory.CategoryStruct.comp ((D i₂).isTerminal.lift hj₂) (u i₂)
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The element of `lp E p` which is `a : E i` at the index `i`, and zero elsewhere.  -/
lp.single : {α : Type u_3} →
  {E : α → Type u_4} →
    [inst : (i : α) → NormedAddCommGroup (E i)] → [DecidableEq α] → (p : ENNReal) → (i : α) → E i → ↥(lp E p)
-- Init.Data.Vector.Find
Vector.findSome?_replicate_of_pos : ∀ {n : ℕ} {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α},
  0 < n → Vector.findSome? f (Vector.replicate n a) = f a
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- Constant polynomials are weighted homogeneous of degree 0.  -/
MvPolynomial.isWeightedHomogeneous_C : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M) (r : R),
  MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.C r) 0
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.dropLast_append_end_eq : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), p.vertices.dropLast ++ [b] = p.vertices
-- Mathlib.CategoryTheory.GradedObject
/-- Constructor for isomorphisms in `GradedObject`  -/
CategoryTheory.GradedObject.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {β : Type u_1} → (X Y : CategoryTheory.GradedObject β C) → ((i : β) → X i ≅ Y i) → (X ≅ Y)
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
/-- One direction of the **Borel-Cantelli lemma**
(sometimes called the "*first* Borel-Cantelli lemma"):
if `(s i)` is a countable family of sets such that `∑' i, μ (s i)` is finite,
then the limit superior of the `s i` along the cofinite filter is a null set.

Note: for the *second* Borel-Cantelli lemma (applying to independent sets in a probability space),
see `ProbabilityTheory.measure_limsup_eq_one`.  -/
MeasureTheory.measure_limsup_cofinite_eq_zero : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α]
  [Countable ι] {μ : F} {s : ι → Set α}, ∑' (i : ι), μ (s i) ≠ ⊤ → μ (Filter.limsup s Filter.cofinite) = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ_of_ne : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (d + 2)),
  i ≠ (SSet.prodStdSimplex.pairingCore.min x hd).castSucc →
    SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd i =
      (SSet.prodStdSimplex.objEquiv (x.cast hd).simplex) ((SSet.prodStdSimplex.pairingCore.min x hd).predAbove i)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.optionFunLeft.eq_1 : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R] (p : MvPowerSeries (Option σ) R),
  MvPowerSeries.optionFunLeft✝ σ R p = PowerSeries.mk fun n x => (MvPowerSeries.coeff (Finsupp.optionElim n x)) p
-- Mathlib.Combinatorics.Tiling.Tile
/-- The group elements considered to be symmetries of the prototile.  -/
DiscreteTiling.Prototile.symmetries : {G : Type u_1} →
  {X : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G X] → (self : DiscreteTiling.Prototile G X) → Subgroup ↥(MulAction.stabilizer G ↑self)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
/-- We say that a matrix represents an endomorphism of `M` if the matrix acting on `ι → R` is
equal to `f` via the projection `(ι → R) →ₗ[R] M` given by a fixed (spanning) set.  -/
Matrix.Represents : {ι : Type u_1} →
  [Fintype ι] →
    {M : Type u_2} →
      [inst : AddCommGroup M] →
        {R : Type u_3} →
          [inst_1 : CommRing R] →
            [inst_2 : Module R M] → (ι → M) → [DecidableEq ι] → Matrix ι ι R → Module.End R M → Prop
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_eq_top_of_bijective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S], Function.Bijective ⇑f → ∀ {I : Ideal R}, Ideal.map f I = ⊤ ↔ I = ⊤
-- Mathlib.Order.Max
noMinOrder_of_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMinOrder α], NoMinOrder (α × β)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.sub : {M N : SemiNormedGrp} → Sub (M ⟶ N)
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instAddMonoid : {m : Type u_1} →
  {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → AddMonoid (α i j)] → AddMonoid (DMatrix m n α)
-- Mathlib.Topology.NhdsSet
/-- An open set belongs to its own set neighborhoods filter.  -/
IsOpen.mem_nhdsSet_self : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → s ∈ nhdsSet s
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ'_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → RatFunc.Luroth.Φ'✝ E ≠ 0
-- Mathlib.Tactic.Explode.Datatypes
/-- Which other lines (aka rows) this row depends on.
`none` means that the dependency has been filtered out of the table.  -/
Mathlib.Explode.Entry.deps : Mathlib.Explode.Entry → List (Option ℕ)
-- Mathlib.Combinatorics.Matroid.Sum
Equiv.ulift.eq_1 : ∀ {α : Type v}, Equiv.ulift = { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.vComp_iff_of_essSurj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {L₂ : CategoryTheory.Functor C₂ C₃}
  {R₂ : CategoryTheory.Functor D₂ D₃} {H₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
  [R₁.EssSurj] [w.GuitartExact], (w.vComp w').GuitartExact ↔ w'.GuitartExact
-- Lean.Data.LBool
Lean.LBool.true.sizeOf_spec : sizeOf Lean.LBool.true = 1
-- Lean.Data.Json.Basic
Lean.instDecidableEqJsonNumber : DecidableEq Lean.JsonNumber
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitor_inv_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.F =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
-- Batteries.Recycling.RBTree.WF
/-- The `del` function has the `DelProp` property.  -/
RBTree.RBNode.Balanced.del : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cut : α → Ordering} {t : RBTree.RBNode α},
  t.Balanced c n → RBTree.RBNode.DelProp t.isBlack (RBTree.RBNode.del cut t) n
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_norm_lt : ∀ (α : Type u_2) [inst : NontriviallyNormedField α] {r : ℝ}, 0 < r → ∃ x, 0 < ‖x‖ ∧ ‖x‖ < r
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.success.sizeOf_spec : ∀ (a : Array LeanSearchClient.SearchResult), sizeOf (LeanSearchClient.LoogleResult.success a) = 1 + sizeOf a
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep1.mk.inj : ∀ {view : Lean.Elab.Command.InductiveView}
  {elabCtors :
    Array Lean.Elab.Command.ElabHeaderResult →
      Lean.Elab.Command.ElabHeaderResult → Array Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep2}
  {view_1 : Lean.Elab.Command.InductiveView}
  {elabCtors_1 :
    Array Lean.Elab.Command.ElabHeaderResult →
      Lean.Elab.Command.ElabHeaderResult → Array Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep2},
  { view := view, elabCtors := elabCtors } = { view := view_1, elabCtors := elabCtors_1 } →
    view = view_1 ∧ elabCtors = elabCtors_1
-- Lean.Meta.Tactic.Simp.Types
/-- Flip the proof in a `Simp.Result`.  -/
Lean.Meta.Simp.Result.mkEqSymm : Lean.Expr → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Algebra.Group.End
Equiv.Perm.eq_inv_iff_eq : ∀ {α : Type u_4} {f : Equiv.Perm α} {x y : α}, x = f⁻¹ y ↔ f x = y
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} →
            (toColimitPresentation : CategoryTheory.Limits.ColimitPresentation J X) →
              (∀ (j : J), P (toColimitPresentation.diag.obj j)) → P.ColimitOfShape J X
-- Mathlib.Algebra.Group.Shrink
Shrink.instCommSemigroup : {α : Type u_2} → [inst : Small.{v, u_2} α] → [CommSemigroup α] → CommSemigroup (Shrink.{v, u_2} α)
-- Mathlib.LinearAlgebra.StdBasis
Pi.spanSubset.eq_1 : ∀ (R : Type u_2) {η : Type u_4} [inst : Semiring R] [inst_1 : Finite η] (s : Set η),
  Pi.spanSubset R s = Submodule.span R (⇑(Pi.basisFun R η) '' s)
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.nsmul_nsmul_self : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (m n : ℕ), AddCommute (m • a) (n • a)
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_iUnion_of_monotone : ∀ {α : Type u_3} {ι : Type u_4} [inst : SemilatticeSup ι] (p : ι → Set (Set α)),
  (∀ (n : ι), IsPiSystem (p n)) → Monotone p → IsPiSystem (⋃ n, p n)
-- Aesop.RuleTac.ElabRuleTerm
Aesop.mkSimpArgs : Lean.Term → Lean.Syntax
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.ofList l cmp).getKey! k = default