mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
/-- If `F` is a `J`-sheaf, then being a sheaf for a presieve `R` is `J`-local on the target, i.e.
it can be checked on the pullbacks from a `1`-hypercover.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_of_pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  {E : J.OneHypercover X} {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)},
  CategoryTheory.Presieve.IsSheaf J F →
    ∀ {R : CategoryTheory.Presieve X},
      (∀ (i : E.I₀),
          CategoryTheory.Presieve.IsSheafFor F
            (CategoryTheory.Sieve.pullback (E.f i) (CategoryTheory.Sieve.generate R)).arrows) →
        (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
            CategoryTheory.Presieve.IsSeparatedFor F
              (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
                  (CategoryTheory.Sieve.generate R)).arrows) →
          CategoryTheory.Presieve.IsSheafFor F R
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.copyCount_of_isEmpty : ∀ {V : Type u_1} {W : Type u_2} [inst : Fintype V] [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W),
  G.copyCount H = 1
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- The tensor product of two bilinear maps injects into bilinear maps on tensor products.

Note this is heterobasic; the bilinear map on the left can take values in a module over a
(commutative) algebra over the ring of the module in which the right bilinear map is valued.  -/
LinearMap.BilinMap.tensorDistrib : (R : Type uR) →
  (A : Type uA) →
    {M₁ : Type uM₁} →
      {M₂ : Type uM₂} →
        {N₁ : Type uN₁} →
          {N₂ : Type uN₂} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring A] →
                [inst_2 : AddCommMonoid M₁] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : AddCommMonoid N₁] →
                      [inst_5 : AddCommMonoid N₂] →
                        [inst_6 : Algebra R A] →
                          [inst_7 : Module R M₁] →
                            [inst_8 : Module A M₁] →
                              [inst_9 : Module R N₁] →
                                [inst_10 : Module A N₁] →
                                  [inst_11 : SMulCommClass R A M₁] →
                                    [IsScalarTower R A M₁] →
                                      [inst_13 : SMulCommClass R A N₁] →
                                        [inst_14 : IsScalarTower R A N₁] →
                                          [inst_15 : Module R M₂] →
                                            [inst_16 : Module R N₂] →
                                              TensorProduct R (LinearMap.BilinMap A M₁ N₁)
                                                  (LinearMap.BilinMap R M₂ N₂) →ₗ[A]
                                                LinearMap.BilinMap A (TensorProduct R M₁ M₂) (TensorProduct R N₁ N₂)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k k' : α} {v : β},
      List.find? (fun a => a.1 == k) (Std.DHashMap.Raw.Const.toList m) = some (k', v) ↔
        m.getKey? k = some k' ∧ Std.DHashMap.Raw.Const.get? m k = some v
-- Mathlib.Topology.FiberBundle.Trivialization
/-- If `e` is a `Trivialization` of `proj : Z → B` with fiber `F` and `h` is a homeomorphism
`F ≃ₜ F'`, then `e.trans_fiber_homeomorph h` is the trivialization of `proj` with the fiber `F'`
that sends `p : Z` to `((e p).1, h (e p).2)`.  -/
Bundle.Trivialization.transFiberHomeomorph : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              {F' : Type u_5} →
                [inst_3 : TopologicalSpace F'] → Bundle.Trivialization F proj → F ≃ₜ F' → Bundle.Trivialization F' proj
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.surjective_snd_prod : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂), Function.Surjective ⇑((LieHom.snd R L₁ L₂).comp (LieAlgebra.Basis.prod✝ eι b₁ b₂).incl)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Module.Basis.equivFunL_symm_apply_repr : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E]
  [inst_5 : CompleteSpace 𝕜] {ι : Type u_1} [inst_6 : Finite ι] [inst_7 : T2Space E] (v : Module.Basis ι 𝕜 E) (x : E),
  v.equivFunL.symm ⇑(v.repr x) = x
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.l_hom_inv : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.CategoryTheory.Sites.Abelian
CategoryTheory.instAdditiveFunctorOppositeConst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 : CategoryTheory.Abelian D], (CategoryTheory.Functor.const Cᵒᵖ).Additive
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
bddBelow_neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G},
  BddBelow (-s) ↔ BddAbove s
-- Mathlib.Logic.Function.Defs
Function.diag_apply : ∀ {α : Type u_1} (a : α), Function.diag a = (a, a)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.one_hadamard_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α], Matrix.hadamard 1 (SimpleGraph.adjMatrix α G) = 0
-- Init.Data.Range.Polymorphic.PRange
/-- This type class allows taking the intersection of a left-closed right-unbounded range with a
left-closed right-open range, resulting in another left-closed right-open range.
 -/
