mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- `P.Quotient` is `P.Ring`-isomorphic to `S` and in particular `R`-isomorphic to `S`.  -/
Algebra.Presentation.quotientEquiv : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Presentation R S ι σ) → P.Quotient ≃ₐ[P.Ring] S
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.keys : Lean.Meta.InstanceEntry → Array Lean.Meta.InstanceKey
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {i j : ι},
  i ≠ j → ∀ {x : M}, x ∈ A i → ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm x) j = 0
-- Mathlib.Analysis.Convex.Basic
Convex.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s t : Set E}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s - t)
-- Lean.Util.MonadBacktrack
/-- Similar to `MonadState`, but it retrieves/restores only the "backtrackable" part of the state  -/
Lean.MonadBacktrack : outParam Type → (Type → Type) → Type
-- Mathlib.Analysis.Convex.EGauge
le_egauge_closedBall_one : ∀ (𝕜 : Type u_1) [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (x : E), ‖x‖ₑ ≤ egauge 𝕜 (Metric.closedBall 0 1) x
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseLeapSeconds : Std.Internal.Parsec.ByteArray.Parser ℤ →
  UInt32 → Std.Internal.Parsec.ByteArray.Parser (Array Std.Time.TimeZone.TZif.LeapSecond)
-- Mathlib.Topology.Order.Basic
nhds_bot_basis_Iic : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderBot α] [OrderTopology α]
  [Nontrivial α] [DenselyOrdered α], (nhds ⊥).HasBasis (fun a => ⊥ < a) Set.Iic
-- Mathlib.Order.Interval.Set.Image
AntitoneOn.mapsTo_Ici : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  AntitoneOn f (Set.Ici a) → Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
-- Mathlib.Data.Matrix.Reflection
/-- This can be used to prove
```lean
example (a b c d : α) [Mul α] [AddCommMonoid α] :
  dot_product ![a, b] ![c, d] = a * c + b * d :=
(dot_productᵣ_eq _ _).symm
```
 -/
Matrix.dotProductᵣ_eq : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : AddCommMonoid α] {m : ℕ} (a b : Fin m → α), Matrix.dotProductᵣ a b = a ⬝ᵥ b
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o]
  [inst_9 : Std.Internal.Do.Assertion Pred] [inst_10 : Std.Internal.Do.Assertion EPred]
  [inst_11 : Std.Internal.Do.WPMonad o Pred EPred] [inst_12 : Std.IteratorLoop α m n] [inst_13 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_16 : MonadLiftT m n] [inst_17 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β}
  {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let __x ← liftM (f b)
          match __x with
            | some c => g d c
            | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.filterMapM f it) ⦃ Q; eQ ⦄
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.p1.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g],
  AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g =
    CategoryTheory.Limits.Multicoequalizer.desc (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram X
      (fun i =>
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
      ⋯
-- Mathlib.CategoryTheory.Limits.Fubini
/-- If `coconeOfCoconeUncurry Q c` is a colimit cocone then `c` is in fact a colimit
cocone.  -/
CategoryTheory.Limits.IsColimit.ofCoconeUncurry : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              {D : CategoryTheory.Limits.DiagramOfCocones F} →
                (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) →
                  {c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.uncurry.obj F)} →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfCoconeUncurry Q c) →
                      CategoryTheory.Limits.IsColimit c
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsTopologicalGroup.rightUniformSpace.eq_1 : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  IsTopologicalGroup.rightUniformSpace G =
    { toTopologicalSpace := inst_1, uniformity := Filter.comap (fun p => p.2 * p.1⁻¹) (nhds 1), symm := ⋯, comp := ⋯,
      nhds_eq_comap_uniformity := ⋯ }
