mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitFlipIsoCompLim_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K),
  (CategoryTheory.Limits.limitFlipIsoCompLim F).inv.app X =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).inv
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F.flip X).inv
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The cone itself  -/
CategoryTheory.Limits.LimitCone.cone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.LimitCone F → CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.instIsMultiplicativeQuasiIso : ∀ (A : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} A] [inst_1 : CategoryTheory.Abelian A],
  (HomotopyCategory.Plus.quasiIso A).IsMultiplicative
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Equiv.fg_iff : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N]
  (f : L.Equiv M N), FirstOrder.Language.Structure.FG L M ↔ FirstOrder.Language.Structure.FG L N
-- Mathlib.RingTheory.Smooth.Basic
/-- An `R` algebra `A` is smooth if it is formally smooth and of finite presentation.  -/
Algebra.Smooth : (R : Type u_4) → [inst : CommRing R] → (A : Type u) → [inst_1 : CommRing A] → [Algebra R A] → Prop
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Evaluation of an exact pairing.  -/
CategoryTheory.ExactPairing.evaluation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [CategoryTheory.ExactPairing X Y] →
          CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Std.Data.DTreeMap.Basic
/-- Internal implementation detail of the tree map.  -/
Std.DTreeMap.inner : {α : Type u} →
  {β : α → Type v} →
    {cmp : autoParam (α → α → Ordering) Std.DTreeMap._auto_1} → Std.DTreeMap α β cmp → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The context for evaluating expressions.  -/
Mathlib.Tactic.Bicategory.Context : Type
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_subset_Iio_union_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iic b ⊆ Set.Iio a ∪ Set.Icc a b
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj_hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsFibrant Y] {f g : HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj X ⟶ Y},
  HomotopicalAlgebra.RightHomotopyRel
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj X) f)
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj X) g) →
    HomotopicalAlgebra.FibrantObject.toHoCat.map (HomotopicalAlgebra.FibrantObject.homMk f) =
      HomotopicalAlgebra.FibrantObject.toHoCat.map (HomotopicalAlgebra.FibrantObject.homMk g)
-- Init.GrindInstances.ToInt
Lean.Grind.instLTUInt8UintOfNatNat : Lean.Grind.ToInt.LT UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_lt_rpow_of_exponent_lt : ∀ {x : NNReal} {y z : ℝ}, 1 < x → y < z → x ^ y < x ^ z
-- Mathlib.Analysis.Convex.Function
convexOn_iff_forall_pos : ∀ {𝕜 : 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 : Module 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E}
  {f : E → β},
  ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_eq_iff : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (x y : DirectSum ι fun i => M i),
  (DirectSum.lmap f) x = (DirectSum.lmap f) y ↔ ∀ (i : ι), (f i) (x i) = (f i) (y i)
-- Mathlib.Data.Sigma.Basic
Prod.toSigma_inj : ∀ {α : Type u_7} {β : Type u_8} {x y : α × β}, x.toSigma = y.toSigma ↔ x = y
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_insertEntryIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = true → Std.Internal.List.minKey (Std.Internal.List.insertEntryIfNew k v l) ⋯ = k
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.fvar.sizeOf_spec : ∀ (a : Lean.FVarId) (a_1 : ℕ), sizeOf (Lean.Meta.LazyDiscrTree.Key.fvar a a_1) = 1 + sizeOf a + sizeOf a_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqDeclValue : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.DeclValue pu)
-- Batteries.Data.List.Lemmas
List.idxOfNth_eq_length_of_ge_count : ∀ {α : Type u_1} {x : α} {n : ℕ} {xs : List α} [inst : BEq α], List.count x xs ≤ n → List.idxOfNth x xs n = xs.length
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, t.isEmpty = true → Std.DTreeMap.Raw.Const.get! t a = default
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.toMessageData : Lean.Meta.Match.Problem → Lean.MetaM Lean.MessageData
-- Mathlib.Logic.Equiv.Basic
/-- A family of equivalences `∀ a, γ₁ a ≃ γ₂ a` generates an equivalence between the product
over the fibers of a function `f : α → β` on index types.  -/
Equiv.piCongrSigmaFiber : {α : Type u_9} →
  {β : Type u_10} →
    {f : α → β} →
      {γ₁ : α → Sort u_11} →
        {γ₂ : α → Sort u_12} →
          ((a : α) → γ₁ a ≃ γ₂ a) → ((σ : (y : β) × { x // f x = y }) → γ₁ ↑σ.snd) ≃ ((a : α) → γ₂ a)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.subcomplex_toN : ∀ {X : SSet} (x : X.S), x.toN.subcomplex = x.subcomplex
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
MonomialOrder.degLex_lt_iff : ∀ {σ : Type u_2} [inst : LinearOrder σ] [inst_1 : WellFoundedGT σ] {a b : σ →₀ ℕ},
  MonomialOrder.degLex.toSyn a < MonomialOrder.degLex.toSyn b ↔ toDegLex a < toDegLex b
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `⨅ i, f i = 0` when the domain of the real-valued function `f` is empty or unbounded below,
it suffices to show that all values of `f` are nonpositive to show that `0 ≤ ⨅ i, f i`.  -/
Real.iInf_nonpos : ∀ {ι : Sort u_1} {f : ι → ℝ}, (∀ (i : ι), f i ≤ 0) → ⨅ i, f i ≤ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.WeakRankFunction.isRegular : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] [WellFoundedLT α] [h.IsProper]
  (f : h.WeakRankFunction α), h.IsRegular
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.le_of_le_cert p₁ p₂ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0
-- Mathlib.Algebra.Group.Subgroup.Basic
AddGroup.addConjugatesOfSet.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddGroup.addConjugatesOfSet s = ⋃ a ∈ s, addConjugatesOf a
-- Batteries.Data.Fin.Lemmas
Fin.exists_isSome_of_isSome_findSomeRev? : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSomeRev? f).isSome = true → ∃ i, (f i).isSome = true
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Wide pushout diagrams of equivalent index types are equivalent.  -/
CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv : {J : Type w} →
  (J' : Type w') → J ≃ J' → (CategoryTheory.Limits.WidePushoutShape J ≌ CategoryTheory.Limits.WidePushoutShape J')
