mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.Ord
Std.LawfulEqCmp.compare_beq_iff_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] {a b : α}, (cmp a b == Ordering.eq) = true ↔ a = b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [toMonoidalCategory : CategoryTheory.MonoidalCategory C] →
      (isTerminalTensorUnit : CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
        (fst : (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ X) →
          (snd : (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Y) →
            autoParam
                (∀ (X Y : C),
                  fst X Y =
                    CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (isTerminalTensorUnit.from Y))
                      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
                CategoryTheory.SemiCartesianMonoidalCategory.fst_def._autoParam →
              autoParam
                  (∀ (X Y : C),
                    snd X Y =
                      CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (isTerminalTensorUnit.from X) Y)
                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom)
                  CategoryTheory.SemiCartesianMonoidalCategory.snd_def._autoParam →
                CategoryTheory.SemiCartesianMonoidalCategory C
-- Mathlib.Tactic.FunProp.Mor
/-- Is `e` morphism application?  -/
Mathlib.Meta.FunProp.Mor.isMorApp? : Lean.Expr → Lean.MetaM (Option Mathlib.Meta.FunProp.Mor.App)
-- Mathlib.SetTheory.Lists
Lists.Equiv.below.refl : ∀ {α : Type u_1} {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop}
  {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop} (l : Lists α), ⋯.below
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.disjoint_map : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ {p q : Submodule R M}, Disjoint p q → Disjoint (Submodule.map f p) (Submodule.map f q)
-- Init.Data.SInt.Bitwise
Int8.toInt_not : ∀ (a : Int8), (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 8)
-- Init.MetaTypes
Lean.Meta.instBEqTransparencyMode : BEq Lean.Meta.TransparencyMode
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.map_inl : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn) (n : N₁),
  (SemidirectProduct.map fn fg h) (SemidirectProduct.inl n) = SemidirectProduct.inl (fn n)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_ofRepr : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (e : M ≃ₗ[R] ι →₀ R), ⇑{ repr := e } = fun i => e.symm fun₀ | i => 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toList_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → Bool},
  (Std.TreeMap.filter f t).toList = List.filter (fun p => f p.1 p.2) t.toList
-- Init.Data.List.Sublist
List.IsInfix.filter : ∀ {α : Type u_1} (p : α → Bool) ⦃l₁ l₂ : List α⦄, l₁ <:+: l₂ → List.filter p l₁ <:+: List.filter p l₂
-- Mathlib.Logic.Encodable.Basic
/-- The quotient of an encodable space by a decidable equivalence relation is encodable.  -/
encodableQuotient : {α : Type u_1} → {s : Setoid α} → [DecidableRel fun x1 x2 => x1 ≈ x2] → [Encodable α] → Encodable (Quotient s)
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instCompactSpaceQuotientAddSubgroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [CompactSpace G] (N : AddSubgroup G),
  CompactSpace (G ⧸ N)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Drop the augmentation.  -/
CategoryTheory.SimplicialObject.Augmented.drop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C) (CategoryTheory.SimplicialObject C)
-- Mathlib.Data.Set.Prod
Set.pi_subset_pi_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  s.pi t₁ ⊆ s.pi t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ s.pi t₁ = ∅
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairMap.eq_1 : ∀ (σ : Type u_1) [inst : DecidableEq σ] (t : Finset σ × σ),
  MvPolynomial.NewtonIdentities.pairMap✝ σ t =
    if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (Finset.cons t.2 t.1 h, t.2)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_max : ∀ {x y p : ℝ}, 0 ≤ x → 0 ≤ y → 0 ≤ p → max x y ^ p = max (x ^ p) (y ^ p)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_eq_none : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α},
  a ∉ m → m.get? a = none
-- Init.Prelude
/-- An array of syntax elements that alternate with the given separator. Each syntax element has a kind
drawn from `ks`.

Separator arrays result from repetition operators such as `,*`.
[Coercions](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=coercions) to and from `Array (TSyntax ks)` insert or remove
separators as required. The untyped equivalent is `Lean.Syntax.SepArray`.
 -/
