mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_baseChange : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) (A : Type u_8) [inst_9 : CommRing A] [inst_10 : Algebra R A],
  (LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ).polyCharpoly (Algebra.TensorProduct.basis A b) =
    Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpoly b)
-- Init.Control.Lawful.Instances
OptionT.run_control : ∀ {m : Type u → Type u_1} {α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)),
  (control f).run = f fun {β} x => x.run
-- Init.Core
Except.error.injEq : ∀ {ε : Type u} {α : Type v} (a a_1 : ε), (Except.error a = Except.error a_1) = (a = a_1)
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprRaw_mathlib_1 : Lean.ToExpr Substring.Raw
-- Mathlib.Tactic.DepRewrite
/-- Cached `p.toHeadIndex`.  -/
Mathlib.Tactic.DepRewrite.Context.pHeadIdx : Mathlib.Tactic.DepRewrite.Context → Lean.HeadIndex
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        k ∈ l → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKey! k' = k
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_insert_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → insert b (Set.Ico a b) = Set.Icc a b
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.collectValues : Lean.Meta.Match.Problem → Array Lean.Expr
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.prod_injective : ∀ {H : Type u_3} [inst : Group H] {ι : Type u_5} {G : ι → Type u_6} [inst_1 : (i : ι) → Group (G i)]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ},
  Function.Injective Monoid.PushoutI.NormalWord.prod
-- Mathlib.Order.Max
IsBot.prodMk : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsBot a → IsBot b → IsBot (a, b)
-- Aesop.Rule
Aesop.instLESafeRuleInfo : LE Aesop.SafeRuleInfo
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- In a 2-truncated quasicategory, right homotopy implies left homotopy.
 -/
