mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Hint
Lean.Meta.Hint.Suggestion.mk.inj : ∀ {toTryThisSuggestion : Lean.Meta.Tactic.TryThis.Suggestion} {span? previewSpan? : Option Lean.Syntax}
  {diffGranularity : Lean.Meta.Hint.DiffGranularity} {toTryThisSuggestion_1 : Lean.Meta.Tactic.TryThis.Suggestion}
  {span?_1 previewSpan?_1 : Option Lean.Syntax} {diffGranularity_1 : Lean.Meta.Hint.DiffGranularity},
  { toTryThisSuggestion := toTryThisSuggestion, span? := span?, previewSpan? := previewSpan?,
        diffGranularity := diffGranularity } =
      { toTryThisSuggestion := toTryThisSuggestion_1, span? := span?_1, previewSpan? := previewSpan?_1,
        diffGranularity := diffGranularity_1 } →
    toTryThisSuggestion = toTryThisSuggestion_1 ∧
      span? = span?_1 ∧ previewSpan? = previewSpan?_1 ∧ diffGranularity = diffGranularity_1
-- Init.NotationExtra
/-- Apply function extensionality and introduce new hypotheses.
The tactic `funext` will keep applying the `funext` lemma until the goal target is not reducible to
```
  |-  ((fun x => ...) = (fun x => ...))
```
The variant `funext h₁ ... hₙ` applies `funext` `n` times, and uses the given identifiers to name the new hypotheses.
Patterns can be used like in the `intro` tactic. Example, given a goal
```
  |-  ((fun x : Nat × Bool => ...) = (fun x => ...))
```
`funext (a, b)` applies `funext` once and performs pattern matching on the newly introduced pair.
 -/
tacticFunext___ : Lean.ParserDescr
-- Aesop.RuleTac.Basic
Aesop.CasesTarget.patterns.inj : ∀ {patterns patterns_1 : Array Aesop.CasesPattern},
  Aesop.CasesTarget.patterns patterns = Aesop.CasesTarget.patterns patterns_1 → patterns = patterns_1