-- Mathlib.Algebra.Order.Kleene
IdemCommSemiring.toIdemSemiring : {α : Type u_5} → [self : IdemCommSemiring α] → IdemSemiring α
-- Mathlib.Util.WhatsNew
/-- `#whats_new in` executes the following command and then prints the
declarations that were added to the environment.  -/
Mathlib.WhatsNew.«command#whats_newIn__» : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toArray_rio_iff : ∀ {n i : ℕ}, 0 < (*...n).toArray[i]! ↔ i < n ∧ 0 < i
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- Euler's reflection formula for the real Gamma function.  -/
Real.Gamma_mul_Gamma_one_sub : ∀ (s : ℝ), Real.Gamma s * Real.Gamma (1 - s) = Real.pi / Real.sin (Real.pi * s)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Make a fan `f` into a limit fan by providing `lift`, `fac`, and `uniq` --
just a convenience lemma to avoid having to go through `Discrete`  -/
CategoryTheory.Limits.Fan.IsLimit.mk : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        (t : CategoryTheory.Limits.Fan f) →
          (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) →
            autoParam
                (∀ (s : CategoryTheory.Limits.Fan f) (j : β),
                  CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j)
                CategoryTheory.Limits.Fan.IsLimit.mk._auto_1 →
              autoParam
                  (∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt),
                    (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s)
                  CategoryTheory.Limits.Fan.IsLimit.mk._auto_3 →
                CategoryTheory.Limits.IsLimit t
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.copy_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  (f : ZeroAtInftyContinuousMap α β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.natDegree_quadratic : ∀ {R : Type u} {a b c : R} [inst : Semiring R],
  a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree = 2
-- Mathlib.Analysis.Convex.Combination
/-- Two simplices glue nicely if the union of their vertices is affine independent.

Note that `AffineIndependent.convexHull_inter` should be more versatile in most use cases.  -/
AffineIndependent.convexHull_inter' : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {t₁ t₂ : Finset E} [inst_5 : DecidableEq E],
  AffineIndependent R Subtype.val → (convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
-- Mathlib.Order.Partition.Basic
/-- The representative of a part belongs to the underlying set.  -/
Partition.rep_mem_supp : ∀ {α : Type u_1} {u t : Set α} {P : Partition u} (ht : t ∈ P), P.rep ht ∈ u
-- Mathlib.GroupTheory.OrderOfElement
IsMulTorsionFree.orderOf_le_one : ∀ {G : Type u_1} [inst : CommGroup G] [IsMulTorsionFree G] (g : G), orderOf g ≤ 1
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_eq_inf_minimalPrimes : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), I.height = ⨅ J ∈ I.minimalPrimes, J.height
-- Mathlib.Data.List.Infix
List.dropSlice_subset : ∀ {α : Type u_1} (n m : ℕ) (l : List α), List.dropSlice n m l ⊆ l
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Insert an element into the set, preserving balance and the BST property.
If an equivalent element is already in the set, the set is returned as is.

```
insert' 1 {1, 2, 3} = {1, 2, 3}
insert' 4 {1, 2, 3} = {1, 2, 3, 4}
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
insert' (1, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2)}
insert' (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2), (3, 1)}
```  -/
Ordnode.insert' : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Ordnode α
-- Init.Data.Array.MinMax
Array.max_mem : ∀ {α : Type u_1} [inst : Max α] [Std.MaxEqOr α] {xs : Array α} (h : xs ≠ #[]), xs.max h ∈ xs
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_natCast : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (n : ℕ), ⇑↑n = ↑n
-- Batteries.Recycling.RBTree.Alter
RBTree.RBMap.alter.adapt.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (k : α) (f : Option β → Option β) (k' : α) (v' : β),
  RBTree.RBMap.alter.adapt k f (some (k', v')) =
    match f (some v') with
    | none => none
    | some v => some (k', v)
-- Lean.LocalContext
Lean.instReprLocalDeclKind : Repr Lean.LocalDeclKind
-- Mathlib.Algebra.Order.Group.Lattice
sup_div : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulRightMono α] (a b c : α), (a ⊔ b) / c = a / c ⊔ b / c
-- Init.Data.SInt.Lemmas
Int16.ofIntLE.congr_simp : ∀ (i i_1 : ℤ) (e_i : i = i_1) (_hl : Int16.minValue.toInt ≤ i) (_hr : i ≤ Int16.maxValue.toInt),
  Int16.ofIntLE i _hl _hr = Int16.ofIntLE i_1 ⋯ ⋯
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.strictColimitsOfShape_le_colimitsOfShape : ∀ {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], P.strictColimitsOfShape J ≤ P.colimitsOfShape J
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.nil : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} (p : s.Pos),
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat p p
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeffLinearEquiv_symm_apply : ∀ (R : Type u_2) {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Type u_5)
  [inst_3 : CommSemiring S] [inst_4 : Module S M] (a : ℕ →₀ M),
  (PolynomialModule.coeffLinearEquiv R S).symm a = { coeff := a }
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {r : ℝ} {x : (NumberField.RingOfIntegers K)ˣ},
  0 ≤ r →
    ‖(NumberField.Units.logEmbedding K) (Additive.ofMul x)‖ ≤ r →
      ∀ (w : NumberField.InfinitePlace K),
        |Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x))| ≤
          ↑(Fintype.card (NumberField.InfinitePlace K)) * r
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.div` -/
MeromorphicOn.fun_div : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s t : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn s U → MeromorphicOn t U → MeromorphicOn (fun i => s i / t i) U
-- Lean.Elab.Command
/-- Returns syntax for `private` or `public` visibility depending on `isPublic`. This function should be
used to generate visibility syntax for declarations that is independent of the presence of
`public section`s.
 -/
Lean.Parser.Command.visibility.ofBool : Bool → Lean.TSyntax `Lean.Parser.Command.visibility
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgHomClass.toCoalgHom.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : FunLike F A B] [inst_8 : CoalgHomClass F R A B] (f f_1 : F),
  f = f_1 → ↑f = ↑f_1
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.normedRing : {R : Type u_1} → [inst : Ring R] → (v : AbsoluteValue R ℝ) → NormedRing (WithAbs v)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.map_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (g : X → Y),
  OnePoint.map (f ∘ g) = OnePoint.map f ∘ OnePoint.map g
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
ContDiff.differentiable_iteratedDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {n : WithTop ℕ∞} (m : ℕ),
  ContDiff 𝕜 n f → ↑m < n → Differentiable 𝕜 (iteratedDeriv m f)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'