Lean.Syntax.TSepArray : Lean.SyntaxNodeKinds → String → Type
-- Init.Data.UInt.Lemmas
UInt32.ofNat_bitVecToNat : ∀ (n : BitVec 32), UInt32.ofNat n.toNat = { toBitVec := n }
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_mono : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Preorder M] [AddLeftMono M],
  Monotone fun f => ∑ i, f i
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Algebra.IsAlgebraic.isTranscendenceBasis_of_le_trdeg : ∀ (R : Type u_1) {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [NoZeroDivisors A]
  [FaithfulSMul R A] {ι : Type w} (x : ι → A) [Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A],
  Algebra.trdeg R A < Cardinal.aleph0 → Cardinal.mk ι ≤ Algebra.trdeg R A → IsTranscendenceBasis R x
-- Lean.Meta.WHNF
Lean.Meta.mkSmartUnfoldingNameFor : Lean.Name → Lean.Name
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Structure.ext_iff : ∀ {L : FirstOrder.Language} {M : Type w} {x y : L.Structure M},
  x = y ↔
    @FirstOrder.Language.Structure.funMap L M x = @FirstOrder.Language.Structure.funMap L M y ∧
      @FirstOrder.Language.Structure.RelMap L M x = @FirstOrder.Language.Structure.RelMap L M y
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`.  -/
EuclideanGeometry.oangle_left_eq_arcsin_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
    EuclideanGeometry.oangle p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))
-- Init.Data.UInt.Lemmas
UInt8.mul_add : ∀ {a b c : UInt8}, a * (b + c) = a * b + a * c
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The alternating group on 3 letters or more acts transitively.  -/
alternatingGroup.isPretransitive_of_three_le_card : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α],
  3 ≤ Nat.card α → MulAction.IsPretransitive (↥(alternatingGroup α)) α
-- Mathlib.Algebra.Ring.Aut
/-- Monoid homomorphism from ring automorphisms to multiplicative automorphisms.  -/
RingAut.toMulAut : (R : Type u_1) → [inst : Mul R] → [inst_1 : Add R] → RingAut R →* MulAut R
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.IsStableUnderBaseChange] {X : C} (E E_1 : J.ZeroHypercover X) (e_E : E = E_1) {Y Z : C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasPullback f g]
  [inst_3 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)],
  E.pullbackCoverOfLeft f g = E_1.pullbackCoverOfLeft f g
-- Mathlib.Algebra.Group.Action.Defs
MulAction.toSemigroupAction : {α : Type u_9} → {β : Type u_10} → {inst : Monoid α} → [self : MulAction α β] → SemigroupAction α β
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.IsInt.raw_refl : ∀ (n : ℤ), Mathlib.Meta.NormNum.IsInt n n
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts_supportsStmt : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Λ] {M : Λ → Turing.TM1.Stmt Γ Λ σ} {S : Finset Λ}
  {q : Turing.TM1.Stmt Γ Λ σ}, Turing.TM1.Supports M S → some q ∈ Turing.TM1.stmts M S → Turing.TM1.SupportsStmt S q
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_eq_restrict_biUnion_finset_iff : ∀ {α : Type u_2} {δ : Type u_4} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α)
  (t : Finset ι) (f g : α → δ), f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_toIsometryEquiv : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e.toIsometryEquiv = ⇑e
-- Mathlib.RingTheory.PowerSeries.WellKnown
/-- Power series for the cosine function at zero.  -/
PowerSeries.cos : (A : Type u_1) → [inst : Ring A] → [Algebra ℚ A] → PowerSeries A
-- Mathlib.Data.List.Defs
List.instSDiffOfDecidableEq_mathlib : {α : Type u_1} → [DecidableEq α] → SDiff (List α)
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IterM.instForMOfIteratorLoop : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m n] → [Monad n] → [MonadLiftT m n] → ForM n (Std.IterM m β) β
-- Mathlib.Algebra.Group.Prod
/-- Given monoids `M`, `N`, the natural inclusion homomorphism from `M` to `M × N`.  -/
MonoidHom.inl : (M : Type u_3) → (N : Type u_4) → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M →* M × N
-- Lean.Util.Path
Lean.realPathNormalized : System.FilePath → IO System.FilePath
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂).getKey? k = none
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence] [inst_5 : CategoryTheory.HasWeakSheafify J A]
  {P : CategoryTheory.Functor Dᵒᵖ A} {Q₁ Q₂ : CategoryTheory.Sheaf K A}
  (f : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁) (g : Q₁ ⟶ Q₂),
  (CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G)
      (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) f)
      g.hom
-- Mathlib.Order.Disjoint
codisjoint_iff : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b ↔ a ⊔ b = ⊤
-- Init.Data.Vector.Lemmas
_private.Init.Data.Vector.Lemmas.0.Vector.toArray_mapM_go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : α → m β}
  {xs : Vector α n} {i : ℕ} (h : i ≤ n) {acc : Vector β i},
  Vector.toArray <$> Vector.mapM.go✝ f xs i h acc = Array.mapM.map✝ f xs.toArray i acc.toArray
-- Mathlib.Order.Concept
Order.IsExtent.iInter : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Set α),
  (∀ (i : ι), Order.IsExtent r (f i)) → Order.IsExtent r (⋂ i, f i)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.not_vle_one_zero : ∀ {R : Type u_1} {inst : Semiring R} [self : ValuativeRel R], ¬1 ≤ᵥ 0
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.invLimEquiv.congr_simp : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι]
  {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} {equiv equiv_1 : (j : ↑(Set.Iio i)) → F ↑j ≃ InverseSystem.piLT X ↑j}
  (e_equiv : equiv = equiv_1) (nat : InverseSystem.IsNatEquiv f equiv),
  InverseSystem.invLimEquiv nat = InverseSystem.invLimEquiv ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toArray_rcc_eq : ∀ {m n i : ℕ}, ((m...=n).toArray[i]?.isSome = true) = (i < n + 1 - m)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_ground : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E), (M.map f hf).E = f '' M.E
-- Mathlib.Topology.EMetricSpace.Defs
edist_congr : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {w x y z : α}, edist w x = 0 → edist y z = 0 → edist w y = edist x z
-- Aesop.Stats.Basic
Aesop.ForwardStateStats.mk.injEq : ∀ (ruleStateStats ruleStateStats_1 : Array Aesop.ForwardRuleStateStats),
  ({ ruleStateStats := ruleStateStats } = { ruleStateStats := ruleStateStats_1 }) = (ruleStateStats = ruleStateStats_1)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
one_le_padicValNat_of_dvd : ∀ {p n : ℕ} [hp : Fact (Nat.Prime p)], n ≠ 0 → p ∣ n → 1 ≤ padicValNat p n
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.of_symm_image_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  ↑e.symm '' (e.target ∩ t) = e.source ∩ s → e.IsImage s t
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCover_U : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (i : 𝒰.I₀), (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).U i = 𝒰.X i
-- Mathlib.Logic.Basic
xor_iff_or_and_not_and : ∀ (a b : Prop), Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.lift_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (f : F' ⟶ F)
  {G : CategoryTheory.Subfunctor F} (hf : CategoryTheory.Subfunctor.range f ≤ G) (U : C),
  (CategoryTheory.Subfunctor.lift f hf).app U =
    TypeCat.ofHom fun x => ⟨(CategoryTheory.ConcreteCategory.hom (f.app U)) x, ⋯⟩
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_insertListConst_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l : List ((_ : α) × β)}
  {toInsert : List (α × β)} {k : α} {not_contains : (List.map Prod.fst toInsert).contains k = false}
  {h : Std.Internal.List.containsKey k (Std.Internal.List.insertListConst l toInsert) = true},
  Std.Internal.List.getValue k (Std.Internal.List.insertListConst l toInsert) h = Std.Internal.List.getValue k l ⋯
-- Mathlib.Data.DFinsupp.BigOperators
AddMonoidHom.coe_dfinsuppSumAddHom : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : AddZeroClass R]
  [inst_2 : AddCommMonoid S] [inst_3 : (i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i →+ R →+ S),
  ⇑((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => (AddMonoidHom.coeFn R S).comp (g i)) f
-- Mathlib.Data.List.Basic
List.map_eq_map : ∀ {α β : Type u_2} (f : α → β) (l : List α), f <$> l = List.map f l
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_natCast : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A} (n : ℕ), (↑n).val = ↑n
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching a real from the left, `deriv` version  -/
deriv.lhopital_zero_nhdsLT : ∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Iio a), DifferentiableAt ℝ f x) →
    (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Iio a), deriv g x ≠ 0) →
      Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds 0) →
        Filter.Tendsto g (nhdsWithin a (Set.Iio a)) (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin a (Set.Iio a)) l →
            Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Iio a)) l
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Option.elim.match_1.splitter : {α : Type u_1} →
  {β : Sort u_3} →
    (motive : Option α → β → (α → β) → Sort u_2) →
      (x : Option α) →
        (x_1 : β) →
          (x_2 : α → β) →
            ((x : α) → (x_3 : β) → (f : α → β) → motive (some x) x_3 f) →
              ((y : β) → (x : α → β) → motive none y x) → motive x x_1 x_2
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_coeff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {i : ℕ},
  p.integralNormalization.coeff i = if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_sdiff : ∀ {x y z : ZFSet.{u}}, z ∈ x \ y ↔ z ∈ x ∧ z ∉ y
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.below.right : ∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop}, Nat.Primrec.below Nat.Primrec.right
-- Mathlib.Data.Option.Basic
Option.mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} {o : Option α}, y ∈ Option.map f o ↔ ∃ x ∈ o, f x = y
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} → (obj : C) → P obj → P.FullSubcategory
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.match_3.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (lrk : α) →
        (lrv : β lrk) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_4 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (size : ℕ) (lrk : α) (lrv : β lrk) (l r : Std.DTreeMap.Internal.Impl α β),
  ll = Std.DTreeMap.Internal.Impl.leaf →
    lr = Std.DTreeMap.Internal.Impl.inner size lrk lrv l r →
      (match ll, lr with
        | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf => h_1 ()
        | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r => h_2 size lrk lrv l r
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_3 size k v l r
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
          h_4 size k v l r lrs lrk lrv lrl lrr) ≍
        h_2 size lrk lrv l r
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_eq_zero_of_degree_lt : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.degree < ↑n → p.coeff n = 0
-- Std.Time.DateTime
/-- Getter for the `Hour` inside of a `DateTime`
 -/
Std.Time.DateTime.hour : Std.Time.DateTime → Std.Time.Hour.Ordinal
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensLegend.tokenModifiers : Lean.Lsp.SemanticTokensLegend → Array String
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
fderivWithin.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x →
    f x ≠ 0 → UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => Real.log (f x)) s x = (f x)⁻¹ • fderivWithin ℝ f s x
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.whiskering_linearYoneda₂ : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C],
  (CategoryTheory.linearYoneda R C).comp
      ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (ModuleCat R) AddCommGrpCat).obj
        (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)) =
    CategoryTheory.preadditiveYoneda
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- Extract a real bilinear form from an operator `T`,
by taking the pairing `fun x ↦ re ⟪T x, x⟫`.  -/
ContinuousLinearMap.reApplyInnerSelf : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →L[𝕜] E) → E → ℝ
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_inv_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.unmop =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.unmop).inv
-- Mathlib.Analysis.Analytic.Within
/-- `AnalyticWithinAt` is trivial if `{x} ∈ 𝓝[s] x`  -/
analyticWithinAt_of_singleton_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E},
  {x} ∈ nhdsWithin x s → AnalyticWithinAt 𝕜 f s x
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.TreeMap.Raw.maxKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α
-- Mathlib.GroupTheory.Coset.Basic
rightAddCoset_assoc : ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α),
  AddOpposite.op b +ᵥ AddOpposite.op a +ᵥ s = AddOpposite.op (a + b) +ᵥ s
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.comapSMul_single : ∀ {G : Type u_2} {M : Type u_6} {α : Type u_7} [inst : Monoid G] [inst_1 : AddCommMonoid M] [inst_2 : MulAction G α]
  (g : G) (a : α) (b : M), g • SkewMonoidAlgebra.single a b = SkewMonoidAlgebra.single (g • a) b
-- Mathlib.Data.Set.Card
Set.encard_le_card : ∀ {α : Type u_1} {s : Set α}, s.encard ≤ ENat.card α
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.max!.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((x : α) → motive (some x)) → motive x
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_one : ⌈1⌉ₑ = 1