mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Defs
/-- Constructs a `Group` structure on a `Monoid` consisting only of units.  -/
groupOfIsUnit : {M : Type u_1} → [hM : Monoid M] → (∀ (a : M), IsUnit a) → Group M
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_subset_uIcc_left : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
  x ∈ Finset.uIcc a b → Finset.uIcc a x ⊆ Finset.uIcc a b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_12 : ∀ (k : ℕ) (x_1 : Lean.Grind.CommRing.Var),
  ((Lean.Grind.CommRing.Expr.var x_1).pow k).toPoly =
    bif k == 0 then Lean.Grind.CommRing.Poly.num 1
    else Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x_1, k := k } Lean.Grind.CommRing.Mon.unit)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instBot : {R : Type u} → [inst : NonAssocSemiring R] → Bot (Subsemiring R)
-- Std.Data.ExtTreeSet.Basic
/-- Given a proof that such an element exists, retrieves the smallest element that is
greater than or equal to the given element.
 -/
Std.ExtTreeSet.getGE : {α : Type u} →
  {cmp : α → α → Ordering} →
    [inst : Std.TransCmp cmp] → (t : Std.ExtTreeSet α cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α
-- Std.Data.String.ToNat
String.toNat?_eq_none : ∀ {s : String}, s.isNat = false → s.toNat? = none
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedSMul.smul_le_smul_right : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : SMul G P} [self : IsOrderedSMul G P] (c d : G),
  c ≤ d → ∀ (a : P), c • a ≤ d • a
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.LiesOver.instLiesOverRealValAbsoluteValueExistsRingHomComplexEqPlaceMkOfLiesOver : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {φ : K →+* ℂ} {ψ : L →+* ℂ}
  [NumberField.ComplexEmbedding.LiesOver ψ φ],
  (↑(NumberField.InfinitePlace.mk ψ)).LiesOver ↑(NumberField.InfinitePlace.mk φ)
-- Mathlib.Data.Finset.Max
Finset.max_of_mem : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a : α}, a ∈ s → ∃ b, s.max = ↑b
-- Mathlib.Tactic.Convert
/-- `convert_to t` on a goal `⊢ t'` changes the goal to `⊢ t` and adds new goals for proving the
equality `t' = t` using congruence. The goals are created like `congr!` would.
Any remaining congruence goals come before the main goal.
Like `refine e`, any holes (`?_` or `?x`) in `t` that are not solved by unification are converted
into new goals, using the hole's name, if any, as the goal case name.
Like `congr!`, `convert_to` introduces variables while applying congruence rules. These can be
pattern-matched, like `rintro` would, using the `with` keyword.

`convert e`, where `e` is a term of type `t`, uses `e` to close the new main goal. In other words,
`convert e` works like `convert_to t; refine e`. Both tactics use the same options.

* `convert_to! t` uses default transparency, rather than reducible, when solving side goals.
* `convert_to ty at h` changes the type of the local hypothesis `h` to `ty`. If later local
  hypotheses or the goal depend on `h`, then `convert_to t at h` may leave a copy of `h`.
* `convert_to ← t` creates equality goals in the opposite direction (with the original goal type on
  the right).
* `convert_to t using n`, where `n` is a positive numeral, controls the depth with which congruence
  is applied. For example, if the main goal is `⊢ Prime (n + n + 1)`,
  then `convert_to Prime (2 * n + 1) using 2` results in one goal, `⊢ n + n = 2 * n`, and
  `convert_to Prime (2 * n + 1) using 3` (or more) results in two (impossible) goals
  `⊢ HAdd.hAdd = HMul.hMul` and `⊢ n = 2`.
  The default value for `n` is 1.
* `convert_to t with x ⟨y₁, y₂⟩ (z₁ | z₂)` names or pattern-matches the variables introduced by
  congruence rules, like `rintro x ⟨y₁, y₂⟩ (z₁ | z₂)` would.
