mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.length = p.length
-- Mathlib.Combinatorics.Graph.Subgraph
/-- **Alias** of `Graph.Compatible.of_le`. -/
Graph.IsSubgraph.compatible : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → H.Compatible G
-- Lean.Server.Requests
Lean.Server.RequestTask : Type u_1 → Type u_1
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.isRegularAtInfty_iff : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.periods], 𝒢.IsRegularAtInfty ↔ 𝒢.widthInfty ∈ 𝒢.strictPeriods
-- Mathlib.Data.ENNReal.Basic
ENNReal.instOrderedSub : OrderedSub ENNReal
-- Mathlib.Data.Part
Part.of_toOption : ∀ {α : Type u_1} (o : Part α) [inst : Decidable o.Dom], ↑o.toOption = o
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore_ι : ∀ {m : ℕ} (k : Fin (m + 1)) (n : ℕ), (SSet.prodStdSimplex.pairingCore k n).ι = SSet.prodStdSimplex.pairingCore.Type₁ k n
-- Mathlib.CategoryTheory.Functor.Category
/-- `hcomp α β` is the horizontal composition of natural transformations.  -/
CategoryTheory.NatTrans.hcomp : {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] →
            {F G : CategoryTheory.Functor C D} →
              {H I : CategoryTheory.Functor D E} → (F ⟶ G) → (H ⟶ I) → (F.comp H ⟶ G.comp I)
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.currentTimeout : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Group.Action.End
MulAction.toPermHom_apply : ∀ (G : Type u_1) (α : Type u_5) [inst : Group G] [inst_1 : MulAction G α] (a : G),
  (MulAction.toPermHom G α) a = MulAction.toPerm a
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.nonempty_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.Nonempty ↔ ∃ X, P X
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.cechNerve_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  {X Y : SimplexCategoryᵒᵖ} (g : X ⟶ Y),
  f.cechNerve.map g =
    CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom)
      (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) i)) ⋯
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_right : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      AddMonoidAlgebra.Monic D p →
        q ≠ 0 → AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_mul_iff_one_le_right' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) {b : α},
  a ≤ a * b ↔ 1 ≤ b
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.compAlternatingMap_add : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {N₂ : Type u_11} [inst_5 : AddCommMonoid N₂]
  [inst_6 : Module R N₂] (g : N →ₗ[R] N₂) (f₁ f₂ : M [⋀^ι]→ₗ[R] N),
  g.compAlternatingMap (f₁ + f₂) = g.compAlternatingMap f₁ + g.compAlternatingMap f₂
-- Init.Data.List.Count
List.countP.go.eq_def : ∀ {α : Type u} (p : α → Bool) (a : List α) (a_1 : ℕ),
  List.countP.go p a a_1 =
    match a, a_1 with
    | [], acc => acc
    | x :: xs, acc => bif p x then List.countP.go p xs (acc + 1) else List.countP.go p xs acc