-- Mathlib.Order.CompleteLattice.Basic
biSup_le_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : Preorder ι] {f : ι → α},
  ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j = ⨆ i, f i
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.Option.pmap_or.match_1.eq_1 : ∀ {α : Type u_1} {p : α → Prop} {o' : Option α}
  (motive : (o : Option α) → {h : ∀ (a : α), o.or o' = some a → p a} → Sort u_2)
  (h : ∀ (a : α), none.or o' = some a → p a) (h_1 : (h : ∀ (a : α), none.or o' = some a → p a) → motive none)
  (h_2 : (a : α) → (h : ∀ (a_1 : α), (some a).or o' = some a_1 → p a_1) → motive (some a)),
  (match none, h with
    | none, h => h_1 h
    | some a, h => h_2 a h) =
    h_1 h
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (D : Set (Set α)) (f : α → β),
  ScottContinuousOn D f =
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
trdeg_eq_zero_of_not_injective : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  ¬Function.Injective ⇑(algebraMap R A) → Algebra.trdeg R A = 0
-- Mathlib.Logic.Equiv.Defs
Equiv.self_comp_symm : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ⇑e ∘ ⇑e.symm = id
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- A subcomplex is the union of its closed cells.  -/
Topology.CWComplex.Subcomplex.union_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [inst : Topology.CWComplex C]
  (E : Topology.RelCWComplex.Subcomplex C), ⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n ↑j = ↑E
-- Plausible.Arbitrary
Plausible.Sigma.Arbitrary : {α : Type u_1} → {β : Type u_2} → [Plausible.Arbitrary α] → [Plausible.Arbitrary β] → Plausible.Arbitrary ((_ : α) × β)
-- Mathlib.RingTheory.IntegralDomain
exists_eq_pow_of_mul_eq_pow_of_coprime : ∀ {R : Type u_2} [inst : CommSemiring R] [GCDMonoid R] [Subsingleton Rˣ] {a b c : R} {n : ℕ},
  IsCoprime a b → a * b = c ^ n → ∃ d, a = d ^ n
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
Unitization.starLift_range : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : StarRing R] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : StarModule R A] [inst_8 : Semiring C] [inst_9 : StarRing C]
  [inst_10 : Algebra R C] [inst_11 : StarModule R C] (f : A →⋆ₙₐ[R] C),
  (Unitization.starLift f).range = StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range f)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instSubCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Sub (CauSeq.Completion.Cauchy abv)
-- Init.Omega.Int
Lean.Omega.Int.neg_congr : ∀ {a b : ℤ}, a = b → -a = -b
-- Batteries.Data.List.Pairwise
List.forall_mem_pwFilter : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R],
  (∀ {x y z : α}, R x z → R x y ∨ R y z) → ∀ (a : α) (l : List α), (∀ b ∈ List.pwFilter R l, R a b) ↔ ∀ b ∈ l, R a b