* `convert_to (config := cfg) t` uses the configuration options in `cfg` to control the congruence
  rules (see `Congr!.Config`).
 -/
Mathlib.Tactic.convertTo : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_le_add_iff_left : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [inst_1 : LE α] [AddLeftMono α] [AddLeftReflectLE α],
  x ≠ ⊤ → (x + y ≤ x + z ↔ y ≤ z)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- Each element of a reproducing kernel Hilbert space may be coerced into a function.
 -/
RKHS.instFunLike : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            {H : Type u_4} →
              [inst_3 : NormedAddCommGroup H] → [inst_4 : InnerProductSpace 𝕜 H] → [RKHS 𝕜 H X V] → FunLike H X V
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eval_zero_of_odd : ∀ (R : Type u_1) [inst : CommRing R] {n : ℤ}, Odd n → Polynomial.eval 0 (Polynomial.Chebyshev.T R n) = 0
-- Mathlib.Order.Filter.Cofinite
/-- For an injective function `f`, inverse images of finite sets are finite. See also
`Filter.comap_cofinite_le` and `Function.Injective.comap_cofinite_eq`.  -/
Function.Injective.tendsto_cofinite : ∀ {α : Type u_2} {β : Type u_3} {f : α → β}, Function.Injective f → Filter.Tendsto f Filter.cofinite Filter.cofinite
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.commSemigroup : {α : Type u} → [AddCommSemigroup α] → CommSemigroup (Multiplicative α)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.of.eq_1 : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : CompactSpace G] [inst_4 : TotallyDisconnectedSpace G],
  ProfiniteAddGrp.of G = { toProfinite := Profinite.of G, addGroup := inst, topologicalAddGroup := inst_2 }
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.orderOf_pow : ∀ {G : Type u_1} [inst : Monoid G] (x : G) (n : ℕ), IsOfFinOrder x → orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinite.ne_zero : ∀ {x : ℝ*}, x.Infinite → x ≠ 0
-- Mathlib.Topology.Category.LightProfinite.Limits
LightProfinite.instEpiCompHausLikeAndTotallyDisconnectedSpaceCarrierSecondCountableTopologyFst : ∀ {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) [h : CategoryTheory.Epi g],
  CategoryTheory.Epi (CompHausLike.pullback.fst f g)
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.instInhabitedStartsWithResult.default : Lean.Grind.AC.StartsWithResult✝
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.asymptoticNhds_eq_smul_vadd : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V) (p : P),
  AffineSpace.asymptoticNhds k P v = Filter.atTop • nhds v +ᵥ pure p
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.WF →
    m₂.WF →
      ∀ (f : (a : α) → β a → Option (γ a)),
        m₁.Equiv m₂ → (Std.DHashMap.Raw.filterMap f m₁).Equiv (Std.DHashMap.Raw.filterMap f m₂)
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of `p` is `p⁻¹` if `p` is prime.

See also `padicNorm.padicNorm_p` for a version assuming `1 < p`.  -/
padicNorm.padicNorm_p_of_prime : ∀ {p : ℕ} [Fact (Nat.Prime p)], padicNorm p ↑p = (↑p)⁻¹
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
SpectrumRestricts.isometric_cfc : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S]
  [inst_10 : Ring A] [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [inst_18 : MetricSpace A]
  [IsometricContinuousFunctionalCalculus S A q] [CompleteSpace R] [ContinuousMap.UniqueHom R A] (f : C(S, R)),
  Isometry ⇑(algebraMap R S) →
    p 0 → (∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f) → IsometricContinuousFunctionalCalculus R A p
-- Mathlib.Algebra.Algebra.Prod
AlgHom.prod_fst_snd : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B], (AlgHom.fst R A B).prod (AlgHom.snd R A B) = AlgHom.id R (A × B)
-- Mathlib.Algebra.Category.Ring.Limits
/-- An auxiliary declaration to speed up typechecking.
 -/