-- Mathlib.Data.List.Sublists
List.nodup_sublistsLen : ∀ {α : Type u} (n : ℕ) {l : List α}, l.Nodup → (List.sublistsLen n l).Nodup
-- Init.Data.List.Lemmas
List.getElem?_replace_of_ne : ∀ {α : Type u_1} [inst : BEq α] {a b : α} [LawfulBEq α] {l : List α} {i : ℕ},
  l[i]? ≠ some a → (l.replace a b)[i]? = l[i]?
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.qParam_left_inv_mod_period : ∀ {h : ℝ}, h ≠ 0 → ∀ (z : ℂ), ∃ m, Function.Periodic.invQParam h (Function.Periodic.qParam h z) = z + ↑m * ↑h
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_9 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match Turing.PartrecToTM2.Λ'.ret k.cons₂ with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_9 k
-- Init.Data.List.Lemmas
List.mem_or_eq_of_mem_set : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a b : α}, a ∈ l.set i b → a ∈ l ∨ a = b
-- Lean.Attributes
Lean.instBEqAttributeApplicationTime.beq : Lean.AttributeApplicationTime → Lean.AttributeApplicationTime → Bool
-- Init.Data.ByteArray.Lemmas
ByteArray.ext_getElem : ∀ {a b : ByteArray}, a.size = b.size → (∀ (i : ℕ) (hi : i < a.size) (hi' : i < b.size), a[i] = b[i]) → a = b
-- Mathlib.Topology.Basic
Classical.epsilon.eq_1 : ∀ {α : Sort u} [h : Nonempty α] (p : α → Prop), Classical.epsilon p = ↑(Classical.strongIndefiniteDescription p h)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- **Alias** of `Polynomial.leadingCoeff_le_mahlerMeasure`. -/
Polynomial.leading_coeff_le_mahlerMeasure : ∀ (p : Polynomial ℂ), ‖p.leadingCoeff‖ ≤ p.mahlerMeasure
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.eval₂_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {T : Type u_6} [inst_3 : CommRing T] [inst_4 : UniformSpace T]
  [T2Space T] [CompleteSpace T] [IsUniformAddGroup T] [IsTopologicalRing T] [IsLinearTopology T T]
  [inst_10 : Algebra R T] [inst_11 : Algebra S T] [IsScalarTower R S T] [inst_13 : UniformSpace R]
  [DiscreteUniformity R] [inst_15 : UniformSpace S] [DiscreteUniformity S],
  MvPowerSeries.HasSubst a →
    ∀ {b : τ → T},
      MvPowerSeries.HasEval b →
        ∀ (f : MvPowerSeries σ R),
          MvPowerSeries.eval₂ (algebraMap S T) b (MvPowerSeries.subst a f) =
            MvPowerSeries.eval₂ (algebraMap R T) (fun s => MvPowerSeries.eval₂ (algebraMap S T) b (a s)) f
-- Lean.Environment
/-- The main module data that will eventually be used to construct the publicly accessible constants.  -/
_private.Lean.Environment.0.Lean.ImportedModule.publicModule? : Lean.ImportedModule✝ → Option Lean.ModuleData
-- Mathlib.Algebra.Group.Defs
IsMulTorsionFree.mk : ∀ {M : Type u_2} [inst : Monoid M], (∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun a => a ^ n) → IsMulTorsionFree M
-- Init.Data.UInt.Lemmas
UInt32.toFin_ofNatLT : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatLT n hn).toFin = ⟨n, hn⟩
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.hasExpired : Lean.Server.FileWorker.RpcSession → IO Bool
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_node4R : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  Ordnode.All P (l.node4R x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.usize.injEq : ∀ (val val_1 : UInt64),
  (Lean.Compiler.LCNF.LitValue.usize val = Lean.Compiler.LCNF.LitValue.usize val_1) = (val = val_1)
-- Mathlib.Topology.Algebra.Group.Quotient
/-- The quotient of a second countable topological group by a subgroup is second countable.  -/
QuotientGroup.instSecondCountableTopology : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (N : Subgroup G)
  [SecondCountableTopology G], SecondCountableTopology (G ⧸ N)
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.instRingSubtypeMem : {K : Type u} → [inst : DivisionRing K] → (s : Subfield K) → Ring ↥s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.w_prod_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D') {X Y : CategoryTheory.StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y) {Z : D'}
  (h : T'.obj Y.right.2 ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.hom.2
      (CategoryTheory.CategoryStruct.comp (T'.map (CategoryTheory.StructuredArrow.Hom.right f).2) h) =
    CategoryTheory.CategoryStruct.comp Y.hom.2 h
-- Init.Control.Reader
/-- Recovers from errors. The same local value is provided to both branches. Typically used via the
`<|>` operator.
 -/
ReaderT.orElse : {m : Type u_1 → Type u_2} → {ρ α : Type u_1} → [Alternative m] → ReaderT ρ m α → (Unit → ReaderT ρ m α) → ReaderT ρ m α
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.hasCoequalizers_of_hasWideCoequalizers : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideCoequalizers C],
  CategoryTheory.Limits.HasCoequalizers C
-- Mathlib.Computability.NFA
NFA.mk.injEq : ∀ {α : Type u} {σ : Type v} (step : σ → α → Set σ) (start accept : Set σ) (step_1 : σ → α → Set σ)
  (start_1 accept_1 : Set σ),
  ({ step := step, start := start, accept := accept } = { step := step_1, start := start_1, accept := accept_1 }) =
    (step = step_1 ∧ start = start_1 ∧ accept = accept_1)
-- Init.Omega.IntList
Lean.Omega.IntList.set_nil_zero : ∀ {y : ℤ}, Lean.Omega.IntList.set [] 0 y = [y]
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.congr_atTop : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α] {f₁ g₁ : ℕ → α},
  Summable f₁ → f₁ =ᶠ[Filter.atTop] g₁ → Summable g₁
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- If `η` is a lax transformation between `F` and `G`, we have a 1-morphism
`η.app a : F.obj a ⟶ G.obj a` for each object `a : B`. We also have a 2-morphism
`η.naturality f : app a ≫ G.map f ⟶ F.map f ≫ app b` for each 1-morphism `f : a ⟶ b`.
These 2-morphisms satisfy the naturality condition, and preserve the identities and
the compositions modulo some adjustments of domains and codomains of 2-morphisms.
 -/
CategoryTheory.Oplax.LaxTrans : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.OplaxFunctor B C → CategoryTheory.OplaxFunctor B C → Type (max (max (max u₁ v₁) v₂) w₂)
-- Mathlib.CategoryTheory.Sites.Spaces
/-- The pretopology associated to a space is the largest pretopology that
generates the Grothendieck topology associated to the space.  -/
Opens.toPretopology_grothendieckTopology : ∀ (T : Type u) [inst : TopologicalSpace T], (Opens.grothendieckTopology T).toPretopology = Opens.pretopology T
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.hasFPowerSeriesOnBall : ∀ {𝕜 : 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] (f : E →L[𝕜] F)
  (x : E), HasFPowerSeriesOnBall (⇑f) (f.fpowerSeries x) x ⊤
-- Std.Async.Signal
Std.Async.Signal.sighup.sizeOf_spec : sizeOf Std.Async.Signal.sighup = 1
-- Mathlib.Topology.Category.TopCat.Opens
/-- An open map `f : X ⟶ Y` induces a functor `Opens X ⥤ Opens Y`.
 -/
IsOpenMap.functor : {X Y : TopCat} →
  {f : X ⟶ Y} →
    IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f) →
      CategoryTheory.Functor (TopologicalSpace.Opens ↑X) (TopologicalSpace.Opens ↑Y)
-- Std.Time.Format.Basic
Std.Time.GenericFormat.mk : {awareness : Std.Time.Awareness} → Std.Time.FormatConfig → Std.Time.FormatString → Std.Time.GenericFormat awareness
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {a : α} {fallback : β a}, Std.DTreeMap.Internal.Impl.contains a t = false → t.getD a fallback = fallback
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.nat_log_helper : ∀ (b n k : ℕ), (b ^ k).ble n = true → n.blt (b ^ (k + 1)) = true → Nat.log b n = k
-- Init.Data.ByteArray.Lemmas
_private.Init.Data.ByteArray.Lemmas.0.ByteArray.set.match_1.splitter : (motive : (x : ByteArray) → (x_1 : ℕ) → UInt8 → x_1 < x.size → Sort u_1) →
  (x : ByteArray) →
    (x_1 : ℕ) →
      (x_2 : UInt8) →
        (x_3 : x_1 < x.size) →
          ((bs : Array UInt8) → (i : ℕ) → (b : UInt8) → (h : i < { data := bs }.size) → motive { data := bs } i b h) →
            motive x x_1 x_2 x_3
-- Init.Data.Ord.Basic
List.compareLex_cons_cons : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {xs ys : List α},
  List.compareLex cmp (x :: xs) (y :: ys) = (cmp x y).then (List.compareLex cmp xs ys)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- Walks of length two from `u` to `v` correspond bijectively to common neighbours of `u` and `v`.
Note that `u` and `v` may be the same.  -/
SimpleGraph.walkLengthTwoEquivCommonNeighbors : {V : Type u} → (G : SimpleGraph V) → (u v : V) → { p // p.length = 2 } ≃ ↑(G.commonNeighbors u v)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.id_linear : ∀ (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1], (AffineMap.id k P1).linear = LinearMap.id
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Burnside's lemma** : given a finite group `G` acting on a type `X`, the sum the orders of the
stabilisers coincides with the number of orbits multiplied by the order of `G`. 

[Wikidata Q1330377](https://www.wikidata.org/wiki/Q1330377) -/
MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group : ∀ (G : Type u) (X : Type v) [inst : Group G] [inst_1 : MulAction G X] [inst_2 : Fintype G]
  [inst_3 : (g : G) → Fintype ↑(MulAction.fixedBy X g)] [inst_4 : Fintype (Quotient (MulAction.orbitRel G X))],
  ∑ g, Fintype.card ↑(MulAction.fixedBy X g) = Fintype.card (Quotient (MulAction.orbitRel G X)) * Fintype.card G
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalNormedRing.mk : {α : Type u_5} →
  [toNorm : Norm α] →
    [toNonUnitalRing : NonUnitalRing α] →
      [toMetricSpace : MetricSpace α] →
        (∀ (x y : α), dist x y = ‖-x + y‖) → (∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖) → NonUnitalNormedRing α
-- Mathlib.Data.Sym.Basic
Sym.fill_filterNe : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (a : α) (m : Sym α n),
  Sym.fill a (Sym.filterNe a m).fst (Sym.filterNe a m).snd = m
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction.lift_seq : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] {lift : ⦃α : Type u⦄ → m α → n α}
  {α β : Type u} [LawfulMonad m] [LawfulMonad n] [Std.Internal.LawfulMonadLiftFunction lift] (mf : m (α → β))
  (ma : m α), lift (mf <*> ma) = lift mf <*> lift ma
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_union_le_size_add_size : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑(m₁.union m₂)).size ≤ (↑m₁).size + (↑m₂).size
-- Mathlib.Algebra.Colimit.Module
DirectLimit.setoid.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f f_1 : (i j : ι) → (h : i ≤ j) → T h) (e_f : f = f_1) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι],
  DirectLimit.setoid f = DirectLimit.setoid f_1
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_eq_true_iff : ∀ {s : String.Slice} {p : String.Pos.Raw},
  String.Pos.Raw.isValidForSlice s p = true ↔ String.Pos.Raw.IsValidForSlice s p
