mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Hom
Function.Surjective.mulActionLeft.eq_1 : ∀ {R : Type u_4} {S : Type u_5} {M : Type u_6} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : Monoid S]
  [inst_3 : SMul S M] (f : R →* S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x),
  Function.Surjective.mulActionLeft f hf hsmul = { toSMul := inst_3, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Basic
mul_left_surjective₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → Function.Surjective fun g => a * g
-- Init.Data.Fin.Lemmas
Fin.exists_fin_two : ∀ {p : Fin 2 → Prop}, (∃ i, p i) ↔ p 0 ∨ p 1
-- Mathlib.Data.Set.Prod
Set.prod_univ_range_eq : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m₂ : β → δ}, Set.univ ×ˢ Set.range m₂ = Set.range fun p => (p.1, m₂ p.2)
-- Mathlib.RingTheory.Finiteness.Finsupp
/-- If 0 → M' → M → M'' → 0 is exact and M' and M'' are
finitely generated then so is M.  -/
Submodule.fg_of_fg_map_of_fg_inf_ker : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup P] [inst_4 : Module R P] (f : M →ₗ[R] P) {s : Submodule R M},
  (Submodule.map f s).FG → (s ⊓ f.ker).FG → s.FG
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforwardIsoBind_hom_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X)
  (i : (CategoryTheory.PreZeroHypercover.pushforward f E).I₀),
  (CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).hom.h₀ i = CategoryTheory.CategoryStruct.id (E.X i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.mulEquivCongrRight.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsMonHom e.hom] (X : C),
  CategoryTheory.Hom.mulEquivCongrRight e X =
    ((CategoryTheory.yonedaMon.mapIso (CategoryTheory.Mon.mkIso' e)).app (Opposite.op X)).monCatIsoToMulEquiv
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorZero'_hom_app_f : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ) (h : n = 0)
  (X : CochainComplex C ℤ) (i : ℤ),
  ((CochainComplex.shiftFunctorZero' C n h).hom.app X).f i = (HomologicalComplex.XIsoOfEq X ⋯).hom
-- Mathlib.Algebra.BigOperators.Finprod
finsum_neg_distrib : ∀ {G : Type u_1} {α : Sort u_4} [inst : SubtractionCommMonoid G] (f : α → G), ∑ᶠ (x : α), -f x = -∑ᶠ (x : α), f x
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- **Alias** of `OrderIso.cof_congr`. -/
OrderIso.cof_eq : ∀ {α γ : Type u} [inst : Preorder α] [inst_1 : Preorder γ] (f : α ≃o γ), Order.cof α = Order.cof γ
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- The sheafification of a presheaf `P`.
*NOTE:* Additional hypotheses are needed to obtain a proof that this is a sheaf!  -/
CategoryTheory.GrothendieckTopology.sheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              CategoryTheory.Functor Cᵒᵖ D → CategoryTheory.Functor Cᵒᵖ D
-- Mathlib.Order.Category.Semilat
SemilatInfCat.isSemilatticeInf : (self : SemilatInfCat) → SemilatticeInf self.X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.pi_div_two_pos : 0 < Real.pi / 2
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_self_eq_variance : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (L : StrongDual ℝ E), ((ProbabilityTheory.covarianceBilinDual μ) L) L = ProbabilityTheory.variance (⇑L) μ
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.two_le_natDegree_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B],
  IsIntegral A x → (2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_mul : ∀ {R : Type u} {M : Type v} [inst : Mul R] [inst_1 : Add M] [inst_2 : SMul R M] [inst_3 : SMul Rᵐᵒᵖ M]
  (x₁ x₂ : TrivSqZeroExt R M), (x₁ * x₂).fst = x₁.fst * x₂.fst
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.AwaitRefreshParams.mk.injEq : ∀ (state : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef) (oldIdx : ℕ)
  (state_1 : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef) (oldIdx_1 : ℕ),
  ({ state := state, oldIdx := oldIdx } = { state := state_1, oldIdx := oldIdx_1 }) =
    (state = state_1 ∧ oldIdx = oldIdx_1)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ : Finset α), s₁ \ s₁ = ∅
-- Mathlib.Algebra.Group.Defs
/-- Commutative `SubtractionMonoid`.  -/
SubtractionCommMonoid : Type u → Type u
-- Mathlib.Order.Concept
/-- The extent of a concept.  -/
Concept.extent : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → Concept α β r → Set α
-- Init.Grind.Lemmas
Lean.Grind.of_eq_eq_true : ∀ {a b : Prop}, (a = b) = True → a ∧ b ∨ ¬a ∧ ¬b
-- Mathlib.Analysis.Meromorphic.Order
/-- The order is additive when multiplying meromorphic functions.  -/
meromorphicOrderAt_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'},
  MeromorphicAt f x → MeromorphicAt g x → meromorphicOrderAt (f * g) x = meromorphicOrderAt f x + meromorphicOrderAt g x
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.smul_infty_eq_ite : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] (g : GL (Fin 2) K),
  g • OnePoint.infty = if ↑g 1 0 = 0 then OnePoint.infty else ↑(↑g 0 0 / ↑g 1 0)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fundamentalDomain_measurableSet : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι], MeasurableSet (ZSpan.fundamentalDomain b)
-- Init.Data.Vector.Lemmas
Vector.swap_swap : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (hi : i < n) (hj : j < n), (xs.swap i j hi hj).swap i j hi hj = xs
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.neg : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J RingCat} → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
an arrow `i` with `i + 1 > j` can be identified with arrow `i + 1` in the
original path.  -/
SSet.Truncated.StrictSegal.spine_δ_arrow_gt : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) {i : Fin m}
  {j : Fin (m + 2)},
  j < i.succ.castSucc →
    (X.spine m ⋯
            ((CategoryTheory.ConcreteCategory.hom
                (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op))
              (sx.spineToSimplex (m + 1) ⋯ f))).arrow
        i =
      f.arrow i.succ
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.eval_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h : C}
  {η η' : f ⟶ g}
  {θ : CategoryTheory.MonoidalCategoryStruct.tensorObj f h ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g h},
  η = η' →
    CategoryTheory.MonoidalCategoryStruct.whiskerRight η' h = θ →
      CategoryTheory.MonoidalCategoryStruct.whiskerRight η h = θ
-- Init.Data.Array.Find
/-- If `¬ p xs[j]` for all `j ≤ i`, then `i < xs.findIdx p`.  -/
Array.lt_findIdx_of_not : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {i : ℕ} (h : i < xs.size),
  (∀ (j : ℕ) (hji : j ≤ i), ¬p xs[j] = true) → i < Array.findIdx p xs
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)],
      (m₁.inter m₂ ⋯).get! k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.get! k else default
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.smul_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {M : Type u_7}
  [inst_6 : Monoid M] [inst_7 : DistribMulAction M F] [inst_8 : SMulCommClass S M F] (a : M) (f : E →ₛₗ.[σ] F)
  (x : ↥(a • f).domain), ↑(a • f) x = a • ↑f x