CommRingCat.forget₂CommSemiRingPreservesLimitsAux : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] →
        CategoryTheory.Limits.IsLimit
          ((CategoryTheory.forget₂ CommRingCat CommSemiRingCat).mapCone (CommRingCat.limitCone F))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.isEmpty = true → t.getKeyD a fallback = fallback
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.of_ringHom_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B] [inst_9 : RingHomClass FAB A B]
  (f : FRS) (g : FAB) {a : A},
  IsAlgebraic S (g a) →
    Function.Surjective ⇑f →
      Function.Injective ⇑g → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → IsAlgebraic R a
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_equivCurry : ∀ {ι : Type u_6} {κ : Type u_7} {X : Type u_8} [inst : MeasurableSpace X], Measurable ⇑(Equiv.curry ι κ X)
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.exists_pow_eq_iff' : ∀ {n a : ℕ}, n ≠ 0 → ((∃ x, x ^ n = a) ↔ n.nthRoot a ^ n = a)
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.univ : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)}, Filter.CardinalGenerateSets g Set.univ
-- Mathlib.Algebra.Group.Prod
Prod.instAddLeftCancelMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddLeftCancelMonoid M] [inst_1 : AddLeftCancelMonoid N],
  Prod.instAddLeftCancelMonoid = { toAddMonoid := Prod.instAddMonoid, toIsLeftCancelAdd := ⋯ }
-- Init.Data.List.Basic
List.reverseAux_cons : ∀ {α : Type u_1} {a : α} {l r : List α}, (a :: l).reverseAux r = l.reverseAux (a :: r)
-- Mathlib.NumberTheory.ModularForms.Discriminant
_private.Mathlib.NumberTheory.ModularForms.Discriminant.0.ModularForm.logDeriv_eta_comp_div_eq : ∀ (z : UpperHalfPlane), logDeriv (ModularForm.eta ∘ fun x => -1 / x) ↑z = (↑z ^ 2)⁻¹ * logDeriv ModularForm.eta (-↑z)⁻¹
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.mk_coeff : ∀ {p n : ℕ} {R : Type u_1} (x : TruncatedWittVector p n R),
  (TruncatedWittVector.mk p fun i => TruncatedWittVector.coeff i x) = x
-- Mathlib.Order.Category.Preord
/-- The equivalence between `Preord` and itself induced by `OrderDual` both ways.  -/
Preord.dualEquiv : Preord ≌ Preord
-- Mathlib.Data.Complex.Basic
Complex.div_I : ∀ (z : ℂ), z / Complex.I = -(z * Complex.I)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toRingHom_apply_symm_toRingHom_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S) (y : S),
  e.toRingHom (e.symm.toRingHom y) = y
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} {E' : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  [inst_3 : CategoryTheory.Category.{v_2, u_2} E'] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ}
  {G : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ} {H : CategoryTheory.Functor Eᵒᵖ E'ᵒᵖ},
  CategoryTheory.NatIso.unop (F.associator G H) =
    F.unopComp (G.comp H) ≪≫
      F.unop.isoWhiskerLeft (G.unopComp H) ≪≫
        (F.unop.associator G.unop H.unop).symm ≪≫
          CategoryTheory.Functor.isoWhiskerRight (F.unopComp G).symm H.unop ≪≫ ((F.comp G).unopComp H).symm
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C) (x : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).obj x = A.X
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.SimpleHandler : Type
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.inter_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ ∩ t₃).Equiv (t₂ ∩ t₃)
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.ι_D₂_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (j j' : J) (i₁ : I₁) (i₂ : I₂)
  (h : c₁.π c₂ c (i₁, i₂) = j) {Z : D} (h_1 : (K₁.mapBifunctor K₂ F c).X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.D₂ K₁ K₂ F c j j') h_1) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j') h_1
-- Mathlib.Order.Filter.Map
Filter.principal_singleton : ∀ {α : Type u_1} (a : α), Filter.principal {a} = pure a
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.ker_le_range_iff : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddZeroClass I]
  (f : G →+ H) [inst_3 : f.range.Normal] (g : H →+ I),
  g.ker ≤ f.range ↔ (QuotientAddGroup.mk' f.range).comp g.ker.subtype = 0
-- Mathlib.Order.Category.DistLat
DistLat.Hom.ext : ∀ {X Y : DistLat} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_eq_getLast_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅},
  t.max he = t.toList.getLast ⋯