Std.Rci.HasRcoIntersection : Type w → Type w
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.IterM.step_drop.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {fallback : α}
  {hc : t.minKeyD fallback ∈ t}, t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback
-- Mathlib.Algebra.Order.Module.Defs
smul_le_smul' : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [inst_4 : Zero β] [PosSMulMono α β] [SMulPosMono α β],
  a₁ ≤ a₂ → b₁ ≤ b₂ → 0 ≤ a₂ → 0 ≤ b₁ → a₁ • b₁ ≤ a₂ • b₂
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instMulAction.eq_1 : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : Monoid K] [inst_1 : MulAction K V],
  WithLp.instMulAction p K V = { toSMul := WithLp.instSMul p K V, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.PreservesEqualizer.iso_inv_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasEqualizer f g]
  [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesEqualizer.iso G f g).inv
      (G.map (CategoryTheory.Limits.equalizer.ι f g)) =
    CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.getEntryGT?.go : {α : Type u} →
  {β : α → Type v} → [Ord α] → α → Option ((a : α) × β a) → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Lean.Elab.AssertExists
/-- `getSortedAssertExists env` returns the array of `AssertExists`, placing first all declarations,
in alphabetical order, and then all modules, also in alphabetical order.  -/
Lean.Elab.Command.getSortedAssertExists : Lean.Environment → Array Lean.Elab.Command.AssertExists
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.get?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.get? k = m₂.get? k
-- Init.Data.List.Basic
List.nil_lex_nil : ∀ {α : Type u} {lt : α → α → Bool} [inst : BEq α], [].lex [] lt = false
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst)
            (𝒰.X i.fst).affineCover).f
        i.snd)
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_add : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α] (M N : Matrix m n α),
  (M + N).transpose = M.transpose + N.transpose
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- The minimum degree of all vertices in a nontrivial tree is one.  -/
SimpleGraph.IsTree.minDegree_eq_one_of_nontrivial : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsTree → ∀ [inst : Fintype V] [Nontrivial V] [inst_2 : DecidableRel G.Adj], G.minDegree = 1
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap_f_of_not_rel_right : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι},
  c.Rel k₁ k₀ →
    (∀ (l : ι), ¬c.Rel l k₁) →
      ∀ (hom : (i j : ι) → C.X i ⟶ D.X j),
        (Homotopy.nullHomotopicMap hom).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (hom k₀ k₁)
-- Mathlib.Data.Fin.SuccPred
/-- Sending `Fin (n+1)` to `Fin n` by subtracting one from anything above `p`
then back to `Fin (n+1)` with a gap around `p` is the identity away from `p`.  -/
Fin.succAbove_predAbove : ∀ {n : ℕ} {p : Fin n} {i : Fin (n + 1)}, i ≠ p.castSucc → p.castSucc.succAbove (p.predAbove i) = i
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_terminates_iff : ∀ {α : Type u} (s : Stream'.WSeq α), s.head.Terminates ↔ s.destruct.Terminates
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgEquiv_apply : ∀ (σ : Type u_1) (R : Type u_3) {n : ℕ} [inst : Fintype σ] [inst_1 : CommRing R] (hn : Fintype.card σ = n)
  (a : MvPolynomial (Fin n) R), (MvPolynomial.esymmAlgEquiv σ R hn) a = (MvPolynomial.esymmAlgHom σ R n) a
-- Mathlib.Data.NNReal.Defs
/-- A scalar multiplication over `ℝ` restricts to a scalar multiplication over `ℝ≥0`.  -/
NNReal.instSMulOfReal : {M : Type u_1} → [SMul ℝ M] → SMul NNReal M
-- Mathlib.Algebra.Module.LinearMap.End
/-- See also `Module.End.intCast_def`.  -/
Module.End.intCast_apply : ∀ {R : Type u_1} {N₁ : Type u_8} [inst : Semiring R] [inst_1 : AddCommGroup N₁] [inst_2 : Module R N₁] (z : ℤ) (m : N₁),
  ↑z m = z • m
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB5OfSize_of_univLE : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w₂, w₂', v, u} C] [inst_2 : UnivLE.{w, w₂}]
  [inst_3 : UnivLE.{w', w₂'}] [CategoryTheory.AB5OfSize.{w₂, w₂', v, u} C], CategoryTheory.AB5OfSize.{w, w', v, u} C
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearMap_toAddMonoidHom : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] N), (Finsupp.mapRange.linearMap f).toAddMonoidHom = Finsupp.mapRange.addMonoidHom f.toAddMonoidHom
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.conjugate_coe_eq : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ) (x : K),
  (NumberField.ComplexEmbedding.conjugate φ) x = (starRingEnd ℂ) (φ x)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.isometry : ∀ {F : Type u_3} {α : outParam (Type u_4)} {β : outParam (Type u_5)} {inst : PseudoEMetricSpace α}
  {inst_1 : PseudoEMetricSpace β} {inst_2 : FunLike F α β} [self : IsometryClass F α β] (f : F), Isometry ⇑f
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- A splitting of a group extension as a (set-theoretic) section.  -/
GroupExtension.Splitting.toSection : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → {S : GroupExtension N E G} → S.Splitting → S.Section
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addRightMono : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [AddRightMono α], AddRightMono (WithBot α)
-- Std.Http.Data.Method
Std.Http.Method.ofNat : ℕ → Std.Http.Method
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_naturalityₗ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n m' : M}
  (f : m ⟶ m') (X : C) [inst_3 : F.LaxMonoidal] {Z : C}
  (h : (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m' n)).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.map f).app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m' n).app X) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f n)).app X) h)
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- Given a group acting freely and transitively, an equivalence between the orbits under the
action of a subgroup and the quotient of the group by the subgroup.  -/
MulAction.equivSubgroupOrbitsQuotientGroup : {G : Type u} →
  {X : Type v} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        X →
          [MulAction.IsPretransitive G X] →
            [IsCancelSMul G X] → (H : Subgroup G) → MulAction.orbitRel.Quotient (↥H) X ≃ G ⧸ H