-- Mathlib.Topology.Constructions
OrderDual.instTopologicalSpace : {X : Type u} → [TopologicalSpace X] → TopologicalSpace Xᵒᵈ
-- Mathlib.Order.Monotone.Defs
Function.Injective.of_lt_imp_ne : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] {f : α → β}, (∀ (x y : α), x < y → f x ≠ f y) → Function.Injective f
-- Aesop.Options.Internal
Aesop.Options'.forwardMaxDepth? : Aesop.Options' → Option ℕ
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G),
  (P.coconePointsIsoOfNatIso Q w).inv = Q.map s w.inv
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.coe_reindexRingEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : Mul R]
  [inst_3 : AddCommMonoid R] (e : m ≃ n), ⇑(Matrix.reindexRingEquiv R e) = ⇑(Matrix.reindex e e)
-- Mathlib.Topology.UniformSpace.Basic
/-- If `s ∈ 𝓤 α`, then for a subset `t` of a sufficiently small set in `𝓤 α`,
we have `t ○ t ⊆ s`.  -/
eventually_uniformity_comp_subset : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α},
  s ∈ uniformity α → ∀ᶠ (t : SetRel α α) in (uniformity α).smallSets, t.comp t ⊆ s
-- Lean.Meta.LetToHave
/-- Give an expression `e` whose definition may be used in an unknown manner (for example, through a metavariable),
marks all fvars in `e` (or accessible through `e`) that can potentially be unfolded.