-- Mathlib.Order.IsNormal
Order.IsNormal.le_iff_forall_le : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [inst : LinearOrder α] [inst_1 : LinearOrder β],
  Order.IsNormal f → Order.IsSuccLimit a → ∀ {b : β}, f a ≤ b ↔ ∀ a' < a, f a' ≤ b
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.const_inv_smul₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddCommMonoid α]
  [inst_1 : DivisionSemiring γ] [inst_2 : Module γ α],
  Function.Periodic f c → ∀ (a : γ), Function.Periodic (fun x => f (a⁻¹ • x)) (a • c)
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.one_le_maxVar : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : MetricSpace Y], 1 ≤ GromovHausdorff.maxVar✝ X Y
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- Data extracted from an InfoTree for each tactic.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData : Type
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_mul_ofNat : ∀ {n : ℕ} [inst : n.AtLeastTwo], Cardinal.aleph0 * OfNat.ofNat n = Cardinal.aleph0
-- Mathlib.Control.Traversable.Equiv
Equiv.comp_map : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Functor t] [LawfulFunctor t] {α β γ : Type u}
  (g : α → β) (h : β → γ) (x : t' α), Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_mono : ∀ {V : Type u_1} {G G' : SimpleGraph V}, G ≤ G' → G.vertexCoverNum ≤ G'.vertexCoverNum
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.homOfLe_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  {G G' : CategoryTheory.Subfunctor F} (h : G ≤ G') {Z : CategoryTheory.Functor C (Type w)} (h_1 : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.homOfLe h)
      (CategoryTheory.CategoryStruct.comp G'.ι h_1) =
    CategoryTheory.CategoryStruct.comp G.ι h_1
-- Mathlib.Topology.Algebra.Monoid
addHomOfMemClosureRangeCoe.eq_1 : ∀ {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : Add M₁] [inst_3 : Add M₂]
  [inst_4 : ContinuousAdd M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂] [inst_6 : AddHomClass F M₁ M₂] (f : M₁ → M₂)
  (hf : f ∈ closure (Set.range fun f x => f x)), addHomOfMemClosureRangeCoe f hf = { toFun := f, map_add' := ⋯ }
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.congr : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : TopologicalSpace E]
  [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] [mE : MeasurableSpace E] {X Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P → X =ᵐ[P] Y → ProbabilityTheory.HasGaussianLaw Y P
-- Init.Data.Int.Gcd
Int.gcd_gcd_self_left_right : ∀ (m n : ℤ), (↑(n.gcd m)).gcd m = n.gcd m
-- Init.Core
neq_of_not_iff : ∀ {a b : Prop}, ¬(a ↔ b) → a ≠ b
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.contsAux.eq_2 : ∀ {K : Type u_2} [inst : DivisionRing K] (g : GenContFract K), g.contsAux 1 = { a := g.h, b := 1 }
-- Mathlib.Data.Int.ModEq
Int.ModEq.mul : ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a * c ≡ b * d [ZMOD n]
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_inter_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
/-- Extension for `Real.sin (Real.arctan _)`.  -/
Mathlib.Meta.Positivity.evalRealSinArctan : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- Given a transcendental `f : L`, the `K`-algebra isomorphism between `RatFunc K` and `L` given
by sending `X` to `f`.  -/
RatFunc.algEquivOfTranscendental : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → (f : L) → Transcendental K f → RatFunc K ≃ₐ[K] ↥K⟮f⟯
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.instIsRightAdjointUnderTopMapOfHasPushoutsAlongOfIsStableUnderCobaseChangeAlong : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X Y : T}
  [inst_1 : P.IsStableUnderComposition] (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f]
  (hPf : P f), (CategoryTheory.MorphismProperty.Under.map ⊤ hPf).IsRightAdjoint
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instRegularSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [RegularSpace M], RegularSpace Mᵈᵐᵃ
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_1.eq_2 : ∀ {β : Type u_3} (γ : Type u_1) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (acc : γ) (out : β)
  (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) (c : γ) (h : PlausibleForInStep out acc (ForInStep.done c))
  (h_1 : (c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩)
  (h_2 : (c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩),
  (match ⟨ForInStep.done c, h⟩ with
    | ⟨ForInStep.yield c, h'⟩ => h_1 c h'
    | ⟨ForInStep.done c, h⟩ => h_2 c h) =
    h_2 c h
-- Init.Data.String.Basic
List.asString_injective : ∀ {l₁ l₂ : List Char}, String.ofList l₁ = String.ofList l₂ → l₁ = l₂
-- Mathlib.Topology.Order.LiminfLimsup
isBounded_le_nhds : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedLENhdsClass α] (a : α),
  Filter.IsBounded (fun x1 x2 => x1 ≤ x2) (nhds a)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (J : Type) [Finite J]
  [CategoryTheory.Limits.HasFiniteWidePullbacks C],
  CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
ComplexShape.Embedding.instFullHomotopyCategoryExtendHomotopyFunctor : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsRelIff]
  (C : Type u_3) [inst_1 : CategoryTheory.Category.{v_1, u_3} C] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Preadditive C], (e.extendHomotopyFunctor C).Full
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
GromovHausdorff.HD_below_aux1 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.Cb✝ X Y} (C : ℝ)
  {x : X}, BddBelow (Set.range fun y => f (Sum.inl x, Sum.inr y) + C)