-- Init.Data.List.Lemmas
List.replace_append : ∀ {α : Type u_1} [inst : BEq α] {a b : α} [inst_1 : LawfulBEq α] {l₁ l₂ : List α},
  (l₁ ++ l₂).replace a b = if a ∈ l₁ then l₁.replace a b ++ l₂ else l₁ ++ l₂.replace a b
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instNeg.eq_1 : ∀ {α : Type u} [inst : AddMonoid α],
  AddUnits.instNeg = { neg := fun u => { val := u.neg, neg := ↑u, val_neg := ⋯, neg_val := ⋯ } }
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.containsKey : {α : Type u} → {β : α → Type v} → [BEq α] → α → List ((a : α) × β a) → Bool
-- Mathlib.Topology.Algebra.Monoid
continuousMul_of_discreteTopology : ∀ {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Mul N] [DiscreteTopology N], ContinuousMul N
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, a ∈ m.erase k → a ∈ m
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
/-- Associator for the vertical composition of strong natural transformations
between pseudofunctors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.associator : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H I : CategoryTheory.Pseudofunctor B C} →
          (η : F ⟶ G) →
            (θ : G ⟶ H) →
              (ι : H ⟶ I) →
                CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp η θ) ι ≅
                  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp θ ι)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_sub : ∀ {R : Type u_1} [inst : CommRing R] (p q : Polynomial R) (n : ℕ),
  (p - q).homogenize n = p.homogenize n - q.homogenize n
-- Mathlib.GroupTheory.OrderOfElement
mod_addOrderOf_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] (x : G) (n : ℕ), (n % addOrderOf x) • x = n • x
-- Init.Data.UInt.Bitwise
UInt16.not_inj : ∀ {a b : UInt16}, ~~~a = ~~~b ↔ a = b
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- **Alias** of `OrderIso.cof_congr`. -/
RelIso.cof_eq : ∀ {α γ : Type u} [inst : Preorder α] [inst_1 : Preorder γ] (f : α ≃o γ), Order.cof α = Order.cof γ
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →L[𝕜] E}, IsSelfAdjoint A ↔ (↑A).IsSymmetric
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.App.mk : Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.FunProp.Mor.App
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.resCongr_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] (f f' : G →ₜ* H) (h : f = f'),
  (ContAction.resCongr V f f' h).hom =
    { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).hom,
      naturality := ⋯ }
-- Mathlib.Algebra.Lie.Semisimple.Defs
/-- A nontrivial Lie module is *irreducible* if its only Lie submodules are `⊥` and `⊤`.  -/
LieModule.IsIrreducible : (R : Type u_1) →
  (L : Type u_2) →
    (M : Type u_3) →
      [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : AddCommGroup M] → [Module R M] → [LieRingModule L M] → Prop
-- Mathlib.Algebra.Group.Action.Basic
AddAction.surjective : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α),
  Function.Surjective fun x => g +ᵥ x
