mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
/-- A strict pseudofunctor `F` between bicategories `B` and `C` is a
pseudofunctor `F` from `B` to `C` such that `mapId` and `mapComp` are given by `eqToIso _`.  -/
CategoryTheory.StrictPseudofunctor : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.var.inj : ∀ {fvarId fvarId_1 : Lean.FVarId},
  Lean.Meta.Match.Pattern.var fvarId = Lean.Meta.Match.Pattern.var fvarId_1 → fvarId = fvarId_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go aig distance curr acc).aig.decls.size
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.instDecidablePredMemSetSupport : {V : Type u_1} → [Fintype V] → {G : SimpleGraph V} → [DecidableRel G.Adj] → DecidablePred fun x => x ∈ G.support
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.Action.applyCases? : Lean.Meta.Grind.Goal →
  Lean.FVarId → Lean.Meta.Grind.ActionCont → Lean.Meta.Grind.GrindM (Option Lean.Meta.Grind.ActionResult)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.Agree.below.intro : ∀ {F : PFunctor.{uA, uB}}
  {motive :
    {n : ℕ} →
      (a : PFunctor.Approx.CofixA F n) → (a_1 : PFunctor.Approx.CofixA F (n + 1)) → PFunctor.Approx.Agree a a_1 → Prop}
  {n : ℕ} {a : F.A} (x : F.B a → PFunctor.Approx.CofixA F n) (x' : F.B a → PFunctor.Approx.CofixA F (n + 1))
  (a_1 : ∀ (i : F.B a), PFunctor.Approx.Agree (x i) (x' i)),
  (∀ (i : F.B a), PFunctor.Approx.Agree.below ⋯) →
    (∀ (i : F.B a), motive (x i) (x' i) ⋯) → PFunctor.Approx.Agree.below ⋯
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.isOpenEmbedding_obj_top : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X), ⋯.functor.obj ⊤ = U
-- Mathlib.Topology.Covering.Basic
/-- A constructor for `IsCoveringMap` when there are both empty and nonempty fibers.  -/
IsCoveringMap.mk' : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (F : X → Type u_3)
  [inst_2 : (x : X) → TopologicalSpace (F x)] [∀ (x : X), DiscreteTopology (F x)]
  (t : (x : X) → x ∈ Set.range f → { t // x ∈ t.baseSet }), IsClosed (Set.range f) → IsCoveringMap f
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Records how a particular argument to a function is delaborated, in non-explicit mode.  -/
Lean.PrettyPrinter.Delaborator.AppImplicitArg : Type
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- Assume that `E` is a normed vector space over semirings `𝕜 ⊆ 𝕜'`
and all points of `s` are points of unique differentiability
with respect to the smaller semiring `𝕜`,
then they are also points of unique differentiability with respect to the larger semiring `𝕜`.
 -/
UniqueDiffOn.mono_field : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {s : Set E} {𝕜' : Type u_3} [inst_4 : Semiring 𝕜'] [inst_5 : SMul 𝕜 𝕜']
  [inst_6 : Module 𝕜' E] [IsScalarTower 𝕜 𝕜' E], UniqueDiffOn 𝕜 s → UniqueDiffOn 𝕜' s
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_insertManyIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [inst_4 : ForIn Id ρ ((a : α) × β a)] {m : Std.DHashMap.Internal.Raw₀ α β} {l : ρ},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑↑(m.insertManyIfNew l)
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- `C` has all limits over any type `J` whose objects and morphisms lie in the same universe
and which has countably many objects and morphisms  -/
CategoryTheory.Limits.HasCountableLimits.out : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Limits.HasCountableLimits C]
  (J : Type) [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J],
  CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.Data.Nat.PSub
Nat.psub_add : ∀ (m n k : ℕ),
  m.psub (n + k) = do
    let __do_lift ← m.psub n
    __do_lift.psub k
-- Lean.Environment
Lean.Kernel.Exception.appTypeMismatch : Lean.Kernel.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Kernel.Exception
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor_toFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.LaxBraidedFunctor C D), F.toLaxMonoidalFunctor.toFunctor = F.toFunctor
-- Init.Control.Basic
/-- Maps a function over a functor, with parameters swapped so that the function comes last.

This function is `Functor.map` with the parameters reversed, typically used via the `<&>` operator.


Conventions for notations in identifiers:

 * The recommended spelling of `<&>` in identifiers is `mapRev`. -/
Functor.mapRev : {f : Type u → Type v} → [Functor f] → {α β : Type u} → f α → (α → β) → f β
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.one_lt_prod_iff : ∀ {ι : Type u_9} {M : Type u_10} [inst : CommMonoid M] [inst_1 : PartialOrder M] [CanonicallyOrderedMul M] {f : ι → M}
  {s : Finset ι}, 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x
-- Mathlib.Algebra.Order.Group.Lattice
inf_sub : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddRightMono α] (a b c : α), a ⊓ b - c = (a - c) ⊓ (b - c)
-- Mathlib.NumberTheory.SmoothNumbers
Nat.ne_zero_of_mem_factoredNumbers : ∀ {s : Finset ℕ} {m : ℕ}, m ∈ Nat.factoredNumbers s → m ≠ 0
-- Mathlib.Computability.Language
Language.instSemiring : {α : Type u_1} → Semiring (Language α)
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.IsNatPowModT.bit1 : ∀ {a b m : ℕ} {c : ℕ},
  Mathlib.Meta.NormNum.IsNatPowModT ((a.pow b).mod m = c) a (2 * b + 1) m ((c.mul ((c.mul a).mod m)).mod m)
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_exp_of_isCoprime : ∀ (i : ℤ) (n : ℕ), n ≠ 0 → IsCoprime i ↑n → IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))) n
-- Mathlib.Order.Lattice
inf_left_le_sup_right : ∀ {α : Type u} [inst : Lattice α] {a b c : α}, a ⊓ b ≤ b ⊔ c
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.center_le_centralizer : ∀ {M : Type u_1} [inst : AddSemigroup M] (S : Set M), AddSubsemigroup.center M ≤ AddSubsemigroup.centralizer S
-- Init.SizeOf
Decidable.isTrue.congr_simp : ∀ {p : Prop} (h : p), isTrue h = isTrue h
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Constructor for objects in `w.StructuredArrowRightwards g`.  -/
CategoryTheory.TwoSquare.StructuredArrowRightwards.mk : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₂ : C₂} →
                            {X₃ : C₃} →
                              (g : R.obj X₂ ⟶ B.obj X₃) →
                                (X₁ : C₁) →
                                  (a : X₂ ⟶ T.obj X₁) →
                                    (b : L.obj X₁ ⟶ X₃) →
                                      CategoryTheory.CategoryStruct.comp (R.map a)
                                            (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) =
                                          g →
                                        w.StructuredArrowRightwards g