Assumption: while there may be metavariables in `e` (or in types of fvars present in `e`),
they have already been processed by `checkMVar` or will be processed by it.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitDepExpr : Lean.Expr → Lean.Meta.LetToHave.M✝ Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.Pairing.rank'_lt : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {y : ↑P.II} (hy : Acc P.AncestralRel y) {x : ↑P.II}
  (r : P.AncestralRel x y), P.rank' ⋯ < P.rank' hy
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a `CommMonoid` under pointwise operations if `α` is.  -/
Finset.commMonoid : {α : Type u_2} → [DecidableEq α] → [CommMonoid α] → CommMonoid (Finset α)
-- Lean.Widget.InteractiveGoal
/-- The symbol to display before the target type. Usually `⊢ ` but `conv` goals use `∣ `
and it could be extended.  -/
Lean.Widget.InteractiveGoal.goalPrefix : Lean.Widget.InteractiveGoal → String
-- Lean.Data.Json.FromToJson.Basic
Lean.Option.fromJson? : {α : Type u_1} → [Lean.FromJson α] → Lean.Json → Except String (Option α)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil.hcongr_8 : ∀ (V V' : Type u),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' →
        ∀ (inst : DecidableEq V) (inst' : DecidableEq V'),
          inst ≍ inst' →
            ∀ (v : V) (v' : V'),
              v ≍ v' →
                ∀ (w : V) (w' : V'),
                  w ≍ w' →
                    ∀ (p : G.Walk v w) (p' : G'.Walk v' w'),
                      p ≍ p' →
                        ∀ (u : V) (u' : V'),
                          u ≍ u' →
                            ∀ (a : u ∈ p.support) (a' : u' ∈ p'.support), a ≍ a' → p.takeUntil u a ≍ p'.takeUntil u' a'
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rio.count_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α] {r : Std.Rio α},
  r.iter.length = r.size
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.associator_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.Pseudofunctor B C} (I : CategoryTheory.Pseudofunctor B C) (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I)
  (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.bicomp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : α → β} {s : Set α} {a : α} [inst_3 : Preorder δ] {op : β → γ → δ},
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) op op →
    IsLocalMinOn f s a → ∀ {g : α → γ}, IsLocalMinOn g s a → IsLocalMinOn (fun x => op (f x) (g x)) s a
-- Mathlib.GroupTheory.OreLocalization.Cardinality
OreLocalization.oreDiv_one_surjective_of_finite_right : ∀ {R : Type u} [inst : Monoid R] (S : Submonoid R) [inst_1 : OreLocalization.OreSet S] (X : Type v)
  [inst_2 : MulAction R X] [Finite X], Function.Surjective fun x => x /ₒ 1
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_isLoop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {D : Set α}, (M.delete D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.toSplittingField.eq_1 : ∀ {k : Type u} [inst : Field k] (s : Finset (AlgebraicClosure.Monics k)),
  AlgebraicClosure.toSplittingField s =
    MvPolynomial.aeval fun fi => if hf : fi.fst ∈ s then (↑((AlgebraicClosure.finEquivRoots ⋯) fi.snd)).1 else 37
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.lift_symm_apply : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] (b : FreeAddGroupBasis ι G)
  (a : G →+ H) (a_1 : ι), b.lift.symm a a_1 = a (b.repr.symm (FreeAddGroup.of a_1))
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_pos_of_pos_of_le_two : ∀ {x : ℝ}, 0 < x → x ≤ 2 → 0 < Real.sin x
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.Config.mk.sizeOf_spec : ∀ (maxDepth : ℕ) (abstract debug : Bool),
  sizeOf { maxDepth := maxDepth, abstract := abstract, debug := debug } =
    1 + sizeOf maxDepth + sizeOf abstract + sizeOf debug
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.involutive_symplComp : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H],
  Function.Involutive StandardSubspace.symplComp
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.singleton_inter_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∈ s → {a} ∩ s = {a}
-- Mathlib.Topology.Homeomorph.Defs
/-- Homeomorphism between `X` and `Y`, also called topological isomorphism  -/
Homeomorph : (X : Type u_5) → (Y : Type u_6) → [TopologicalSpace X] → [TopologicalSpace Y] → Type (max u_5 u_6)
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.Integrable.const_inner : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {f : α → E} (c : E),
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => inner 𝕜 c (f x)) μ
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofNat' : ∀ (n : ℕ), (USize.ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n
-- Aesop.Forward.State.ApplyGoalDiff
/-- Apply a goal diff to the state, adding and removing hypotheses as indicated
by the diff.  -/
Aesop.ForwardState.applyGoalDiff : Aesop.LocalRuleSet → Aesop.GoalDiff → Aesop.ForwardState → Aesop.BaseM Aesop.ForwardState
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.multiset_prod_comp : ∀ {R : Type u} [inst : CommSemiring R] (s : Multiset (Polynomial R)) (q : Polynomial R),
  s.prod.comp q = (Multiset.map (fun p => p.comp q) s).prod
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.NoetherianSpace.iUnion : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_3} (f : ι → Set α) [Finite ι]
  [hf : ∀ (i : ι), TopologicalSpace.NoetherianSpace ↑(f i)], TopologicalSpace.NoetherianSpace ↑(⋃ i, f i)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyMap'_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.rightHomologyMap' (φ - φ') h₁ h₂ =
    CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ - CategoryTheory.ShortComplex.rightHomologyMap' φ' h₁ h₂
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_sSup_of_directedOn : ∀ {R : Type u} [inst : NonAssocSemiring R] {S : Set (Subsemiring R)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : R}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.CheckCoverageResult.missing.sizeOf_spec : ∀ (pos : List ℕ), sizeOf (Lean.Meta.Grind.CheckCoverageResult.missing pos) = 1 + sizeOf pos
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.decode.eq_def : ∀ (n : ℕ),
  Mathlib.Deriving.Encodable.S.decode✝ n =
    let p := Nat.unpair n;
    if h : p.1 = 0 then Mathlib.Deriving.Encodable.S.nat✝ p.2
    else
      have this := ⋯;
      have this := ⋯;
      have this := ⋯;
      Mathlib.Deriving.Encodable.S.cons✝ (Mathlib.Deriving.Encodable.S.decode✝ (p.1 - 1))
        (Mathlib.Deriving.Encodable.S.decode✝ p.2)
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.Total.mk : {V : Type u} → [inst : Quiver V] → (left right : V) → (left ⟶ right) → Quiver.Total V
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.map₀_def : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [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 ι] [inst_4 : Nonempty ι]
  (ih : (i : ι) → F i),
  (∀ (i j : ι) (h : i ≤ j), (f i j h) (ih i) = ih j) → ∀ (i : ι), DirectLimit.map₀ f ih = ⟦⟨i, ih i⟩⟧
-- Mathlib.FieldTheory.SeparableDegree
/-- If `x` is a separable elements, then `-x` is also a separable element.  -/
Field.isSeparable_neg : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  IsSeparable F x → IsSeparable F (-x)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Producer.chunk : Std.Http.Body.Channel.Producer✝ → Std.Http.Chunk
-- Mathlib.RingTheory.KrullDimension.Polynomial
/-- Let `p` be a maximal ideal of `R`. Then the height of `p[X]` equals the height of `p`.  -/
Polynomial.height_map_C : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsMaximal],
  (Ideal.map Polynomial.C p).height = p.height
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- If a function is `r`-Hölder over a bounded set, then it is also `s`-Hölder over this set
when `s ≤ r`. See `HolderOnWith.exists_holderOnWith_of_le'`
for the version in a pseudoemetric space.  -/
HolderOnWith.exists_holderOnWith_of_le : ∀ {Y : Type u_2} [inst : PseudoEMetricSpace Y] {r : NNReal} {X : Type u_3} [inst_1 : PseudoMetricSpace X] {f : X → Y}
  {s : NNReal} {A : Set X}, (∃ C, HolderOnWith C r f A) → s ≤ r → Bornology.IsBounded A → ∃ C, HolderOnWith C s f A
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.leadingCoeff 1 = 1
-- Mathlib.Data.Int.CardIntervalMod
Int.Ico_filter_modEq_eq : ∀ (a b : ℤ) {r : ℤ} (v : ℤ),
  {x ∈ Finset.Ico a b | x ≡ v [ZMOD r]} =
    Finset.map { toFun := fun x => x + v, inj' := ⋯ } ({x ∈ Finset.Ico (a - v) (b - v) | r ∣ x})
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  (x : CategoryTheory.Limits.WalkingParallelPair),
  (I.parallelPairDiagramOfIsLimit c hd).obj x = CategoryTheory.Limits.parallelPair.parallelPairObj c.pt d.pt x
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- If `G` is isomorphic to `H`, then `G` is contained in `H`.  -/
SimpleGraph.Iso.isContained : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H), G.IsContained H
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.eventuallyEq_one : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M)
  (hx : x ∈ s), ↑(fs.toFun (fs.ind x hx)) =ᶠ[nhds x] 1