-- Batteries.Data.PairingHeap
/-- The well formedness predicate for a heap node.
It asserts that:
* If `a` is added at the top to make the forest into a tree, the resulting tree
  is a `le`-min-heap (if `le` is well-behaved)
 -/
Batteries.PairingHeapImp.Heap.NodeWF : {α : Type u_1} → (α → α → Bool) → α → Batteries.PairingHeapImp.Heap α → Prop
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which antivary together on `s`, is unchanged by a permutation if and only if `f` and `g ∘ σ`
antivary together on `s`. Stated by permuting the entries of `g`.  -/
AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ AntivaryOn f (g ∘ ⇑σ) ↑s)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} {l : List α} {k : α} {fallback : Unit},
  (m.insertManyIfNewUnit l).getD k fallback = ()
-- Mathlib.Probability.Process.Filtration
MeasureTheory.filtrationOfSet.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {s : ι → Set Ω}
  (hsm : ∀ (i : ι), MeasurableSet (s i)),
  MeasureTheory.filtrationOfSet hsm =
    { seq := fun i => MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}, mono' := ⋯, le' := ⋯ }
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
natDegree_minpolyDiv : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.restr_toFun : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : Equidecomp X G) (A : Set X) (a : X),
  ↑(f.restr A).toPartialEquiv a = ↑f.toPartialEquiv a
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.inverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) [P.RespectsIso] (F : CategoryTheory.Functor C D),
  (P.inverseImage F).RespectsIso
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'' : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g +ᵥ x) ∂μ
-- Mathlib.Analysis.Calculus.Darboux
/-- If the derivative of a function is never equal to `m`, then either
it is always greater than `m`, or it is always less than `m`.  -/
hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne : ∀ {f f' : ℝ → ℝ} {s : Set ℝ},
  Convex ℝ s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → ∀ {m : ℝ}, (∀ x ∈ s, f' x ≠ m) → (∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.modifyStateImpl : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → (σ → σ) → Lean.Meta.Grind.GoalM Unit
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_sub : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (f g : MvPowerSeries σ R), MvPowerSeries.subst a (f - g) = MvPowerSeries.subst a f - MvPowerSeries.subst a g
-- Mathlib.CategoryTheory.Comma.Basic
/-- Morphism on right objects  -/
CategoryTheory.CommaMorphism.right : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {X Y : CategoryTheory.Comma L R} → CategoryTheory.CommaMorphism X Y → (X.right ⟶ Y.right)
-- Mathlib.Algebra.Group.PNatPowAssoc
/-- Multiplication is power-associative.  -/
PNatPowAssoc.ppow_add : ∀ {M : Type u_2} {inst : Mul M} {inst_1 : Pow M ℕ+} [self : PNatPowAssoc M] (k n : ℕ+) (x : M),
  x ^ (k + n) = x ^ k * x ^ n
-- Mathlib.Algebra.GroupWithZero.Basic
/-- An element of a left-cancellative `MulZeroOneClass` fixed by right multiplication by
an element other than one must be zero.  -/
eq_zero_of_mul_eq_self_right : ∀ {M₀ : Type u_1} {a b : M₀} [inst : MulZeroOneClass M₀] [IsLeftCancelMulZero M₀], b ≠ 1 → a * b = a → a = 0
-- Mathlib.Topology.MetricSpace.Algebra
Real.hasLipschitzAdd : LipschitzAdd ℝ
-- Mathlib.Algebra.Lie.Subalgebra
/-- An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its
image.  -/
LieEquiv.lieSubalgebraMap : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieRing L₂] →
            [inst_3 : LieAlgebra R L₁] →
              [inst_4 : LieAlgebra R L₂] →
                (L₁'' : LieSubalgebra R L₁) → (e : L₁ ≃ₗ⁅R⁆ L₂) → ↥L₁'' ≃ₗ⁅R⁆ ↥(LieSubalgebra.map e.toLieHom L₁'')
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.single.congr_simp : ∀ {ι : Type u_1} (I J J_1 : BoxIntegral.Box ι) (e_J : J = J_1) (h : J ≤ I),
  BoxIntegral.Prepartition.single I J h = BoxIntegral.Prepartition.single I J_1 ⋯
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.lawfulOrderOrd : ∀ {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α),
  let this := self.ord;
  let this_1 := ⋯;
  let this_2 := self.le;
  Std.LawfulOrderOrd α
-- Mathlib.GroupTheory.Congruence.Basic
Con.mem_coe : ∀ {M : Type u_1} [inst : MulOneClass M] {c : Con M} {x y : M}, (x, y) ∈ ↑c ↔ (x, y) ∈ c
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Modify an element in the set with the given function,
doing nothing if the key is not found.
Note that the element returned by `f` must be equivalent to `x`.

```
updateWith f 0 {1, 2, 3} = {1, 2, 3}
updateWith f 1 {1, 2, 3} = {2, 3}     if f 1 = none
                         = {a, 2, 3}  if f 1 = some a
```  -/
Ordnode.updateWith : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → (α → Option α) → α → Ordnode α → Ordnode α
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddAbove.neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G},
  BddAbove s → BddBelow (-s)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.fap.injEq : ∀ (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg) (c_1 : Lean.IR.FunId) (ys_1 : Array Lean.IR.Arg),
  (Lean.IR.Expr.fap c ys = Lean.IR.Expr.fap c_1 ys_1) = (c = c_1 ∧ ys = ys_1)
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} {f : β → β} {t : Std.TreeMap.Raw α β cmp},
  t.WF → (t.modify a f).WF
