mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Perfection
PerfectionMap.comp_map : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {S : Type u₂} [inst_6 : CommSemiring S]
  [inst_7 : CharP S p] {Q : Type u₄} [inst_8 : CommSemiring Q] [inst_9 : CharP Q p] [inst_10 : PerfectRing Q p]
  {π : P →+* R} (m : PerfectionMap p π) {σ : Q →+* S} (n : PerfectionMap p σ) (φ : R →+* S),
  σ.comp (PerfectionMap.map p m n φ) = φ.comp π
-- Mathlib.Order.Category.Frm
_private.Mathlib.Order.Category.Frm.0.Frm.Hom.mk.sizeOf_spec : ∀ {X Y : Frm} (hom' : FrameHom ↑X ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNat_eq_sMod : ∀ (p k : ℕ), 2 ≤ p → ↑(LucasLehmer.norm_num_ext.sModNat (2 ^ p - 1) k) = LucasLehmer.sMod p k
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_union : ∀ {α : Type u_2} [inst : Sub α] {s t₁ t₂ : Set α}, s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)
-- Mathlib.NumberTheory.SelbergSieve
/-- Extension for the `positivity` tactic: `BoundingSieve.weights`.  -/
Mathlib.Meta.Positivity.evalBoundingSieveWeights : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The level for objects.  -/
Mathlib.Tactic.Bicategory.Context.level₀ : Mathlib.Tactic.Bicategory.Context → Lean.Level
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.i_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y} (self : HomotopicalAlgebra.FibrantBrownFactorization f),
  CategoryTheory.CategoryStruct.comp self.i self.r = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.CommSq.cube_lemma_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M000 M001 M010 M011 M100 M101 M110 M111 : C}
  (f00x : M000 ⟶ M001) (f01x : M010 ⟶ M011) (f10x : M100 ⟶ M101) (f11x : M110 ⟶ M111) (f0x0 : M000 ⟶ M010)
  (f0x1 : M001 ⟶ M011) (f1x0 : M100 ⟶ M110) (f1x1 : M101 ⟶ M111) (fx00 : M000 ⟶ M100) (fx01 : M001 ⟶ M101)
  (fx10 : M010 ⟶ M110) (fx11 : M011 ⟶ M111),
  CategoryTheory.CommSq f0x0 f00x f01x f0x1 →
    CategoryTheory.CommSq f1x0 f10x f11x f1x1 →
      CategoryTheory.CommSq fx00 f00x f10x fx01 →
        CategoryTheory.CommSq fx10 f01x f11x fx11 →
          CategoryTheory.CommSq f0x1 fx01 fx11 f1x1 →
            ∀ [CategoryTheory.Mono f11x], CategoryTheory.CommSq f0x0 fx00 fx10 f1x0
-- Mathlib.Algebra.Group.Defs
one_mul : ∀ {M : Type u} [inst : MulOneClass M] (a : M), 1 * a = a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.length_rotate : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (c : G.Walk v v) (u : V) (h : u ∈ c.support),
  (c.rotate u h).length = c.length
-- Init.Data.Vector.Zip
Vector.zipWith_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n m : ℕ} {xs : Vector γ n} {ys : Vector γ m} {f : α → β → γ}
  {as : Vector α (n + m)} {bs : Vector β (n + m)},
  Vector.zipWith f as bs = xs ++ ys ↔
    ∃ as₁ as₂ bs₁ bs₂, as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = Vector.zipWith f as₁ bs₁ ∧ ys = Vector.zipWith f as₂ bs₂
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The tensor product of R-algebras is commutative, up to algebra isomorphism.
 -/