-- Mathlib.Algebra.Category.CommAlgCat.Basic
_private.Mathlib.Algebra.Category.CommAlgCat.Basic.0.CommAlgCat.mk.inj : ∀ {R : Type u} {inst : CommRing R} {carrier : Type v} {commRing : CommRing carrier} {algebra : Algebra R carrier}
  {carrier_1 : Type v} {commRing_1 : CommRing carrier_1} {algebra_1 : Algebra R carrier_1},
  { carrier := carrier, commRing := commRing, algebra := algebra } =
      { carrier := carrier_1, commRing := commRing_1, algebra := algebra_1 } →
    carrier = carrier_1 ∧ commRing ≍ commRing_1 ∧ algebra ≍ algebra_1
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {metaSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf}
  {ictx : Lean.Parser.InputContext} {stx : Lean.Syntax} {result? : Option Lean.Language.Lean.HeaderParsedState}
  {toSnapshot_1 : Lean.Language.Snapshot} {metaSnap_1 : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf}
  {ictx_1 : Lean.Parser.InputContext} {stx_1 : Lean.Syntax} {result?_1 : Option Lean.Language.Lean.HeaderParsedState},
  { toSnapshot := toSnapshot, metaSnap := metaSnap, ictx := ictx, stx := stx, result? := result? } =
      { toSnapshot := toSnapshot_1, metaSnap := metaSnap_1, ictx := ictx_1, stx := stx_1, result? := result?_1 } →
    toSnapshot = toSnapshot_1 ∧ metaSnap = metaSnap_1 ∧ ictx = ictx_1 ∧ stx = stx_1 ∧ result? = result?_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_min?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.insert k).min?.isSome = true
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.w_compact_support : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ}, 0 < D → HasCompactSupport (ExistsContDiffBumpBase.w D)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.mk.sizeOf_spec : ∀ {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} [inst_9 : SizeOf ι] [inst_10 : SizeOf R] [inst_11 : SizeOf M]
  [inst_12 : SizeOf N] [inst_13 : SizeOf ι₂] [inst_14 : SizeOf M₂] [inst_15 : SizeOf N₂] (toHom : P.Hom Q)
  (bijective_weightMap : Function.Bijective ⇑toHom.weightMap)
  (bijective_coweightMap : Function.Bijective ⇑toHom.coweightMap),
  sizeOf
      { toHom := toHom, bijective_weightMap := bijective_weightMap, bijective_coweightMap := bijective_coweightMap } =
    1 + sizeOf toHom + sizeOf bijective_weightMap + sizeOf bijective_coweightMap
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  UpperHalfPlane.IsZeroAtImInfty f →
    0 < h →
      Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
        MDiff f →
          UpperHalfPlane.IsBoundedAtImInfty f →
            f =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-2 * Real.pi * τ.im / h)