-- Aesop.Tree.Data
Aesop.Iteration.one : Aesop.Iteration
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instAddCommGroupWithOne : {R : Type u_1} → {a b : R} → [AddCommGroupWithOne R] → AddCommGroupWithOne (QuadraticAlgebra R a b)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.inv_le_iff : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : Aˣ},
  0 ≤ ↑a → 0 ≤ ↑b → (↑a⁻¹ ≤ ↑b ↔ ↑b⁻¹ ≤ ↑a)
-- Mathlib.RingTheory.AdicCompletion.Completeness
_private.Mathlib.RingTheory.AdicCompletion.Completeness.0.AdicCompletion.ofValEqZero.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {x : AdicCompletion I M} (hxn : ↑x n = 0),
  AdicCompletion.ofValEqZero I hxn = ⟨fun i => AdicCompletion.ofValEqZeroAux I ⋯ hxn, ⋯⟩
-- Mathlib.Computability.ContextFreeGrammar
instReprContextFreeRule.repr : {T : Type u_1} → {N : Type u_2} → [Repr T] → [Repr N] → ContextFreeRule T N → ℕ → Std.Format
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
_private.Mathlib.Analysis.InnerProductSpace.Projection.Submodule.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.addEquivProdDirectSum_symm_apply_support' : ∀ {ι : Type v} {α : Option ι → Type w} [inst : (i : Option ι) → AddCommMonoid (α i)]
  (f : (fun i => α i) none × Π₀ (i : ι), (fun i => α i) (some i)),
  (DirectSum.addEquivProdDirectSum.symm f).support' =
    Trunc.map (fun s => ⟨none ::ₘ Multiset.map some ↑s, ⋯⟩) f.2.support'
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.not_revMatchesAt_or_isLongestRevMatchAt_revSkipWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} (pos : s.Pos),
  ¬String.Slice.Pattern.Model.RevMatchesAt pat (pos.revSkipWhile pat) ∨
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat (pos.revSkipWhile pat) (pos.revSkipWhile pat)
-- Mathlib.GroupTheory.Nilpotent
/-- A group is nilpotent if and only if its lower central series eventually reaches
the trivial subgroup.  -/
Subgroup.nilpotent_iff_lowerCentralSeries : ∀ {G : Type u_1} [inst : Group G], Group.IsNilpotent G ↔ ∃ n, ⊤.lowerCentralSeries n = ⊥
-- Init.Data.Int.Lemmas
Int.mul_eq_mul_left_iff : ∀ {a b c : ℤ}, c ≠ 0 → (c * a = c * b ↔ a = b)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The local instances, which may contain the introduced bound variables.  -/
Lean.Meta.RefinedDiscrTree.ExprInfo.localInsts : Lean.Meta.RefinedDiscrTree.ExprInfo → Lean.LocalInstances
-- Lean.LocalContext
Lean.LocalContext.setUserName : Lean.LocalContext → Lean.FVarId → Lean.Name → Lean.LocalContext
-- Mathlib.Topology.Continuous
denseRange_iff_closure_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X}, DenseRange f ↔ closure (Set.range f) = Set.univ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.associator_inv : ∀ (X Y Z : CategoryTheory.Cat),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv =
    (((CategoryTheory.Prod.fst (↑X) (↑Y × ↑Z)).prod'
            ((CategoryTheory.Prod.snd (↑X) (↑Y × ↑Z)).comp (CategoryTheory.Prod.fst ↑Y ↑Z))).prod'
        ((CategoryTheory.Prod.snd (↑X) (↑Y × ↑Z)).comp (CategoryTheory.Prod.snd ↑Y ↑Z))).toCatHom
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.div.eq_1 : ∀ (k k_1 : ℤ),
  Int.Internal.Linear.Poly.div k (Int.Internal.Linear.Poly.num k_1) =
    Int.Internal.Linear.Poly.num (Int.Internal.Linear.cdiv k_1 k)
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.of_mul_pos : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] [Nontrivial R],
  (∀ (a b : R), 0 < a → 0 < b → 0 < a * b) → IsStrictOrderedRing R