-- Mathlib.Data.Set.Notation
/-- Coercion using `(Subtype.val '' ·)`  -/
Set.Notation.instCoeHeadElem : {α : Type u_1} → {s : Set α} → CoeHead (Set ↑s) (Set α)
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo : Type
-- Mathlib.Algebra.Group.Submonoid.Basic
IsAddUnit.addSubmonoid.eq_1 : ∀ (M : Type u_4) [inst : AddMonoid M],
  IsAddUnit.addSubmonoid M = { carrier := Set.ofPred IsAddUnit, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.mul_apply_one : ∀ {R : Type u_1} [inst : Semiring R] {f g : ArithmeticFunction R}, (f * g) 1 = f 1 * g 1
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_le_dist_of_mem : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {x y : α} {s : Set α}, x ∈ s → y ∈ s → x ≠ y → s.infsep ≤ dist x y
-- Mathlib.Data.PEquiv
PEquiv.symm_trans_self : ∀ {α : Type u} {β : Type v} (f : α ≃. β), f.symm.trans f = PEquiv.ofSet {b | (f.symm b).isSome = true}
-- Mathlib.Algebra.Ring.Hom.Defs
/-- `α →+* β` denotes the type of ring homomorphisms from `α` to `β`.  -/
«term_→+*_» : Lean.TrailingParserDescr
-- Lean.Parser.Basic
/-- The `andthen(p, q)` combinator, usually written as adjacency in syntax declarations (`p q`),
parses `p` followed by `q`.

The arity of this parser is the sum of the arities of `p` and `q`:
that is, it accumulates all the nodes produced by `p` followed by the nodes from `q` into the list
of arguments to the surrounding parse node.  -/
Lean.Parser.andthen : Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Analysis.Complex.Norm
Complex.norm_intCast : ∀ (n : ℤ), ‖↑n‖ = |↑n|
-- Mathlib.Data.Finset.Preimage
Finset.sup_preimage_self : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] [inst : SemilatticeSup β] [inst_1 : OrderBot β] {s : Finset β} {f : α → β}
  (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s), (s.preimage f ⋯).sup f = s.sup id
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.GeneralLinearGroup.continuous_upperRightHom : ∀ {R : Type u_4} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R],
  Continuous ⇑Matrix.GeneralLinearGroup.upperRightHom
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_succ_right : ∀ {V : Type u_11} {E : Type u_12} [inst : LineDeriv V E E] {n : ℕ} (m : Fin (n + 1) → V) (f : E),
  LineDeriv.iteratedLineDerivOp m f =
    LineDeriv.iteratedLineDerivOp (Fin.init m) (LineDeriv.lineDerivOp (m (Fin.last n)) f)
-- Mathlib.NumberTheory.SmoothNumbers
/-- A number that divides an `n`-smooth number is itself `n`-smooth.  -/
Nat.mem_smoothNumbers_of_dvd : ∀ {n m k : ℕ}, m ∈ n.smoothNumbers → k ∣ m → k ∈ n.smoothNumbers
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.Cauchy.coeff_tendsto : ∀ {K : Type u_2} [inst : Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) (D : ℤ),
  Filter.Tendsto (fun f => f.coeff D) ℱ (Filter.principal {LaurentSeries.Cauchy.coeff hℱ D})
-- Aesop.RuleSet
/-- Rules for the builtin unfold rule. A pair `(decl, unfoldThm?)` in this map
represents a declaration `decl` which should be unfolded. `unfoldThm?` should
be the output of `getUnfoldEqnFor? decl` and is cached here for efficiency.
 -/
Aesop.BaseRuleSet.unfoldRules : Aesop.BaseRuleSet → Lean.PHashMap Lean.Name (Option Lean.Name)
-- Lean.Compiler.IR.Basic
Lean.IR.Param.ty : Lean.IR.Param → Lean.IR.IRType
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.elim_set : ∀ {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ι → Set α},
  s.PairwiseDisjoint f → ∀ {i j : ι}, i ∈ s → j ∈ s → ∀ a ∈ f i, a ∈ f j → i = j
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.liftTruncLE.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f f_1 : X ⟶ Y),
  f = f_1 → ∀ (n : ℤ) [inst_6 : t.IsLE X n], t.liftTruncLE f n = t.liftTruncLE f_1 n
-- Mathlib.FieldTheory.Separable
/-- If the minimal polynomial of `x : K` over `F` is separable, then `x` is integral over `F`,
because the minimal polynomial of a non-integral element is `0`, which is not separable.  -/
IsSeparable.isIntegral : ∀ {F : Type u_1} {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] {x : K},
  IsSeparable F x → IsIntegral F x
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G] {l : Filter α}
  {m : α → G} {a : G}, Filter.Tendsto (fun x => -m x) l (nhds (-a)) ↔ Filter.Tendsto m l (nhds a)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.map.eq_1 : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f)
  {u v : V} (p : G.Path u v), SimpleGraph.Path.map f hinj p = ⟨SimpleGraph.Walk.map f ↑p, ⋯⟩
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.sub_comp : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {π₃ : ContRepresentation R G U}
  (f g : ContIntertwiningMap π₂ π₃) (h : ContIntertwiningMap π₁ π₂), (f - g).comp h = f.comp h - g.comp h
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isAdjointPair_one : ∀ {R : Type u_1} {M : Type u_5} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃}, B.IsAdjointPair B ⇑1 ⇑1
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- Given `f : X ⟶ Y`, this is the class of `f` in the quotient `RightHomotopyClass X Y`.  -/
HomotopicalAlgebra.RightHomotopyClass.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] → (X ⟶ Y) → HomotopicalAlgebra.RightHomotopyClass X Y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi_div_sixteen : Real.sin (Real.pi / 16) = √(2 - √(2 + √2)) / 2
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.next?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (l : List α) → motive (a :: l)) → motive x