Algebra.TensorProduct.comm : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] → [inst_4 : Algebra R B] → TensorProduct R A B ≃ₐ[R] TensorProduct R B A
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_max?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → t.max?.isSome = true
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.map_one : ∀ {A : Type u_1} {B : Type u_2} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], PontryaginDual.map 1 = 1
-- Mathlib.Combinatorics.Graph.Basic
/-- The binary incidence predicate, stating that `x` and `y` are the ends of an edge `e`.
If `G.IsLink e x y` then we refer to `e` as `edge` and `x` and `y` as `left` and `right`.  -/
Graph.IsLink : {α : Type u_3} → {β : Type u_4} → Graph α β → β → α → α → Prop
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  Set.range ⇑(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f) =
    Set.range ⇑f ∩ Set.range ⇑g
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.not_isRegular_aleph_add_one : ∀ (o : Ordinal.{u_1}), ¬(Cardinal.aleph (o + 1)).IsSingular
-- Mathlib.Control.Traversable.Lemmas
Traversable.pureTransformation_apply : ∀ (F : Type u → Type u) [inst : Applicative F] [inst_1 : LawfulApplicative F] {α : Type u} (x : id α),
  (fun {α} => (Traversable.PureTransformation F).app α) x = pure x
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α}, Multipliable f → Multipliable fun b => ∏' (c : γ b), f ⟨b, c⟩
-- Mathlib.RingTheory.Algebraic.Basic
/-- An element `x` is transcendental over `R` if and only if the map `Polynomial.aeval x`
is injective. This is similar to `algebraicIndependent_iff_injective_aeval`.  -/
transcendental_iff_injective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A},
  Transcendental R x ↔ Function.Injective ⇑(Polynomial.aeval x)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.brecOn.eq : ∀ {motive : ONote → Sort u} (t : ONote) (F_1 : (t : ONote) → ONote.below t → motive t),
  ONote.brecOn t F_1 = F_1 t (ONote.brecOn.go t F_1).2
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.C_dvd_iff_dvd_coeff : ∀ {R : Type u} [inst : Semiring R] (r : R) (φ : Polynomial R), Polynomial.C r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.mk : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_2} →
        {H : Type u_3} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  {I : ModelWithCorners ℝ E H} →
                    (M : Type u) →
                      [topSpaceM : TopologicalSpace M] →
                        [chartedSpace : ChartedSpace H M] →
                          [isManifold : IsManifold I k M] →
                            [compactSpace : CompactSpace M] →
                              [boundaryless : BoundarylessManifold I M] →
                                (f : M → X) → Continuous f → SingularManifold X k I
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The universal morphism from a colimit cocone to any other cocone.  -/
CategoryTheory.Limits.IsColimit.descCoconeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit t → (s : CategoryTheory.Limits.Cocone F) → t ⟶ s
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeSubtypeEquivSubtype_symm_apply_coe_coe : ∀ {α : Type u_9} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) (a : Subtype q),
  ↑↑((Equiv.subtypeSubtypeEquivSubtype h).symm a) = ↑a
-- Mathlib.Data.Nat.Choose.Sum
Int.alternating_sum_range_choose_of_ne : ∀ {n : ℕ}, n ≠ 0 → ∑ m ∈ Finset.range (n + 1), (-1) ^ m * ↑(n.choose m) = 0
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Path.reverse_toPath : ∀ {V : Type u_2} [inst : Quiver V] [inst_1 : Quiver.HasReverse V] {a b : V} (f : a ⟶ b),
  f.toPath.reverse = (Quiver.reverse f).toPath
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isColocal_adj_counit_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : G ⊣ F) [G.Full] [G.Faithful] (X : C),
  CategoryTheory.ObjectProperty.isColocal (fun x => x ∈ Set.range G.obj) (adj.counit.app X)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.div_ratCast : ∀ {x : ℝ}, Irrational x → ∀ {q : ℚ}, q ≠ 0 → Irrational (x / ↑q)