SSet.Truncated.HomotopicR.homotopicL : ∀ {X : SSet.Truncated 2} [X.Quasicategory₂]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicR f g → SSet.Truncated.HomotopicL f g
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.coe_transPartialEquiv_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ≃ β} {g : PartialEquiv β γ},
  ↑(f.transPartialEquiv g).symm = ⇑f.symm ∘ ↑g.symm
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.eq_1 : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u}
  {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (it' : Std.IterM m β) (out : β),
  Std.Iterators.Types.ULiftIterator.Monadic.modifyStep (Std.IterStep.yield it' out) =
    Std.IterStep.yield { internalState := { inner := it' } } { down := out }
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.Internal.List.getKey!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] (a : α) (l : List ((a : α) × β a)),
  Std.Internal.List.getKey! a l = (Std.Internal.List.getKey? a l).get!
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.Hom.comp_eq_comp : ∀ {J : CategoryTheory.Limits.MulticospanShape} {X Y Z : CategoryTheory.Limits.WalkingMulticospan J} (f : X ⟶ Y)
  (g : Y ⟶ Z), CategoryTheory.Limits.WalkingMulticospan.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [inst : BEq α] [Std.LawfulBEqOrd α]
  [Std.TransOrd α] (h : t.WF) {l : List α} {k fallback : α},
  k ∉ t →
    l.contains k = false → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKeyD k fallback = fallback
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.le_neg_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommGroup M] [Lean.Grind.OrderedAdd M]
  {a b : M}, a ≤ -b ↔ b ≤ -a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_insertMany_empty_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List (α × β)}
  {k : α},
  Std.DTreeMap.Internal.Impl.contains k
      ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯) =
    (List.map Prod.fst l).contains k
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.trivialization_target : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  (Bundle.Trivial.trivialization B F).target = Set.univ
-- Mathlib.Data.Rat.Floor
Rat.ceil_natCast_div_natCast : ∀ (n d : ℕ), ⌈↑n / ↑d⌉ = -(-↑n / ↑d)
-- Mathlib.Topology.Order.Completion
Order.Fill.instOrderTopology : ∀ {α : Type u_1} [inst : LinearOrder α], OrderTopology (Order.Fill α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tendsto_tan_neg_pi_div_two : Filter.Tendsto Real.tan (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) Filter.atBot
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerRight.of.sizeOf_spec : ∀ (η : Mathlib.Tactic.BicategoryLike.Atom), sizeOf (Mathlib.Tactic.BicategoryLike.WhiskerRight.of η) = 1 + sizeOf η
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.eval₂_trunc_eq_sum_range : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (s : S) (G : R →+* S) (n : ℕ)
  (f : PowerSeries R),
  Polynomial.eval₂ G s ((PowerSeries.trunc n) f) = ∑ i ∈ Finset.range n, G ((PowerSeries.coeff i) f) * s ^ i
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs : Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.coreAssociator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  (H : CategoryTheory.Functor E E'),
  (F.associator G H).core =
    (F.comp G).coreComp H ≪≫
      CategoryTheory.Functor.isoWhiskerRight (F.coreComp G) H.core ≪≫
        F.core.associator G.core H.core ≪≫ (F.core.isoWhiskerLeft (G.coreComp H)).symm ≪≫ (F.coreComp (G.comp H)).symm
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.Set.prod_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y)
  (x : { c // (fun x => x ∈ s) c.1 ∧ (fun x => x ∈ t) c.2 }), (Homeomorph.Set.prod s t) x = (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  groupCohomology.cocycles₁ A = (ModuleCat.Hom.hom (groupCohomology.d₁₂ A)).ker
-- Mathlib.CategoryTheory.Limits.Cones
/-- The category of cocones on a given diagram.  -/
CategoryTheory.Limits.Cocone.category : {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.Category.{v₃, max (max u₃ u₁) v₃} (CategoryTheory.Limits.Cocone F)
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- If a function is `C^n` on a domain with unique derivatives, then its bundled derivative
is `C^m` when `m+1 ≤ n`.  -/
ContMDiffOn.contMDiffOn_tangentMapWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {m n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  [Is : IsManifold I 1 M] [I's : IsManifold I' 1 M'],
  ContMDiffOn I I' n f s →
    m + 1 ≤ n →
      UniqueMDiff[s] → ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
-- Init.Internal.Order.Basic
Lean.Order.iterates.below.step : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α} {motive : (a : α) → Lean.Order.iterates f a → Prop} {x : α}
  (a : Lean.Order.iterates f x), Lean.Order.iterates.below a → motive x a → Lean.Order.iterates.below ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_toArray_rco : ∀ {m n : ℕ}, (m<...=n).toArray = ((m + 1)...n + 1).toArray
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Const.insertMany t l).getKeyD k' fallback = k
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps.mk.inj : ∀ {map map_1 : Std.HashMap ℕ (Std.TreeSet ℕ compare)}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.Algebra.Category.AlgCat.FilteredColimits
/-- The cocone of the underlying diagram of rings lifted to `AlgCat R`. The algebra instance
on the cocone point is induced from the `j`-th inclusion map.  -/
_private.Mathlib.Algebra.Category.AlgCat.FilteredColimits.0.AlgCat.coconeOfIsFiltered : {R : Type u} →
  [inst : CommRing R] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        {F : CategoryTheory.Functor J (AlgCat R)} →
          [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget RingCat)] →
            {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget₂ (AlgCat R) RingCat))} →
              [CategoryTheory.IsFilteredOrEmpty J] →
                CategoryTheory.Limits.IsColimit c → J → CategoryTheory.Limits.Cocone F
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.inclusion_eq_id : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι), RestrictedProduct.inclusion R A ⋯ = id
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.integralRep_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {I : FractionalIdeal (nonZeroDivisors R) (FractionRing R)},
  I ≠ 0 → I.num ∈ nonZeroDivisors (Ideal R)
-- Mathlib.Data.Set.Basic
Set.mem_empty_iff_false : ∀ {α : Type u} (x : α), x ∈ ∅ ↔ False
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' fallback : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true then k else fallback
    else t.getKeyD k' fallback
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.symm_trans_self : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.symm.trans e ≈ OpenPartialHomeomorph.ofSet e.target ⋯
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The linear map from sesquilinear maps to `Matrix n m N₂` given an `n`-indexed basis for `M₁`
and an `m`-indexed basis for `M₂`.

This is an auxiliary definition for the equivalence `Matrix.toLinearMapₛₗ₂'`.  -/
LinearMap.toMatrix₂Aux : (R : Type u_1) →
  {R₁ : Type u_2} →
    {S₁ : Type u_3} →
      {R₂ : Type u_4} →
        {S₂ : Type u_5} →
          {M₁ : Type u_6} →
            {M₂ : Type u_7} →
              {N₂ : Type u_10} →
                {n : Type u_11} →
                  {m : Type u_12} →
                    [inst : CommSemiring R] →
                      [inst_1 : Semiring R₁] →
                        [inst_2 : Semiring S₁] →
                          [inst_3 : Semiring R₂] →
                            [inst_4 : Semiring S₂] →
                              [inst_5 : AddCommMonoid M₁] →
                                [inst_6 : Module R₁ M₁] →
                                  [inst_7 : AddCommMonoid M₂] →
                                    [inst_8 : Module R₂ M₂] →
                                      [inst_9 : AddCommMonoid N₂] →
                                        [inst_10 : Module R N₂] →
                                          [inst_11 : Module S₁ N₂] →
                                            [inst_12 : Module S₂ N₂] →
                                              [inst_13 : SMulCommClass S₁ R N₂] →
                                                [inst_14 : SMulCommClass S₂ R N₂] →
                                                  [inst_15 : SMulCommClass S₂ S₁ N₂] →
                                                    {σ₁ : R₁ →+* S₁} →
                                                      {σ₂ : R₂ →+* S₂} →
                                                        (n → M₁) →
                                                          (m → M₂) → (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂
-- Mathlib.Topology.Category.Sequential
Sequential.instFullTopCatSequentialToTop : Sequential.sequentialToTop.Full
-- Mathlib.Algebra.Notation.Support
Function.support_comp_eq : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] (g : M → N),
  (∀ {x : M}, g x = 0 ↔ x = 0) → ∀ (f : ι → M), Function.support (g ∘ f) = Function.support f
-- Mathlib.Combinatorics.Quiver.Path.Decomposition
Quiver.Path.exists_mem_notMem_hom_path_path_of_notMem_mem : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) (S : Set V),
  a ∈ S → b ∉ S → ∃ u ∈ S, ∃ v ∉ S, ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- The bicoloring of a complete bipartite graph using whether a vertex