-- Mathlib.Probability.Density
/-- A random variable `X : Ω → E` is said to have a probability density function (`HasPDF`)
with respect to the measure `ℙ` on `Ω` and `μ` on `E`
if the push-forward measure of `ℙ` along `X` is absolutely continuous with respect to `μ`
and they have a Lebesgue decomposition (`HaveLebesgueDecomposition`).  -/
MeasureTheory.HasPDF : {Ω : Type u_1} →
  {E : Type u_2} →
    [inst : MeasurableSpace E] →
      {m : MeasurableSpace Ω} →
        (Ω → E) → MeasureTheory.Measure Ω → autoParam (MeasureTheory.Measure E) MeasureTheory.HasPDF._auto_1 → Prop
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cocones` is corepresented by `X`, the cocone corresponding to the identity morphism on `X`
will be a colimit cocone.  -/
CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → {X : C} → F.cocones.CorepresentableBy X → CategoryTheory.Limits.Cocone F
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.liftNC_one : ∀ {k : Type u_1} {G : Type u_2} {g_hom : Type u_3} {R : Type u_4} [inst : NonAssocSemiring k] [inst_1 : One G]
  [inst_2 : Semiring R] [inst_3 : FunLike g_hom G R] [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom),
  (SkewMonoidAlgebra.liftNC ↑f ⇑g) 1 = 1
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwLemma.mk.inj : ∀ {name : Mathlib.Tactic.ClickSuggestions.Premise} {symm : Bool} {relName : Lean.Name}
  {name_1 : Mathlib.Tactic.ClickSuggestions.Premise} {symm_1 : Bool} {relName_1 : Lean.Name},
  { name := name, symm := symm, relName := relName } = { name := name_1, symm := symm_1, relName := relName_1 } →
    name = name_1 ∧ symm = symm_1 ∧ relName = relName_1
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_ofCoeff`. -/
SkewMonoidAlgebra.coeff_ofFinsupp : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (f : G →₀ k), { coeff := f }.coeff = f
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The obvious auto-equivalence of a monoidal category is monoidal.  -/
CategoryTheory.Equivalence.isMonoidal_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Equivalence.refl.IsMonoidal
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- A lift of a monotone degree one map `S¹ → S¹`.  -/
CircleDeg1Lift : Type
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.insert : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Lean.PersistentHashSet α
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  [inst_1 : SizeOf C] (f : A.A ⟶ B.A)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map f) = CategoryTheory.CategoryStruct.comp f B.a)
      CategoryTheory.Comonad.Coalgebra.Hom.h._autoParam),
  sizeOf { f := f, h := h } = 1 + sizeOf f + sizeOf h
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- the restriction maps of a presheaf of modules  -/
PresheafOfModules.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (self : PresheafOfModules R) →
        {X Y : Cᵒᵖ} →
          (f : X ⟶ Y) → self.obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (self.obj Y)
-- Mathlib.RingTheory.Congruence.Defs
/-- The inductively defined smallest ring congruence relation containing a given binary
relation.  -/
ringConGen : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → (R → R → Prop) → RingCon R
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.LeCnstr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm c) = 1 + sizeOf c
-- Batteries.Data.Stream
_private.Batteries.Data.Stream.0.Std.Stream.take.match_1.splitter : {σ : Type u_2} →
  {α : Type u_1} →
    (motive : List α × σ → Sort u_3) → (x : List α × σ) → ((as : List α) → (s : σ) → motive (as, s)) → motive x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insert.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → ∀ (b b_1 : β), b = b_1 → m.insert a b = m_1.insert a_1 b_1
