mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
  ((hY.spineEquiv 2 SSet.Truncated.liftOfStrictSegal.f₂._proof_5)
          (SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY x)).arrow
      1 =
    f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) x)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_subset_Icc_union_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Icc a c ⊆ Set.Icc a b ∪ Set.Icc b c
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
/-- The **signed** variation of `f` on the interval `Icc a b` intersected with the set `s`,
squashed to a real (therefore only really meaningful if the variation is finite)
 -/
variationOnFromTo : {α : Type u_1} → [LinearOrder α] → {E : Type u_2} → [PseudoEMetricSpace E] → (α → E) → Set α → α → α → ℝ
-- Init.Notation
/-- `prec` is a builtin syntax category for precedences. A precedence is a value
that expresses how tightly a piece of syntax binds: for example `1 + 2 * 3` is
parsed as `1 + (2 * 3)` because `*` has a higher precedence than `+`.
Higher numbers denote higher precedence.
In addition to literals like `37`, there are some special named precedence levels:
* `arg` for the precedence of function arguments
* `max` for the highest precedence used in term parsers (not actually the maximum possible value)
* `lead` for the precedence of terms not supposed to be used as arguments
and you can also add and subtract precedences.  -/
Lean.Parser.Category.prec : Lean.Parser.Category
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Pigeonhole principle for measure spaces: if `s` is a `Finset` and
`∑ i ∈ s, μ (t i) > μ univ`, then one of the intersections `t i ∩ t j` is not empty.  -/
MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : Finset ι} {t : ι → Set α},
  (∀ i ∈ s, MeasureTheory.NullMeasurableSet (t i) μ) →
    μ Set.univ < ∑ i ∈ s, μ (t i) → ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty
-- Aesop.Search.Expansion.Norm
Aesop.runFirstNormRule : Lean.MVarId →
  Aesop.UnorderedArraySet Lean.MVarId →
    Array (Aesop.IndexMatchResult Aesop.NormRule) → Aesop.NormM (Option (Aesop.DisplayRuleName × Aesop.NormRuleResult))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given
```
Y₃ - i₃ -> X₃
|          |
g₂         f₂
∨          ∨
Y₂ - i₂ -> X₂
|          |
g₁         f₁
∨          ∨
Y₁ - i₁ -> X₁
```
The bottom square is a pushout if the top square and the big square are.
 -/