-- Mathlib.RingTheory.Filtration
/-- **Krull's intersection theorem** for Noetherian local rings.  -/
Ideal.iInf_pow_eq_bot_of_isLocalRing : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [IsNoetherianRing R] [IsLocalRing R], I ≠ ⊤ → ⨅ i, I ^ i = ⊥
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRank_le_iff : ∀ {α : Type u} {M : Matroid α} {κ : Cardinal.{u}}, M.cRank ≤ κ ↔ ∀ ⦃B : Set α⦄, M.IsBase B → Cardinal.mk ↑B ≤ κ
-- Init.Data.SInt.Basic
/-- Converts an 8-bit signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.toInt : Int8 → ℤ
-- Mathlib.CategoryTheory.MorphismProperty.Ind
/-- If `P` ind-spreads and all under categories are finitely accessible, `ind P`
is multiplicative if `P` is.  -/
CategoryTheory.MorphismProperty.IsMultiplicative.ind_of_preIndSpreads : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [∀ (X : C), CategoryTheory.IsFinitelyAccessibleCategory (CategoryTheory.Under X)]
  [CategoryTheory.Limits.HasPushouts C] [P.IsMultiplicative] [P.IsStableUnderCobaseChange] [P.PreIndSpreads],
  P ≤ CategoryTheory.MorphismProperty.isFinitelyPresentable C → P.ind.IsMultiplicative
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (y : α) → (ys : List α) → motive (y :: ys)),
  (match [] with
    | [] => h_1 ()
    | y :: ys => h_2 y ys) =
    h_1 ()
-- Mathlib.Logic.Equiv.Prod
Equiv.prodPUnit_symm_apply : ∀ (α : Type u_9) (a : α), (Equiv.prodPUnit α).symm a = (a, PUnit.unit)
-- Mathlib.Topology.Compactness.SigmaCompact
/-- In a σ-compact space, `Set.univ` is a σ-compact set.  -/
SigmaCompactSpace.isSigmaCompact_univ : ∀ {X : Type u_4} {inst : TopologicalSpace X} [self : SigmaCompactSpace X], IsSigmaCompact Set.univ
-- Init.Data.Array.Lemmas
Array.flatMap_append : ∀ {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : α → Array β},
  Array.flatMap f (xs ++ ys) = Array.flatMap f xs ++ Array.flatMap f ys
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCoconeEquiv_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ},
  CategoryTheory.Limits.coneUnopOfCoconeEquiv.counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeUnop c),
            map := fun {Y X} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun c => CategoryTheory.Limits.coneUnopOfCocone (Opposite.unop c),
          map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
-- Mathlib.Data.Set.Card
Set.ncard_le_one : ∀ {α : Type u_1} {s : Set α}, autoParam s.Finite Set.ncard_le_one._auto_1 → (s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.Quotient.smul_mk : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : Monoid X] [inst_2 : MulAction X G] (H : Subgroup G)
  [inst_3 : MulAction.QuotientAction X H] (b : X) (g : G), b • ↑g = ↑(b • g)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.continuousOn_arg : ContinuousOn Complex.arg Complex.slitPlane
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The bare function of an `AddGroupSeminorm`.  -/
AddGroupSeminorm.toFun : {G : Type u_6} → [inst : AddGroup G] → AddGroupSeminorm G → G → ℝ
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.ext_iff : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} {f g : A.Copy B}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Logic.Equiv.Set
/-- If sets `s` and `t` are disjoint, then `s ∪ t` is equivalent to `s ⊕ t`.  -/
Equiv.Set.union : {α : Type u_3} → {s t : Set α} → [DecidablePred fun x => x ∈ s] → Disjoint s t → ↑(s ∪ t) ≃ ↑s ⊕ ↑t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.ext : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L}, (∀ (x : X), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_zero : NNReal.sqrt 0 = 0
-- Mathlib.Order.Basic
/-- **Alias** of `le_of_lt`. -/
LT.lt.le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → a ≤ b
-- Lean.DocString.Types
Lean.Doc.Block.code.injEq : ∀ {i : Type u} {b : Type v} (content content_1 : String),
  (Lean.Doc.Block.code content = Lean.Doc.Block.code content_1) = (content = content_1)
-- Lean.Elab.App
/-- The elaborated application so far, with applied arguments.  -/
Lean.Elab.Term.ElabAppArgs.State.f : Lean.Elab.Term.ElabAppArgs.State → Lean.Expr
-- Lean.Meta.CoeAttr
/-- The argument index that represents the value being coerced  -/
Lean.Meta.CoeFnInfo.coercee : Lean.Meta.CoeFnInfo → ℕ
-- Mathlib.Topology.Algebra.LinearTopology
/-- A variant of `IsLinearTopology.hasBasis_subbimodule` using `IsOpen I` instead of `I ∈ 𝓝 0`.  -/
IsLinearTopology.hasBasis_open_subbimodule : ∀ (R : Type u_1) (R' : Type u_2) {M : Type u_3} [inst : Ring R] [inst_1 : Ring R'] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module R' M] [SMulCommClass R R' M] [inst_6 : TopologicalSpace M] [ContinuousAdd M]
  [IsLinearTopology R M] [IsLinearTopology R' M],
  (nhds 0).HasBasis (fun I => IsOpen ↑I ∧ (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I) fun I =>
    ↑I
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.mul_const_inv : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (x * a⁻¹)) (c * a)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter_singleton_mem_affineSpan_range : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), s.excenter {i} ∈ affineSpan ℝ (Set.range s.points)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.nonemptyTheory.eq_1 : ∀ (L : FirstOrder.Language), L.nonemptyTheory = {FirstOrder.Language.Sentence.cardGe L 1}
-- Mathlib.Topology.Constructions
ULift.topologicalSpace.eq_1 : ∀ {X : Type u} [t : TopologicalSpace X], ULift.topologicalSpace = TopologicalSpace.induced ULift.down t
-- Mathlib.Order.Filter.Pointwise
Filter.pure_add_pure : ∀ {α : Type u_2} [inst : Add α] {a b : α}, pure a + pure b = pure (a + b)
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instPreservesEffectiveEpisComp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesEffectiveEpis]
  [G.PreservesEffectiveEpis], (F.comp G).PreservesEffectiveEpis
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Monadic fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
 -/