-- Init.Data.Array.Attach
Array.filterMap_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Option β}
  {g : α → Option β}, (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Array.filterMap f xs = Array.filterMap g xs.unattach
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertMany_list_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ : Std.DTreeMap.Raw α (fun x => β) cmp} {l : List (α × β)},
  (Std.DTreeMap.Raw.Const.insertMany t₁ l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) t₁ l)
-- Init.Data.UInt.Lemmas
USize.lt_or_lt_of_ne : ∀ {a b : USize}, a ≠ b → a < b ∨ b < a
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_dvd_of_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, n • x = 0 → addOrderOf x ∣ n
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.isUniformEmbedding_singleton : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformEmbedding fun x => {x}
-- Mathlib.RingTheory.Algebraic.Defs
/-- An algebra is algebraic if and only if it is algebraic as a subalgebra.  -/
Algebra.isAlgebraic_iff : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  Algebra.IsAlgebraic R A ↔ ⊤.IsAlgebraic
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.alter.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (a : α) →
      (motive : Option (β a) → Sort u_2) →
        (x : Option (β a)) → (Unit → motive none) → ((b : β a) → motive (some b)) → motive x
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.exists_mem_splitCenterBox : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι → ℝ}, (∃ s, x ∈ I.splitCenterBox s) ↔ x ∈ I
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instIsSubApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsSubApply (CuspForm Γ k) UpperHalfPlane ℂ