-- Init.Data.Vector.Find
Vector.findFinIdx?_push : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {a : α} {p : α → Bool},
  Vector.findFinIdx? p (xs.push a) =
    (Option.map Fin.castSucc (Vector.findFinIdx? p xs)).or (if p a = true then some ⟨n, ⋯⟩ else none)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat : ∀ {R : CommRingCat} (ι : Type u),
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Modules.fromTildeΓ (SheafOfModules.free ι))
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.inv_hom_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (A B : Rep.{w, u, v} k G) (e : A ≅ B) (x : ↑A),
  (Rep.Hom.hom e.inv) ((Rep.Hom.hom e.hom) x) = x
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIsoX_hom_D₂ : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j j' : J),
  CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j).hom (K.D₂ c j j') =
    CategoryTheory.CategoryStruct.comp (K.flip.D₁ c j j') (K.totalFlipIsoX c j').hom
-- Lean.DocString.DeferredCheck
/-- The current namespace at the reference site.  -/
Lean.Doc.DeferredCheck.currNamespace : Lean.Doc.DeferredCheck → Lean.Name
-- Mathlib.RingTheory.Localization.Defs
Localization.mk_sum : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {ι : Type u_4} (f : ι → R) (s : Finset ι) (b : ↥M),
  Localization.mk (∑ i ∈ s, f i) b = ∑ i ∈ s, Localization.mk (f i) b