-- Mathlib.Topology.Separation.GDelta
Topology.IsEmbedding.t6Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T6Space Y] {e : X → Y},
  Topology.IsEmbedding e → T6Space X
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_int32ToInt : ∀ (x : Int32), ISize.ofIntLE x.toInt ⋯ ⋯ = x.toISize
-- Mathlib.Data.Multiset.Filter
/-- `Filter p s` returns the elements in `s` (with the same multiplicities)
which satisfy `p`, and removes the rest.  -/
Multiset.filter : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Multiset α → Multiset α
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_injective : ∀ {M : Type u_2} [inst : Add M], Function.Injective AddSubsemigroup.op
-- Mathlib.CategoryTheory.Skeletal
/-- The functor `F` is an equivalence  -/
CategoryTheory.IsSkeletonOf.eqv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor D C}, CategoryTheory.IsSkeletonOf C D F → F.IsEquivalence
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.le_dirac_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α}, s.indicator 1 a ≤ (MeasureTheory.Measure.dirac a) s
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.symbol : ℕ → Lean.Meta.Grind.AttrKind
-- Std.Time.Date.PlainDate
/-- The year component of the date. It is represented as an `Offset` type from `Year`.  -/
Std.Time.PlainDate.year : Std.Time.PlainDate → Std.Time.Year.Offset
-- Lean.Elab.Do.Basic
/-- We inferred the code is syntactically dead and don't need to elaborate it at all.  -/
Lean.Elab.Do.CodeLiveness.deadSyntactically : Lean.Elab.Do.CodeLiveness
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- The map makes the triangle with the two natural transformations commute  -/
CategoryTheory.Limits.IsWeakLimit.fac : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (self : CategoryTheory.Limits.IsWeakLimit t) (s : CategoryTheory.Limits.Cone F) (j : J),
  CategoryTheory.CategoryStruct.comp (self.lift s) (t.π.app j) = s.π.app j
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.colimitCocone_ι_app : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] [inst_2 : Small.{w, max w u} (AddCommGrpCat.Colimits.Quot F)] (j : J),
  (AddCommGrpCat.Colimits.colimitCocone F).ι.app j =
    AddCommGrpCat.ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (AddCommGrpCat.Colimits.Quot.ι F j))
-- Init.Data.Rat.Lemmas
Rat.normalize_mul_normalize : ∀ (n₁ n₂ : ℤ) {d₁ d₂ : ℕ} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0),
  Rat.normalize n₁ d₁ z₁ * Rat.normalize n₂ d₂ z₂ = Rat.normalize (n₁ * n₂) (d₁ * d₂) ⋯
-- Lean.Meta.Tactic.Simp.Types
/-- Converts `Simp.Config` into `Meta.ConfigWithKey` used for indexing.
 -/
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.mkIndexConfig : Lean.Meta.Simp.Config → Lean.MetaM Lean.Meta.ConfigWithKey
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.StateStack.mk.inj : ∀ {α β σ : Type} {stateStack : List (Lean.ScopedEnvExtension.State σ)}
  {scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β} {newEntries : List (Lean.ScopedEnvExtension.Entry α)}
  {stateStack_1 : List (Lean.ScopedEnvExtension.State σ)} {scopedEntries_1 : Lean.ScopedEnvExtension.ScopedEntries β}
  {newEntries_1 : List (Lean.ScopedEnvExtension.Entry α)},
  { stateStack := stateStack, scopedEntries := scopedEntries, newEntries := newEntries } =
      { stateStack := stateStack_1, scopedEntries := scopedEntries_1, newEntries := newEntries_1 } →
    stateStack = stateStack_1 ∧ scopedEntries = scopedEntries_1 ∧ newEntries = newEntries_1
-- Init.Data.BitVec.Bitblast
/-- Unsigned addition overflows iff the final carry bit of the addition circuit is `true`.  -/
BitVec.uaddOverflow_eq : ∀ {w : ℕ} (x y : BitVec w), x.uaddOverflow y = (BitVec.setWidth (w + 1) x + BitVec.setWidth (w + 1) y).msb
-- Init.Data.Order.Ord
List.instReflCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp], Std.ReflCmp (List.compareLex cmp)
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.dual : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β},
  StrictConvexOn 𝕜 s f → StrictConcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)
-- Mathlib.Topology.LocallyFinsupp
/-- Present a function with with finite support as a finsum of singleton indicator functions.
 -/