is on the left or on the right.  -/
SimpleGraph.CompleteBipartiteGraph.bicoloring : (V : Type u_4) → (W : Type u_5) → (completeBipartiteGraph V W).Coloring Bool
-- Batteries.Recycling.RBTree.Alter
/-- The `modify` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.modify : ∀ {α : Type u_1} {cut : α → Ordering} {cmp : α → α → Ordering} {f : α → α} {t : RBTree.RBNode α},
  RBTree.RBNode.OnRoot (fun x => RBTree.RBNode.cmpEq cmp (f x) x) (RBTree.RBNode.zoom cut t).1 →
    RBTree.RBNode.Ordered cmp t → RBTree.RBNode.Ordered cmp (RBTree.RBNode.modify cut f t)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C},
  CategoryTheory.Injective (CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlp 0).Z
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `F` is fully faithful, then so is `Over.post F`.  -/
CategoryTheory.Functor.FullyFaithful.over : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (X : T) → (F : CategoryTheory.Functor T D) → F.FullyFaithful → (CategoryTheory.Over.post F).FullyFaithful
-- Mathlib.Order.Filter.Partial
Filter.rcomap'_compose : ∀ {α : Type u} {β : Type v} {γ : Type w} (r : SetRel α β) (s : SetRel β γ),
  Filter.rcomap' r ∘ Filter.rcomap' s = Filter.rcomap' (r.comp s)
-- Mathlib.Algebra.Group.EvenFunction
/-- If `f` is both even and odd, and its target is a torsion-free commutative additive group,
then `f = 0`.
 -/
Function.zero_of_even_and_odd : ∀ {α : Type u_3} {β : Type u_4} [inst : AddCommGroup β] [IsAddTorsionFree β] {f : α → β} [inst_2 : Neg α],
  Function.Even f → Function.Odd f → f = 0
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.degree_list_prod_le : ∀ {S : Type u_1} [inst : Semiring S] (l : List (Polynomial S)), l.prod.degree ≤ (List.map Polynomial.degree l).sum
-- Lean.Data.AssocList
Lean.AssocList.any : {α : Type u} → {β : Type v} → (α → β → Bool) → Lean.AssocList α β → Bool
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendSingleIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : DecidableEq ι] (e : c.Embedding c') (X : C)
  [inst_4 : DecidableEq ι'] (i : ι) (i' : ι') (h : e.f i = i'),
  HomologicalComplex.extendSingleIso e X i i' h = HomologicalComplex.extendSingleIso e X i i' h
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_lt_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ},
  m.toSyn 0 < m.toSyn d → (m.toSyn (m.degree f) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d)
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized₀_le_localized₀_of_smul_le : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] {P Q : Submodule R M} (x : ↥p),
  x • P ≤ Q → Submodule.localized₀ p f P ≤ Submodule.localized₀ p f Q
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.toConstProdLinearMap_symm_apply : ∀ (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddCommGroup V2] [inst_3 : Module k V1] [inst_4 : Module k V2] [inst_5 : Semiring R] [inst_6 : Module R V2]
  [inst_7 : SMulCommClass k R V2] (p : V2 × (V1 →ₗ[k] V2)),
  (AffineMap.toConstProdLinearMap R).symm p = p.2.toAffineMap + AffineMap.const k V1 p.1