-- Lean.Meta.Tactic.LibrarySearch
/-- We drop `.star` and `Eq * * *` from the discriminator trees because
they match too much.
 -/
Lean.Meta.LibrarySearch.droppedKeys : List (List Lean.Meta.LazyDiscrTree.Key)
-- Mathlib.RepresentationTheory.Maschke
LinearMap.conjugate_apply : ∀ {k : Type u_1} [inst : CommRing k] {G : Type u_2} [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) (g : G) (v : W),
  (π.conjugate g) v = MonoidAlgebra.single g⁻¹ 1 • π (MonoidAlgebra.single g 1 • v)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instUpwardEnumerable : {α : Type u} →
  [inst : LE α] →
    [inst_1 : LT α] →
      {β : Type v} →
        [inst_2 : LE β] →
          [inst_3 : LT β] →
            [inst_4 : Std.PRange.UpwardEnumerable β] →
              [inst_5 : Std.PRange.LawfulUpwardEnumerable β] →
                [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] →
                  [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] → [m : HasModel✝ α β] → Std.PRange.UpwardEnumerable α
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- The morphism `(X' ⟶[V] Y) ⟶ (X ⟶[V] Y)` induced by a morphism `X ⟶ X'`.  -/
CategoryTheory.eHomWhiskerRight : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] →
            {X X' : C} → (X ⟶ X') → (Y : C) → (X' ⟶[V] Y) ⟶ X ⟶[V] Y
-- Mathlib.Logic.Encodable.Basic
Encodable.surjective_decode_iget : ∀ (α : Type u_3) [inst : Encodable α] [inst_1 : Inhabited α],
  Function.Surjective fun n => (Encodable.decode n).getD default
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_eq_one`. -/
Ideal.ramificationIdx'_eq_one : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [inst_3 : q.IsPrime] [Algebra.EssFiniteType R S] [Algebra.IsUnramifiedAt R q], q.ramificationIdx R = 1
-- Init.Data.Array.Lemmas
Array.getElem?_eq_some_iff : ∀ {α : Type u_1} {i : ℕ} {b : α} {xs : Array α}, xs[i]? = some b ↔ ∃ (h : i < xs.size), xs[i] = b
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.powLogEquiv_apply : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m)
  (m : Multiplicative ℕ), (Submonoid.powLogEquiv h) m = Submonoid.pow n (Multiplicative.toAdd m)
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR_eq_sModNat.helper : ∀ (b q k : ℕ), LucasLehmer.norm_num_ext.sModNatTR.go✝ q k b = LucasLehmer.norm_num_ext.sModNatAux b q k
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker.inj : ∀ {e : Mathlib.Tactic.BicategoryLike.Mor₂} {η : Mathlib.Tactic.BicategoryLike.WhiskerRight}
  {f : Mathlib.Tactic.BicategoryLike.Atom₁} {e_1 : Mathlib.Tactic.BicategoryLike.Mor₂}
  {η_1 : Mathlib.Tactic.BicategoryLike.WhiskerRight} {f_1 : Mathlib.Tactic.BicategoryLike.Atom₁},
  Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker e η f =
      Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker e_1 η_1 f_1 →
    e = e_1 ∧ η = η_1 ∧ f = f_1
-- Mathlib.GroupTheory.Sylow
/-- If `H` is a `p`-subgroup of `G`, then the index of `H` inside its normalizer is congruent
mod `p` to the index of `H`.  -/
Sylow.card_quotient_normalizer_modEq_card_quotient : ∀ {G : Type u} [inst : Group G] [Finite G] {p n : ℕ} [hp : Fact (Nat.Prime p)] {H : Subgroup G},
  Nat.card ↥H = p ^ n →
    Nat.card (↥(Subgroup.normalizer ↑H) ⧸ Subgroup.comap (Subgroup.normalizer ↑H).subtype H) ≡ Nat.card (G ⧸ H) [MOD p]
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.unitRecOn`.  -/
Tree.unitRecOn : {motive : Tree Unit → Sort u_1} →
  (t : Tree Unit) →
    motive BinaryTree.nil → ((x y : Tree Unit) → motive x → motive y → motive (BinaryTree.node () x y)) → motive t
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeightsUnnorm_ne_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1)))
  (i : Fin (n + 1)), s.excenterWeightsUnnorm signs i ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_unique' : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : AddMonoidAlgebra R M →ₐ[R] A),
  F = (AddMonoidAlgebra.lift R A M) ((↑F).comp (AddMonoidAlgebra.of R M))
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.exists_isTorsionBy : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : (x : M) → Decidable (x = 0)] {p : R} (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) (d : ℕ),
  d ≠ 0 →
    ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ j, Module.IsTorsionBy R M (p ^ Submodule.pOrder hM (s j))
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.gcd_eq_sum : ∀ {R : Type u} [inst : CommRing R] (x y : R) [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})],
  ∃ a b, a * x + b * y = IsBezout.gcd x y