Function.locallyFinsuppWithin.sum_apply_smul_single_eq_self : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : DecidableEq X] [inst_2 : AddCommMonoid Y]
  {U : Set X} {F : Function.locallyFinsuppWithin U Y},
  F.support.Finite →
    ∑ᶠ (x : X), Function.locallyFinsuppWithin.restrict (Function.locallyFinsuppWithin.single x (F x)) ⋯ = F
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_injective_isMulCommutative : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) {f : G' →* G},
  Function.Injective ⇑f → ∀ [IsMulCommutative ↥H], IsMulCommutative ↥(Subgroup.comap f H)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_comp_comm : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N]
  [Module.Finite R N],
  (LinearMap.llcomp R M N M).compr₂ (LinearMap.trace R M) = (LinearMap.llcomp R N M N).flip.compr₂ (LinearMap.trace R N)
-- Mathlib.Data.NNReal.Defs
NNReal.instSMulPosStrictMono : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : MulAction ℝ α] [SMulPosStrictMono ℝ α],
  SMulPosStrictMono NNReal α
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensorHom_comp_tensorHom : ∀ {R : Type u} [inst : CommSemiring R] {X₁ Y₁ Z₁ : SemimoduleCat R} {X₂ Y₂ Z₂ : SemimoduleCat R} (f₁ : X₁ ⟶ Y₁)
  (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp (SemimoduleCat.MonoidalCategory.tensorHom f₁ f₂)
      (SemimoduleCat.MonoidalCategory.tensorHom g₁ g₂) =
    SemimoduleCat.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
      (CategoryTheory.CategoryStruct.comp f₂ g₂)
-- Init.Data.Nat.Basic
Nat.sub_lt_of_lt : ∀ {a b c : ℕ}, a < c → a - b < c
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.unit_mul_pow_congr_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {p q : R},
  Irreducible p → Irreducible q → ∀ (u v : Rˣ) (m n : ℕ), ↑u * p ^ m = ↑v * q ^ n → m = n
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Embeds an element of `α` into `FreeMonoid α` as a singleton list.  -/
FreeMonoid.of : {α : Type u_1} → α → FreeMonoid α
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Spec.fromSpecStalk_eq : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)),
  (AlgebraicGeometry.Spec R).fromSpecStalk x =
    AlgebraicGeometry.Spec.map
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
        ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial))
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
_private.Mathlib.Analysis.CStarAlgebra.Module.Constructions.0.WithCStarModule.antilipschitzWith_card_equiv_pi_aux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [inst_7 : StarOrderedRing A],
  AntilipschitzWith ↑(Fintype.card ι) ⇑(WithCStarModule.equiv A ((i : ι) → E i))
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.instIsCyclicSubtypeMemSubgroupOfFactPrime : ∀ {G : Type u_1} [inst : Group G] [IsZGroup G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), IsCyclic ↥↑P
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_degree_eq_one : ∀ {R : Type u_1} [inst : DivisionSemiring R] {f : Polynomial R}, f.degree = 1 → f.Splits
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The `MonoidHom` from the preimage of a `Submonoid` to itself.  -/
MonoidHom.submonoidComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → (f : M →* N) → (N' : Submonoid N) → ↥(Submonoid.comap f N') →* ↥N'
-- Mathlib.Data.FunLike.IsApply
IsNatCastApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : FunLike F α α] [inst_1 : NatCast F] [inst_2 : SMul ℕ α],
  (∀ (n : ℕ) (x : α), ↑n x = n • x) → IsNatCastApply F α
-- Lean.Meta.LitValues
/-- Return `some v` if `e` is a `Float32` literal: an `OfScientific` or `OfNat` application, or `Neg.neg`
of either (e.g. `-1.5`).
 -/