-- Lean.Environment
Lean.AsyncBranch.mainEnv.sizeOf_spec : sizeOf Lean.AsyncBranch.mainEnv = 1
-- Mathlib.Order.WithBot
WithTop.untopA_le : ∀ {α : Type u_1} [inst : PartialOrder α] {y : WithTop α} {b : α} [inst_1 : Nonempty α], y ≤ ↑b → y.untopA ≤ b
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- The **Cauchy criterion** for infinite sums, also known as the
**Cauchy convergence test**  -/
summable_iff_cauchySeq_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommMonoid α] [CompleteSpace α] {f : β → α},
  Summable f ↔ CauchySeq fun s => ∑ b ∈ s, f b
-- Mathlib.Data.Set.MulAntidiagonal
/-- `Set.addAntidiagonal s t a` is the set of all pairs of an element in `s` and an
element in `t` that add to `a`.  -/
Set.antidiagonal : {α : Type u_1} → [Add α] → Set α → Set α → α → Set (α × α)
-- Mathlib.Order.WithBot
WithBot.exists : ∀ {α : Type u_1} {p : WithBot α → Prop}, (∃ x, p x) ↔ p ⊥ ∨ ∃ x, p ↑x
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (e : E) {U : Set 𝕜}, MeromorphicOn (fun x => e) U
-- Mathlib.Algebra.Order.Floor.Defs
Int.le_floor : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {z : ℤ} {a : α}, z ≤ ⌊a⌋ ↔ ↑z ≤ a
-- Mathlib.CategoryTheory.EpiMono
/-- The chosen section of a split epimorphism.
(Note that `section` is a reserved keyword, so we append an underscore.)
 -/
CategoryTheory.section_ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (f : X ⟶ Y) → [hf : CategoryTheory.IsSplitEpi f] → Y ⟶ X
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.iSup_lt_ord_of_isRegular : ∀ {ι : Type u_1} {f : ι → Ordinal.{u_1}} {c : Cardinal.{u_1}},
  c.IsRegular → Cardinal.mk ι < c → (∀ (i : ι), f i < c.ord) → iSup f < c.ord
-- Mathlib.Data.Nat.Multiplicity
/-- The multiplicity of `m` in `n` is the number of positive natural numbers `i` such that `m ^ i`
divides `n`. This set is expressed by filtering `Ico 1 b` where `b` is any bound greater than
`log m n`.  -/
Nat.emultiplicity_eq_card_pow_dvd : ∀ {m n b : ℕ}, m ≠ 1 → 0 < n → Nat.log m n < b → emultiplicity m n = ↑{i ∈ Finset.Ico 1 b | m ^ i ∣ n}.card
-- Mathlib.Order.Filter.Interval
/-- `Function.uncurry Ixx` tends to `l₂.smallSets` along `l₁ ×ˢ l₁`. In other words, for any
`s ∈ l₂` there exists `t ∈ l₁` such that `Ixx x y ⊆ s` whenever `x ∈ t` and `y ∈ t`.

Use lemmas like `Filter.Tendsto.Icc` instead.  -/
Filter.TendstoIxxClass.tendsto_Ixx : ∀ {α : Type u_1} {Ixx : α → α → Set α} {l₁ : Filter α} {l₂ : outParam (Filter α)}
  [self : Filter.TendstoIxxClass Ixx l₁ l₂], Filter.Tendsto (fun p => Ixx p.1 p.2) (l₁ ×ˢ l₁) l₂.smallSets
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.zpow_smul_eq_iff_period_dvd : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] {j : ℤ} {g : G} {a : α},
  g ^ j • a = a ↔ ↑(MulAction.period g a) ∣ j
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (T : CategoryTheory.Over X),
  (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f).unit.app T =
    CategoryTheory.Over.homMk
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Over X)).obj T).left) T.hom)
      ⋯
-- Mathlib.GroupTheory.Divisible
/-- The division function  -/
DivisibleBy.div : {A : Type u_1} →
  {α : Type u_2} → {inst : AddMonoid A} → {inst_1 : SMul α A} → {inst_2 : Zero α} → [self : DivisibleBy A α] → A → α → A
-- Mathlib.Data.ENNReal.Basic
ENNReal.top_ne_coe : ∀ {r : NNReal}, ⊤ ≠ ↑r
-- Mathlib.Topology.Connected.Basic
IsPreconnected.union : ∀ {α : Type u} [inst : TopologicalSpace α] (x : α) {s t : Set α},
  x ∈ s → x ∈ t → IsPreconnected s → IsPreconnected t → IsPreconnected (s ∪ t)
-- Mathlib.Topology.Filter
Filter.continuous_nhds : ∀ {X : Type u_4} [inst : TopologicalSpace X], Continuous nhds