-- Lean.Elab.MutualInductive
/-- An intermediate step for mutual inductive elaboration. See `InductiveElabDescr`.  -/
Lean.Elab.Command.InductiveElabStep1 : Type
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₂_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  (RatFunc.Luroth.Q₂✝ h).natDegree = 0
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.isTorsionFree : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommRing A] [inst_4 : AddCommMonoid N] [inst_5 : Module A N] [inst_6 : Algebra R A]
  [inst_7 : Module R N] [IsScalarTower R A N] (f : M →ₗ[R] N) [IsDomain R] [Module.IsTorsionFree R M] (S : Submonoid R)
  [IsLocalization S A] [IsLocalizedModule S f], Module.IsTorsionFree A N
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.continue.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (a : Std.Http.Protocol.H1.Reader.State dir), sizeOf a.continue = 1 + sizeOf a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.compare_minKeyD_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β} {fallback : α},
  cmp ((Std.DTreeMap.Const.modify t k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd f g))
      (CategoryTheory.Limits.pullback.fst f g) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv f)
-- Mathlib.Algebra.Order.GroupWithZero.Lex
LinearOrderedCommGroupWithZero.inl_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β]
  (a : α),
  (LinearOrderedCommGroupWithZero.inl α β) a =
    (WithZero.map' ↑(toLexMulEquiv (αˣ × βˣ))) ((MonoidWithZeroHom.inl α β) a)
-- Std.Data.HashMap.Raw
/-- The number of mappings present in the hash map  -/
Std.HashMap.Raw.size : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → ℕ
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
/-- The particular case of `hasCardinalLT_sigma` when all the inputs are in the
same universe `w`. It is used to prove the general case.  -/
hasCardinalLT_sigma' : ∀ {ι : Type w} (α : ι → Type w) (κ : Cardinal.{w}) [Fact κ.IsRegular],
  HasCardinalLT ι κ → (∀ (i : ι), HasCardinalLT (α i) κ) → HasCardinalLT ((i : ι) × α i) κ
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Init.Data.Array.Extract
Array.popWhile_filter : ∀ {α : Type u_1} {p q : α → Bool} {as : Array α},
  Array.popWhile q (Array.filter p as) = Array.filter p (Array.popWhile (fun a => !p a || q a) as)
-- Mathlib.Algebra.Group.Conj
/-- The bijection between an `AddCommGroup` and its `AddConjClasses`.  -/
AddConjClasses.mkEquiv : {α : Type u} → [inst : AddCommMonoid α] → α ≃ AddConjClasses α
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.num : ℤ → Int.Internal.Linear.Poly
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq_spec_3 : ∀ (x x_1 : Lean.Grind.AC.Seq),
  (∀ (a b : Lean.Grind.AC.Var), x = Lean.Grind.AC.Seq.var a → x_1 = Lean.Grind.AC.Seq.var b → False) →
    (∀ (a : Lean.Grind.AC.Var) (a_1 : Lean.Grind.AC.Seq) (b : Lean.Grind.AC.Var) (b_1 : Lean.Grind.AC.Seq),
        x = Lean.Grind.AC.Seq.cons a a_1 → x_1 = Lean.Grind.AC.Seq.cons b b_1 → False) →
      (x == x_1) = false
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit.congr_simp : ∀ {M : Type u_1} [inst : Monoid M] {a a_1 : M} (e_a : a = a_1) (h : IsUnit a), h.unit = ⋯.unit
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusEquiv_symm_apply : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [inst_1 : CharP R p] [inst_2 : PerfectRing R p],
  ⇑(WittVector.frobeniusEquiv p R).symm = ⇑(WittVector.map ↑(frobeniusEquiv R p).symm)
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvalues.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (i : n), hA.eigenvalues i = hA.eigenvalues₀ ((Fintype.equivOfCardEq ⋯).symm i)
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.instMonoidHomClassMulHom : ∀ {M : Type u_10} {N : Type u_11} [inst : Monoid M] [inst_1 : LeftCancelMonoid N], MonoidHomClass (M →ₙ* N) M N
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear_apply_add_three : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) (n : ℕ),
  f.fpowerSeriesBilinear x (n + 3) = 0