-- Mathlib.LinearAlgebra.Dimension.Constructions
Submodule.lt_of_le_of_finrank_lt_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Submodule R M},
  s ≤ t → Module.finrank R ↥s < Module.finrank R ↥t → s < t
-- Init.Internal.Order.Lemmas
Array.mapFinIdxM.map.induct : ∀ {α : Type u} {β : Type v} (as : Array α) (motive : (i j : ℕ) → i + j = as.size → Array β → Prop),
  (∀ (j : ℕ) (bs : Array β) (x : 0 + j = as.size), motive 0 j x bs) →
    (∀ (j : ℕ) (bs : Array β) (i : ℕ) (inv : i + 1 + j = as.size),
        j < as.size →
          ∀ (this : i + (j + 1) = as.size),
            (∀ (__do_lift : β), motive i (j + 1) this (bs.push __do_lift)) → motive i.succ j inv bs) →
      ∀ (i j : ℕ) (inv : i + j = as.size) (bs : Array β), motive i j inv bs
-- Mathlib.Data.SetLike.Basic
SetLike.exists : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : ↥p → Prop}, (∃ x, q x) ↔ ∃ x, ∃ (h : x ∈ p), q ⟨x, h⟩
-- Mathlib.CategoryTheory.Monad.EquivMon
/-- To every monoid object in `C ⥤ C` we associate a `Monad C`.  -/
CategoryTheory.Monad.ofMon : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Mon (CategoryTheory.Functor C C) → CategoryTheory.Monad C
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad n Pred EPred] [inst_10 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_12 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Std.IterM m β}
  {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← f b
          pure (g d c))
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.mapM f it) ⦃ Q; eQ ⦄
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.instCountableSigmaNat : ∀ {L : FirstOrder.Language} {α : Type u'} [Countable α] [Countable L.Symbols],
  Countable ((n : ℕ) × L.BoundedFormula α n)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_list_prod : ∀ {m : Type u_2} {α : Type v} [inst : Semiring α] [inst_1 : StarRing α] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  (l : List (Matrix m m α)), l.prod.conjTranspose = (List.map Matrix.conjTranspose l).reverse.prod
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S.eq_3 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.S R (Int.ofNat n.succ.succ) =
    Polynomial.X * Polynomial.Chebyshev.S R (↑n + 1) - Polynomial.Chebyshev.S R ↑n
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isPrincipal : ∀ {K : Type u_4} [inst : Field K] {R : Type u_5} [inst_1 : CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
  [inst_4 : Algebra R K] [IsFractionRing R K] (I : FractionalIdeal (nonZeroDivisors R) K), (↑I).IsPrincipal
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.brecOn.eq : ∀ {motive : Mathlib.Tactic.ITauto.Proof → Sort u} (t : Mathlib.Tactic.ITauto.Proof)
  (F_1 : (t : Mathlib.Tactic.ITauto.Proof) → Mathlib.Tactic.ITauto.Proof.below t → motive t),
  Mathlib.Tactic.ITauto.Proof.brecOn t F_1 = F_1 t (Mathlib.Tactic.ITauto.Proof.brecOn.go t F_1).2
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instPartialOrder : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → PartialOrder (LieSubmodule R L M)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- Let `f`, `g` be power series over `A`, `I` be an ideal of `A`,
`PowerSeries.IsWeierstrassDivisionAt f g q r I` is a `Prop` which asserts that a power series
`q` and a polynomial `r` of degree `< n` satisfy `f = g * q + r`, where `n` is the order of the
image of `g` in `(A / I)⟦X⟧` (defined to be zero if such image is zero, in which case
it's mathematically not considered).  -/
PowerSeries.IsWeierstrassDivisionAt : {A : Type u_1} → [inst : CommRing A] → PowerSeries A → PowerSeries A → PowerSeries A → Polynomial A → Ideal A → Prop