CategoryTheory.Limits.botSquareIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y₃ Y₂ Y₁ X₃ : C} →
      {g₂ : Y₃ ⟶ Y₂} →
        {g₁ : Y₂ ⟶ Y₁} →
          {i₃ : Y₃ ⟶ X₃} →
            {t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃} →
              {i₂ : Y₂ ⟶ t₁.pt} →
                (t₂ : CategoryTheory.Limits.PushoutCocone g₁ i₂) →
                  (hi₂ : i₂ = t₁.inl) →
                    CategoryTheory.Limits.IsColimit t₁ →
                      CategoryTheory.Limits.IsColimit (t₁.pasteVert t₂ hi₂) → CategoryTheory.Limits.IsColimit t₂
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.insert : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Std.TreeSet.Raw α cmp
-- Init.Data.List.MinMax
List.min?_eq_some_iff_subtype : ∀ {α : Type u_1} {a : α} [inst : Min α] [inst_1 : LE α] {xs : List α} [inst_2 : Std.MinEqOr α]
  [Std.IsLinearOrder { x // x ∈ xs }] [Std.LawfulOrderMin { x // x ∈ xs }], xs.min? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, a ≤ b
-- Init.Data.String.Lemmas.Iterate
String.Slice.foldl_eq_foldl_toList : ∀ {α : Type u} {f : α → Char → α} {init : α} {s : String.Slice},
  String.Slice.foldl f init s = List.foldl f init s.copy.toList
-- Mathlib.NumberTheory.Divisors
Nat.perfect_iff_sum_properDivisors : ∀ {n : ℕ}, 0 < n → (n.Perfect ↔ ∑ i ∈ n.properDivisors, i = n)
-- Mathlib.Data.Finset.Sups
Finset.disjSups_empty_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {t : Finset α}, ∅.disjSups t = ∅
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_union_le`. -/
EMetric.hausdorffEdist_union_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s₁ s₂ t₁ t₂ : Set α},
  Metric.hausdorffEDist (s₁ ∪ s₂) (t₁ ∪ t₂) ≤ max (Metric.hausdorffEDist s₁ t₁) (Metric.hausdorffEDist s₂ t₂)
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If a function is `C^n` with `1 ≤ n` around a point, then the derivative of `f` at this point
is also a strict derivative.  -/
ContDiffAt.hasStrictDerivAt : ∀ {n : WithTop ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {F' : Type u_3} [inst_1 : NormedAddCommGroup F']
  [inst_2 : NormedSpace 𝕂 F'] {f : 𝕂 → F'} {x : 𝕂}, ContDiffAt 𝕂 n f x → n ≠ 0 → HasStrictDerivAt f (deriv f x) x
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_ne_one_of_charC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.Linarith.Context α)
  (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.zero_ne_one_of_charC_cert c p = true →
    Lean.Grind.Linarith.Var.denote ctx 0 = One.one → Lean.Grind.Linarith.Poly.denote' ctx p ≠ 0
-- Mathlib.Data.NNReal.Basic
NNReal.coe_multiset_prod : ∀ (s : Multiset NNReal), ↑s.prod = (Multiset.map NNReal.toReal s).prod
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.bot : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
  x ≡ y [SMOD ⊥] ↔ x = y
-- Init.Core
imp_congr_left : ∀ {a b c : Prop}, (a ↔ b) → (a → c ↔ b → c)
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousOn.div₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α] {s : Set α},
  ContinuousOn f s → ContinuousOn g s → (∀ x ∈ s, g x ≠ 0) → ContinuousOn (fun x => f x / g x) s
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Given a presieve `S` on `X`, and presieve `R` on `Y` for each
`f : Y ⟶ X` in `S`, produce a presieve on `X`:
`{ g ≫ f | (f : Y ⟶ X) ∈ S, (g : Z ⟶ Y) ∈ R f }`.
 -/
CategoryTheory.Presieve.bind : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (S : CategoryTheory.Presieve X) →
        (⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y) → CategoryTheory.Presieve X
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.tsum_fiberwise : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  [CompleteSpace α] [T2Space α] {f : β → α} {a : α},
  HasSum f a → ∀ (g : β → γ), HasSum (fun c => ∑' (b : ↑(g ⁻¹' {c})), f ↑b) a
-- Mathlib.Analysis.Fourier.Notation
FourierInvModule.toFourierTransformInv : {R : Type u_5} →
  {E : Type u_6} →
    {F : outParam (Type u_7)} →
      [inst : Add E] →
        [inst_1 : Add F] → [inst_2 : SMul R E] → [inst_3 : SMul R F] → FourierInvModule R E F → FourierTransformInv E F
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.nonarchimedean : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℤ_[p]), ‖q + r‖ ≤ max ‖q‖ ‖r‖
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.isLittleO_const_left_of_properSpace_of_discreteTopology : ∀ {α : Type u_1} (a : α) [inst : NormedAddCommGroup α] [DiscreteTopology α] [ProperSpace α],
  (fun x => a) =o[Filter.cofinite] fun x => ‖x‖
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_singleton : ∀ {m n : ℤ}, n = m + 2 → (m<...n).toArray = #[m + 1]
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_comp_const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜},
  DifferentiableAt 𝕜 (fun x => f (b - x)) a ↔ DifferentiableAt 𝕜 f (b - a)
-- Mathlib.Algebra.Quaternion
Quaternion.instIsStarNormal : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), IsStarNormal a
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_refl_real : ∀ (r : ℝ), (↑r).IsSt r
-- Aesop.RuleTac.Basic
/-- A diff between the goal the rule was run on and this goal. Many `MetaM`
tactics report information that allows you to easily construct a `GoalDiff`.
If you don't have access to such information, use `diffGoals`, but note that
it may not give optimal results.
 -/
Aesop.Subgoal.diff : Aesop.Subgoal → Aesop.GoalDiff
-- Mathlib.Data.Nat.Bits
Nat.bodd_one : Nat.bodd 1 = true
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.inclusion_inj : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H ≤ K) {x y : ↥H},
  (Subgroup.inclusion h) x = (Subgroup.inclusion h) y ↔ x = y
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.instMonoidalCategoryStruct : (R : Type u) → [inst : CommRing R] → CategoryTheory.MonoidalCategoryStruct (HopfAlgCat R)
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of the forward direction of `continuous_neg_iff`. -/
Continuous.of_neg : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G]
  [inst_3 : TopologicalSpace α] {f : α → G}, Continuous (-f) → Continuous f
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal : Type
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_sum_lex : ∀ {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.type (Sum.Lex r s) = Ordinal.type r + Ordinal.type s
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toExtension_σ : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) (a : S), P.toExtension.σ a = P.σ a
-- Batteries.Data.BinomialHeap.Basic
/-- Computes `s.rank + r`  -/
Batteries.BinomialHeap.Imp.HeapNode.rankTR.go : {α : Type u_1} → Batteries.BinomialHeap.Imp.HeapNode α → ℕ → ℕ
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.lift.eq_1 : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  (φ : G →+ M) (HN : N ≤ φ.ker), QuotientAddGroup.lift N φ HN = (QuotientAddGroup.con N).lift φ ⋯
-- Mathlib.SetTheory.Cardinal.NatCard
Set.eq_top_of_card_le_of_finite : ∀ {α : Type u_1} [Finite α] {s : Set α}, Nat.card α ≤ Nat.card ↑s → s = ⊤
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Continuous.rpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ℝ},
  Continuous f → Continuous g → (∀ (x : α), f x ≠ 0 ∨ 0 < g x) → Continuous fun x => f x ^ g x
-- Std.Http.Data.Chunk
Std.Http.Chunk.instDecidableEqExtensionValue : DecidableEq Std.Http.Chunk.ExtensionValue
-- Mathlib.GroupTheory.MonoidLocalization.DivPairs
AddSubmonoid.subPairs.eq_1 : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (f : ⊤.LocalizationMap G)
  (s : AddSubmonoid G), AddSubmonoid.subPairs f s = AddSubmonoid.comap (subAddMonoidHom.comp ((↑f).prodMap ↑f)) s
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_strictMonoOn : StrictMonoOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.IsBisimulation.mk : ∀ {F : PFunctor.{uA, uB}} {R : F.M → F.M → Prop},
  (∀ {a a' : F.A} {f : F.B a → F.M} {f' : F.B a' → F.M}, R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a', f'⟩) → a = a') →
    (∀ {a : F.A} {f f' : F.B a → F.M},
        R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a, f'⟩) → ∀ (i : F.B a), R (f i) (f' i)) →
      PFunctor.M.IsBisimulation R
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.IsInitial.subsingleton_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C}
  (hI : CategoryTheory.Limits.IsInitial I) {A : C}, Subsingleton (A ⟶ I)
-- Mathlib.Data.List.DropRight
List.rdrop.eq_1 : ∀ {α : Type u_1} (l : List α) (n : ℕ), l.rdrop n = List.take (l.length - n) l
-- Init.Data.List.Perm
List.perm_cons_append_cons : ∀ {α : Type u_1} {l l₁ l₂ : List α} (a : α), l.Perm (l₁ ++ l₂) → (a :: l).Perm (l₁ ++ a :: l₂)
-- Mathlib.Data.Finset.Basic
Equiv.Finset.union_symm_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (h : Disjoint s t) {i : α} (hi : i ∈ t) (hi' : i ∈ s ∪ t),
  (Equiv.Finset.union s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.coe_refl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (n : WithTop ℕ∞), ⇑(Diffeomorph.refl I M n) = id
-- Init.Data.UInt.Lemmas
UInt8.ofNat_eq_iff_mod_eq_toNat : ∀ (a : ℕ) (b : UInt8), UInt8.ofNat a = b ↔ a % 2 ^ 8 = b.toNat
-- Plausible.Random
Plausible.Random.instBoundedRandomFin : {m : Type → Type u_1} → [Monad m] → {n : ℕ} → Plausible.BoundedRandom m (Fin n)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.mergeSort.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (a : α) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match [a], x with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_2 a x
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_mem_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y),
  P f → P.map F (F.map f)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.subtypeRestr_target_subset : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s),
  (e.subtypeRestr hs).target ⊆ e.target
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_Iic : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R},
  0 ≤ a → Nat.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋₊
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_finset_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {a : α}
  [inst_3 : Fintype β], a • Finset.univ = Finset.univ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.union m₂).contains k = true → m₂.contains k = false → m₁.contains k = true
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_union_closure_right_eq : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk (X ∪ M.closure Y) = M.eRk (X ∪ Y)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.mk : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                (toFun' :
                    (S : Type u) →
                      [inst_5 : CommSemiring S] → [inst_6 : Algebra R S] → TensorProduct R S M → TensorProduct R S N) →
                  autoParam
                      (∀ {S : Type u} [inst_5 : CommSemiring S] [inst_6 : Algebra R S] {S' : Type u}
                        [inst_7 : CommSemiring S'] [inst_8 : Algebra R S'] (φ : S →ₐ[R] S'),
                        ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ toFun' S =
                          toFun' S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap))
                      PolynomialLaw.isCompat'._autoParam →
                    M →ₚₗ[R] N
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_le : ∀ {n : ℕ} {x : Fin (2 ^ n)} {y : BitVec n}, { toFin := x } ≤ y ↔ x ≤ y.toFin
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_algebraMap : ∀ {R A : Type u} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (f : R)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen f),
  AlgebraicGeometry.StructureSheaf.const ((algebraMap R A) f) f U hu = 1
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.Equiv.coe_toElementaryEmbedding : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), ⇑f.toElementaryEmbedding = ⇑f
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
_private.Mathlib.LinearAlgebra.TensorProduct.Graded.External.0.TensorProduct.term𝒜ℬ : Lean.ParserDescr
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalSym : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Enriched.Basic
/-- We verify that the presheaf representing natural transformations
between `Type v`-enriched functors is actually represented by
the usual type of natural transformations!
 -/
CategoryTheory.enrichedNatTransYonedaTypeIsoYonedaNatTrans : {C : Type v} →
  [inst : CategoryTheory.EnrichedCategory (Type v) C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.EnrichedCategory (Type v) D] →
        (F G : CategoryTheory.EnrichedFunctor (Type v) C D) →
          CategoryTheory.enrichedNatTransYoneda F G ≅
            CategoryTheory.yoneda.obj
              (CategoryTheory.enrichedFunctorTypeEquivFunctor F ⟶ CategoryTheory.enrichedFunctorTypeEquivFunctor G)
-- Mathlib.Data.Nat.Pairing
Nat.pairEquiv_symm_apply : ⇑Nat.pairEquiv.symm = Nat.unpair
-- Mathlib.Analysis.Convex.Basic
/-- Lift the convexity of a set up through a scalar tower.  -/
Convex.lift : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : Module 𝕜 E] (R : Type u_5) [inst_5 : Semiring R] [inst_6 : PartialOrder R]
  [inst_7 : Module R E] [inst_8 : Module R 𝕜] [IsScalarTower R 𝕜 E] [SMulPosMono R 𝕜] {s : Set E},
  Convex 𝕜 s → Convex R s
-- Std.Time.Format.Modifier
Std.Time.instReprOffsetO.repr : Std.Time.OffsetO → ℕ → Std.Format
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.EventuallyEq.of_eventually_mem_of_forall_separating_preimage : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → β} (p : Set β → Prop) {s : Set β}
  [HasCountableSeparatingOn β p s],
  (∀ᶠ (x : α) in l, f x ∈ s) → (∀ᶠ (x : α) in l, g x ∈ s) → (∀ (U : Set β), p U → f ⁻¹' U =ᶠ[l] g ⁻¹' U) → f =ᶠ[l] g
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
_private.Mathlib.RingTheory.WittVector.FrobeniusFractionField.0.WittVector.frobeniusRotationCoeff.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_set_EStateM_apply_eq : ∀ {σ ε : Type} {post : PUnit.{1} → σ → Prop} {epost : ε → σ → Prop} (x : σ),
  Std.Internal.Do.wp (set x) post epost = fun x_1 => post PUnit.unit x
-- Mathlib.Analysis.Convex.AmpleSet
/-- A set is ample iff its affine translation is.  -/
AmpleSet.vadd_iff : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  {s : Set E} {y : E}, AmpleSet (y +ᵥ s) ↔ AmpleSet s
-- Lean.Meta.CongrTheorems
Lean.Meta.hcongrThmSuffixBase : String
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubOffset_2 : HSub Std.Time.WallTime Std.Time.Hour.Offset Std.Time.WallTime
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_zero_fun : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  ProbabilityTheory.mgf 0 μ t = μ.real Set.univ
-- Mathlib.Topology.Compactification.StoneCech
/-- The image of `stoneCechUnit` is dense. (But `stoneCechUnit` need
not be an embedding, for example if the original space is not Hausdorff.)  -/
denseRange_stoneCechUnit : ∀ {α : Type u} [inst : TopologicalSpace α], DenseRange stoneCechUnit
-- Mathlib.Logic.Function.Basic
Function.instIsStrictWeakOrderOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [IsStrictWeakOrder β r],
  IsStrictWeakOrder α (Function.onFun r f)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullback.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C)
  (arrows arrows_1 : (j : J) → objs j ⟶ B) (e_arrows : arrows = arrows_1)
  [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows],
  CategoryTheory.Limits.widePullback B objs arrows = CategoryTheory.Limits.widePullback B objs arrows_1
-- Lean.Parser.Attr
Lean.Parser.Attr.class.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.trans_le : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g h : α → β}, f =ᶠ[l] g → g ≤ᶠ[l] h → f ≤ᶠ[l] h
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsIsoQinv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s),
  CategoryTheory.IsIso (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.extendCone_obj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone (F.comp G)),
  (CategoryTheory.Functor.Initial.extendCone.obj c).pt = c.pt
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- If `G` acts on `R` as a `MulSemiringAction`, then it also acts on `IsLocalRing.ResidueField R`.
 -/
IsLocalRing.ResidueField.instMulSemiringAction : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsLocalRing R] →
      (G : Type u_4) → [inst_2 : Group G] → [MulSemiringAction G R] → MulSemiringAction G (IsLocalRing.ResidueField R)
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.id_apply : ∀ (X : FinPartOrd) (x : ↑X.toPartOrd), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Init.System.IO
/-- The file should be opened for writing.

If the file does not already exist, it is created. If the file already exists, it is opened, and
the read/write cursor is positioned at the end of the file.

* `open` flags: `O_WRONLY | O_CREAT | O_APPEND`
* `fdopen` mode: `a`
 -/
IO.FS.Mode.append : IO.FS.Mode
-- Init.Data.Int.Order
Int.sub_one_lt_of_le : ∀ {a b : ℤ}, a ≤ b → a - 1 < b