Lean.Meta.getFloat32Value? : Lean.Expr → Lean.MetaM (Option Float32)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.disjoint_support_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {a : σ →₀ ℕ} {p : MvPolynomial σ R} {s : R},
  a ∉ p.support → s ≠ 0 → Disjoint ((MvPolynomial.monomial a) s).support p.support
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the value for the key `k`, or panics if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.get! : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → [Std.LawfulEqOrd α] → Std.DTreeMap.Internal.Impl α β → (k : α) → [Inhabited (β k)] → β k
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_of_contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α}, (Std.ExtHashMap.map f m).contains k = true → m.contains k = true
-- Mathlib.Tactic.TFAE
/-- Uses depth-first search to find a path from `P` to `P'`.  -/
Mathlib.Tactic.TFAE.dfs : Array (ℕ × ℕ × Lean.Expr) →
  Array Q(Prop) → ℕ → ℕ → (P P' : Q(Prop)) → Q(«$P») → StateT (Std.HashSet ℕ) Lean.MetaM Q(«$P'»)
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.prime_C_iff : ∀ {R : Type u} (σ : Type v) [inst : CommRing R] {r : R}, Prime (MvPolynomial.C r) ↔ Prime r
-- Lean.Parser.Command
Lean.Parser.Command.open.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_eq_compl_singleton : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, G.neighborSet v = {v}ᶜ ↔ G.IsUniversal v
-- Mathlib.Order.Disjoint
disjoint_sup_right : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α},
  Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c
-- Mathlib.Lean.Meta.KAbstractPositions
/-- Determine whether the result of abstracting `subExpr` from `e` at position `pos` results
in a well-typed expression. This is important if you want to rewrite at this position.

Here is an example of what goes wrong with an ill-typed kabstract result:

```
example (h : [5] ≠ []) : List.getLast [5] h = 5 := by
  rw [show [5] = [5] from rfl] -- tactic 'rewrite' failed, motive is not type correct
```
 -/
Lean.Meta.kabstractIsTypeCorrect : Lean.Expr → Lean.Expr → Lean.SubExpr.Pos → Lean.MetaM Bool
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of the reverse direction of `Set.Finite.toFinset_subset_toFinset`. -/
Set.Finite.toFinset_mono : ∀ {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite}, s ⊆ t → hs.toFinset ⊆ ht.toFinset
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) {hc : k' ∈ m.alter k f},
  (m.alter k f).get k' hc = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_6 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.clz with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_6 ()
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- A base of a root pairing.

For reduced root pairings this definition is equivalent to the usual definition appearing in the
informal literature but not for non-reduced root pairings it is more restrictive. See the module
doc string for further remarks.

See also `RootPairing.Base.mk'`.  -/
RootPairing.Base : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → Type u_1
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_succ_of_lt : ∀ {n : ℕ} (p i : Fin n) (h : i < p), p.predAbove i.succ = i.succ.castPred ⋯
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.mk : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} →
                {L L' : Φ.LeftResolution X₂} →
                  (f : L.X₁ ⟶ L'.X₁) →
                    autoParam (CategoryTheory.CategoryStruct.comp (Φ.functor.map f) L'.w = L.w)
                        CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm._autoParam →
                      L.Hom L'
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_mul_opow_omega0_add : ∀ {a c : Ordinal.{u_1}} (b : Ordinal.{u_1}),
  0 < a →
    0 < c →
      c ≤ a ^ Ordinal.omega0 →
        Ordinal.nfp (fun x => a * x) (a ^ Ordinal.omega0 * b + c) = a ^ Ordinal.omega0 * Order.succ b
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.instZPow : {𝕜 : Type u_1} → [inst : NormedDivisionRing 𝕜] → Pow ↑(Metric.sphere 0 1) ℤ
-- Std.Time.DateTime.Timestamp
/-- Adds an `Hour.Offset` to the given `Timestamp`.
 -/
Std.Time.Timestamp.addHours : Std.Time.Timestamp → Std.Time.Hour.Offset → Std.Time.Timestamp
-- Mathlib.Tactic.NormNum.Result
/-- The element is equal to the coercion of the integer.  -/
Mathlib.Meta.NormNum.IsInt.out : ∀ {α : Type u} [inst : Ring α] {a : α} {n : ℤ}, Mathlib.Meta.NormNum.IsInt a n → a = ↑n
-- Mathlib.Order.UpperLower.Closure
upperBounds_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, upperBounds ↑(lowerClosure s) = upperBounds s