Batteries.BinomialHeap.Imp.Heap.foldM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} → [Monad m] → (α → α → Bool) → Batteries.BinomialHeap.Imp.Heap α → β → (β → α → m β) → m β
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `Matrix.toQuadraticForm'`.

---

`M.toQuadraticForm'` is the map `fun x ↦ row x * M * col x` as a quadratic form on `n → R`.  -/
Matrix.toQuadraticMap' : {R : Type u_3} →
  {n : Type w} → [Fintype n] → [DecidableEq n] → [inst : CommRing R] → Matrix n n R → QuadraticForm R (n → R)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_one : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LinearMap.toMatrix' 1 = 1
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.instFiniteSubtypeMemSubmoduleRootSpanOfFinite : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Module S M] [Finite ι], Module.Finite S ↥(P.rootSpan S)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.coeff_ne_zero_of_eq_degree : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.degree = ↑n → p.coeff n ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.hd : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (self : SSet.prodStdSimplex.pairingCore.Type₁ k n), self.x.dim = self.d + 1
-- Lean.Environment
Lean.Kernel.Diagnostics.mk.inj : ∀ {unfoldCounter : Lean.PHashMap Lean.Name ℕ} {enabled : Bool} {unfoldCounter_1 : Lean.PHashMap Lean.Name ℕ}
  {enabled_1 : Bool},
  { unfoldCounter := unfoldCounter, enabled := enabled } = { unfoldCounter := unfoldCounter_1, enabled := enabled_1 } →
    unfoldCounter = unfoldCounter_1 ∧ enabled = enabled_1
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Summable.div_const : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α}, Summable f L → ∀ (b : α), Summable (fun i => f i / b) L
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_inter_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict₂`.

---

If a function `f` is restricted to a set `t`, and `s ⊆ t`, this is the restriction to `s`.  -/
Set.restrict₂ : {α : Type u_1} → {π : α → Type u_6} → {s t : Set α} → s ⊆ t → ((a : ↑t) → π ↑a) → (a : ↑s) → π ↑a
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
CompactConvergenceCLM.continuousSMul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [RingHomSurjective σ] [RingHomIsometric σ] [inst_8 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [inst_10 : TopologicalSpace F] [inst_11 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E]
  [inst_13 : ContinuousSMul 𝕜₂ F], ContinuousSMul 𝕜₂ (CompactConvergenceCLM σ E F)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
IsometryEquiv.dimH_preimage : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] (e : X ≃ᵢ Y) (s : Set Y),
  dimH (⇑e ⁻¹' s) = dimH s
-- Mathlib.Logic.Equiv.Basic
/-- If two predicates are equal, then the corresponding subtypes are equivalent.  -/
Equiv.subtypeEquivProp : {α : Sort u_1} → {p q : α → Prop} → p = q → Subtype p ≃ Subtype q
-- Mathlib.Data.List.AList
/-- There are no duplicate keys in `entries`  -/
AList.nodupKeys : ∀ {α : Type u} {β : α → Type v} (self : AList β), self.entries.NodupKeys
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [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} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  [inst_4 :
    ∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
      ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  (X₂ : CategoryTheory.GradedObject I₂ C₂) {x x_1 : CategoryTheory.GradedObject I₃ C₃} (φ : x ⟶ x_1) (i : J),
  ((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).obj X₂).map φ i =
    CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁)
      (CategoryTheory.CategoryStruct.id X₂) φ i
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.π.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  HomologicalComplex.cylinder.π K =
    HomologicalComplex.cylinder.desc (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id K)
      (Homotopy.refl (CategoryTheory.CategoryStruct.id K))
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- We say that a functor creates finite limits if it creates all limits of shape `J` where
`J : Type` is a finite category.  -/
CategoryTheory.Limits.CreatesFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → Type (max (max (max (max 1 u₁) u₂) v₁) v₂)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.genLoopGenLoopEquiv_apply_coe : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X)
  (p : ↑(GenLoop M (↑(GenLoop N X x)) GenLoop.const)),
  ↑((GenLoop.genLoopGenLoopEquiv x) p) =
    (GenLoop.uncurry x p).comp { toFun := Homeomorph.sumArrowHomeomorphProdArrow.toFun, continuous_toFun := ⋯ }
-- Mathlib.RingTheory.Ideal.Basic
Ideal.pi_span : ∀ {ι : Type u_1} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] {r : (i : ι) → R i},
  (Ideal.pi fun x => Ideal.span {r x}) = Ideal.span {r}
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isInt_emod : ∀ {a b q m a' : ℤ} {b' r : ℕ},
  Mathlib.Meta.NormNum.IsInt a a' →
    Mathlib.Meta.NormNum.IsNat b b' → q * ↑b' = m → ↑r + m = a' → r.blt b' = true → Mathlib.Meta.NormNum.IsNat (a % b) r
-- Lean.Elab.App
Lean.Elab.Term.elabExplicit : Lean.Elab.Term.TermElab
-- Std.Data.HashMap.Raw
/-- Removes all mappings of the hash map for which the given function returns `false`.  -/
Std.HashMap.Raw.filter : {α : Type u} → {β : Type v} → (α → β → Bool) → Std.HashMap.Raw α β → Std.HashMap.Raw α β
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.counitAppAppImage.eq_1 : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))}
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}]
  (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) (a : Function.Fiber ⇑f),
  CompHausLike.LocallyConstant.counitAppAppImage f a =
    (CategoryTheory.ConcreteCategory.hom
        (Y.map (CompHausLike.isTerminalPUnit.from (CompHausLike.LocallyConstant.fiber f a)).op))
      (Function.Fiber.image (⇑f) a)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
MeasureTheory.taylorWithinEval_charFun_zero : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ},
  MeasureTheory.MemLp id (↑n) μ →
    ∀ (t : ℝ),
      taylorWithinEval (MeasureTheory.charFun μ) n Set.univ 0 t =
        ∑ k ∈ Finset.range (n + 1), (↑k.factorial)⁻¹ * (↑t * Complex.I) ^ k * ↑(∫ (x : ℝ), x ^ k ∂μ)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'