-- Mathlib.Order.PFilter
Order.PFilter.ext_iff : ∀ {P : Type u_1} [inst : Preorder P] {s t : Order.PFilter P}, s = t ↔ ↑s = ↑t
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.tail_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).tail = p.copy ⋯ ⋯
-- Mathlib.GroupTheory.FinitelyPresentedGroup
Group.IsFinitelyPresented.instPresentedGroupOfFiniteElemFreeGroup : ∀ {α : Type u_3} [Finite α] (s : Set (FreeGroup α)) [Finite ↑s], Group.IsFinitelyPresented (PresentedGroup s)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.breakCont : Lean.Elab.Do.ContInfo → Option (Lean.Elab.Do.DoElabM Lean.Expr)
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Context.mk.sizeOf_spec : ∀ (config : Mathlib.Meta.FunProp.Config) (constToUnfold : Std.TreeSet Lean.Name Lean.Name.quickCmp)
  (disch : Lean.Expr → Lean.MetaM (Option Lean.Expr)) (transitionDepth : ℕ),
  sizeOf { config := config, constToUnfold := constToUnfold, disch := disch, transitionDepth := transitionDepth } =
    1 + sizeOf config + sizeOf constToUnfold + sizeOf transitionDepth
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).minKey ⋯ = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- A family `f i : ArithmeticFunction R` tends to `g` if and only if for each `n`, the `n`th
coefficient of `f i` is eventually equal to the `n`th coefficient of `g`. If `R` is viewed as
having the discrete topology, then this is the topology of pointwise convergence.

See `tendsTo_eulerProduct_of_tendsTo` for the outward facing `eulerProduct` API.  -/
_private.Mathlib.NumberTheory.ArithmeticFunction.LFunction.0.ArithmeticFunction.tendsto_iff : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {f : ι → ArithmeticFunction R} {F : Filter ι}
  {g : ArithmeticFunction R}, Filter.Tendsto f F (nhds g) ↔ ∀ (n : ℕ), ∀ᶠ (i : ι) in F, (f i) n = g n
-- Mathlib.Algebra.Star.Prod
Prod.instStarAddMonoid : {R : Type u} →
  {S : Type v} →
    [inst : AddMonoid R] → [inst_1 : AddMonoid S] → [StarAddMonoid R] → [StarAddMonoid S] → StarAddMonoid (R × S)
-- Mathlib.Data.Setoid.Partition
/-- A map choosing a representative for each element of the quotient associated to an indexed
partition. This is a computable version of `Quotient.out` using `IndexedPartition.some`.  -/
IndexedPartition.out : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → (hs : IndexedPartition s) → hs.Quotient ↪ α
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.hermite.eq_2 : ∀ (n : ℕ),
  Polynomial.hermite n.succ = Polynomial.X * Polynomial.hermite n - Polynomial.derivative (Polynomial.hermite n)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_univ : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι}, TendstoLocallyUniformlyOn F f p Set.univ ↔ TendstoLocallyUniformly F f p
-- Mathlib.Data.Finset.Basic
Finset.erase_sdiff_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (a : α), (s \ t).erase a = s.erase a \ t.erase a
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.w_assoc : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (self : CategoryTheory.CommaMorphism X Y) {Z : T}
  (h : R.obj Y.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.map self.left) (CategoryTheory.CategoryStruct.comp Y.hom h) =
    CategoryTheory.CategoryStruct.comp X.hom (CategoryTheory.CategoryStruct.comp (R.map self.right) h)
-- Mathlib.RingTheory.Radical.Basic
Associated.primeFactors_eq : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, Associated a b → UniqueFactorizationMonoid.primeFactors a = UniqueFactorizationMonoid.primeFactors b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasFDerivWithinAt.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E}
  {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) • f') s x
-- Aesop.Forward.RuleInfo
Aesop.Slot.mk.sizeOf_spec : ∀ (typeDiscrTreeKeys? : Option (Array Lean.Meta.DiscrTree.Key)) (index : Aesop.SlotIndex)
  (premiseIndex : Aesop.PremiseIndex) (deps common : Std.HashSet Aesop.PremiseIndex)
  (forwardDeps : Array Aesop.PremiseIndex),
  sizeOf
      { typeDiscrTreeKeys? := typeDiscrTreeKeys?, index := index, premiseIndex := premiseIndex, deps := deps,
        common := common, forwardDeps := forwardDeps } =
    1 + sizeOf typeDiscrTreeKeys? + sizeOf index + sizeOf premiseIndex + sizeOf deps + sizeOf common +
      sizeOf forwardDeps