-- Mathlib.Order.Category.BddDistLat
BddDistLat.hom_inv_apply : ∀ {X Y : BddDistLat} (e : X ≅ Y) (s : ↑Y.toDistLat),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- Given an orthogonal basis with respect to a bilinear map, the bilinear map is left-separating if
the basis has no elements which are self-orthogonal.  -/
LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self : ∀ {n : Type u_19} {R : Type u_20} {M : Type u_21} {M₁ : Type u_22} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [IsDomain R] [Module.IsTorsionFree R M₁]
  {B : M →ₗ[R] M →ₗ[R] M₁} (v : Module.Basis n R M), B.IsOrthoᵢ ⇑v → (∀ (i : n), (B (v i)) (v i) ≠ 0) → B.SeparatingLeft
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.ofNatTrans.sizeOf_spec : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D} (toNatTrans : F.toFunctor ⟶ G.toFunctor),
  sizeOf { toNatTrans := toNatTrans } = 1 + sizeOf toNatTrans
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.coe_range : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [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₂), ↑f.range = Set.range ⇑f
-- Lean.Parser.Command
Lean.Parser.Command.deprecated_module.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.IsMonoidal.toContainsUnit : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsMonoidal], P.ContainsUnit
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_disjoint_of_disjoint_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {X K : Set α}, Disjoint X K → K ⊆ M.coloops → Disjoint (M.closure X) K
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_id : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B],
  Algebra.TensorProduct.map (AlgHom.id S A) (AlgHom.id R B) = AlgHom.id S (TensorProduct R A B)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.insert.eq_1 : ∀ {α : Type u_1} (path : RBTree.RBNode.Path α) (v : α), path.insert RBTree.RBNode.nil v = path.insertNew v
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_smul_iff : ∀ {α : Type u_1} {n : Type u_3} {R : Type u_5} [inst : Monoid R] [inst_1 : MulAction R α] {A : Matrix n n α} (k : R)
  [Invertible k], (k • A).IsSymm ↔ A.IsSymm