-- Lean.Widget.InteractiveCode
Lean.Widget.instRpcEncodableSubexprInfo : Lean.Server.RpcEncodable Lean.Widget.SubexprInfo
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Linear_CC'₁.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.Linear_CC'₁ C hsC ho =
    LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.CC'₁ C hsC ho, continuous_toFun := ⋯ }
-- Aesop.Search.SearchM
Aesop.SearchM.State.iteration : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM.State Q → Aesop.Iteration
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.withZeroUnits_symm_apply : ∀ {α : Type u_6} [inst : LinearOrderedCommGroupWithZero α] [inst_1 : DecidablePred fun a => a = 0] (a : α),
  OrderMonoidIso.withZeroUnits.symm a = if h : a = 0 then 0 else ↑(Units.mk0 a h)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaObjObjEquiv_symm_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y Y' : C}
  (g : Y' ⟶ Y) (f : Y ⟶ X),
  CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g f) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.obj X).map g.op))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm f)
-- Init.Data.BitVec.Lemmas
BitVec.and_twoPow : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x &&& BitVec.twoPow w i = if x.getLsbD i = true then BitVec.twoPow w i else 0#w
-- Mathlib.Order.Hom.CompleteLattice
FrameHomClass.tosSupHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [FrameHomClass F α β], sSupHomClass F α β