-- Mathlib.Algebra.Group.Nat.Units
Nat.units_eq_one : ∀ (u : ℕˣ), u = 1
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.idealOfLE.eq_1 : ∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S),
  R.idealOfLE S h = Ideal.comap (R.inclusion S h) (IsLocalRing.maximalIdeal ↥S)
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.mem_submonoid_iff : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : MulOneClass β] {f : α → β},
  f ∈ HasCompactMulSupport.submonoid α β ↔ HasCompactMulSupport f
-- Std.Sync.StreamMap
Std.AnyAsyncStream.mk.inj : ∀ {α t : Type} {inst : Std.Async.IO.AsyncStream t α} {a : t} {t_1 : Type} {inst_1 : Std.Async.IO.AsyncStream t_1 α}
  {a_1 : t_1}, Std.AnyAsyncStream.mk a = Std.AnyAsyncStream.mk a_1 → t = t_1 ∧ inst ≍ inst_1 ∧ a ≍ a_1
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.eq_of_le_of_ne_self : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) [Ring.KrullDimLE 1 ↥A] {B : ValuationSubring K},
  A ≤ B → A ≠ B → B = ⊤
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
fourier_gaussian_pi : ∀ {b : ℂ},
  0 < b.re →
    (FourierTransform.fourier fun x => Complex.exp (-↑Real.pi * b * ↑x ^ 2)) = fun t =>
      1 / b ^ (1 / 2) * Complex.exp (-↑Real.pi / b * ↑t ^ 2)
-- Mathlib.Data.Part
Part.instSDiff : {α : Type u_1} → [SDiff α] → SDiff (Part α)
-- Mathlib.RingTheory.Congruence.Basic
/-- The supremum of two congruence relations equals the smallest congruence relation containing
the supremum of the underlying binary operations.  -/
RingCon.sup_def : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (c d : RingCon R), c ⊔ d = ringConGen (⇑c ⊔ ⇑d)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.darts_takeUntil_subset_darts : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).darts ⊆ p.darts
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.other.sizeOf_spec : sizeOf Lean.Meta.DiscrTree.Key.other = 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (assign : α → Bool) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ)
  (hidx1 : idx < w),
  curr ≤ idx →
    ⟦assign,
        { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).aig,
          ref :=
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).vec.get idx
              hidx1 }⟧ =
      if hidx : distance + idx < w then ⟦assign, { aig := aig, ref := input.get (distance + idx) hidx }⟧ else false
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_Ψ₃ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B),
  (W.baseChange B).Ψ₃ = Polynomial.map (↑f) (W.baseChange A).Ψ₃
-- Aesop.Forward.State
/-- Add a match to the cluster state.  -/
Aesop.ClusterState.addMatch : Aesop.ClusterState → Aesop.Match → Aesop.ClusterState.AddM Aesop.ClusterState
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.exists_pow_mem_range_tensorProduct : ∀ {k : Type u_1} {K : Type u_2} {R : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  [inst_3 : CommRing R] [inst_4 : Algebra k R] [IsPurelyInseparable k K] (x : TensorProduct k R K),
  ∃ n > 0, x ^ n ∈ (algebraMap R (TensorProduct k R K)).range
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The subgroup of Dirichlet characters of level `n` whose conductor is coprime to `d`.  -/
DirichletCharacter.subgroupOfCoprimeConductor : {R : Type u_1} → [inst : CommMonoidWithZero R] → {n : ℕ} → [NeZero n] → ℕ → Subgroup (DirichletCharacter R n)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If the image of the `(fixedBy α g)ᶜ` set by the pointwise action of `h: G`
is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute.
 -/
MulAction.not_commute_of_disjoint_movedBy_preimage : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [FaithfulSMul G α] {g h : G},
  g ≠ 1 → Disjoint (MulAction.fixedBy α g)ᶜ (h • (MulAction.fixedBy α g)ᶜ) → ¬Commute g h
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.image : ∀ {G : Type u_1} [inst : Group G] {A : Set G} {K : ℝ} {F : Type u_2} {H : Type u_3} [inst_1 : Group H]
  [inst_2 : FunLike F G H] [MonoidHomClass F G H] (f : F), IsApproximateSubgroup K A → IsApproximateSubgroup K (⇑f '' A)
-- Init.Guard
/-- The `guard_expr` matching specifier, one of `=`, `=~`, `=ₛ`, `=ₐ`  -/
Lean.Parser.equal : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.val_image_orbit : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] {p : SubAddAction R M} (m : ↥p),
  Subtype.val '' AddAction.orbit R m = AddAction.orbit R ↑m
-- Mathlib.Order.Category.Semilat
/-- The underlying type of a sup-semilattice with a bottom element.  -/
SemilatSupCat.X : SemilatSupCat → Type u