mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_right_idem : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s ∪ t ∪ t = s ∪ t
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S),
  (F.toDescentDataAsCoalgebra fun x => f).IsEquivalence ↔
    (CategoryTheory.Comonad.comparison (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj)).IsEquivalence
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Any cocone morphism between colimit cocones is an isomorphism.  -/
CategoryTheory.Limits.IsColimit.hom_isIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (Q : CategoryTheory.Limits.IsColimit t)
  (P : CategoryTheory.Limits.IsColimit s) (f : t ⟶ s), CategoryTheory.IsIso f
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Constructs the array of keys of the map.  -/
RBTree.RBMap.Keys.toArray : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → Array α
-- Init.Data.SInt.Lemmas
Int32.toInt64_toISize : ∀ (n : Int32), n.toISize.toInt64 = n.toInt64
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is of the form
```
@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) _ _
```
 -/
Lean.Meta.Grind.Arith.isNatAdd : Lean.Expr → Bool
-- Aesop.Tree.UnsafeQueue
Aesop.PostponedSafeRule.rule : Aesop.PostponedSafeRule → Aesop.SafeRule
-- Mathlib.Tactic.Ring.Common
/-- Equality test for expressions. This is not a `BEq` instance because it is heterogeneous.  -/
Mathlib.Tactic.Ring.Common.ExSum.eq : Mathlib.Tactic.Ring.Common.RingCompare Mathlib.Tactic.Ring.Common.btℕ →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {bt : Q(«$α») → Type} →
        {sα : Q(CommSemiring «$α»)} →
          Mathlib.Tactic.Ring.Common.RingCompare bt →
            {a b : Q(«$α»)} → Mathlib.Tactic.Ring.Common.ExSum bt sα a → Mathlib.Tactic.Ring.Common.ExSum bt sα b → Bool
-- Mathlib.Analysis.RCLike.Basic
RCLike.inv_eq_conj : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, ‖z‖ = 1 → z⁻¹ = (starRingEnd K) z
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- the Leibniz pullback  -/
CategoryTheory.Functor.PullbackObjObj.π : {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₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₃ Y₃ : C₃} →
                    {f₃ : X₃ ⟶ Y₃} → (self : G.PullbackObjObj f₁ f₃) → (G.obj (Opposite.op Y₁)).obj X₃ ⟶ self.pt
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_cancel_of_dvd : ∀ {a b : ℤ}, b ∣ a → b * a.tdiv b = a
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mul.match_1.eq_1 : ∀ {v : Lean.Level} {M : Q(Type v)}
  (motive : Mathlib.Tactic.FieldSimp.qNF q(«$M») → Mathlib.Tactic.FieldSimp.qNF q(«$M») → Sort u_1)
  (l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) (h_1 : (l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) → motive l [])
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
            (a₂ : ℤ) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) → (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (match [], l with
    | [], l => h_1 l
    | l, [] => h_2 l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
    h_1 l
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.toGerm_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β],
  Function.Injective MeasureTheory.AEEqFun.toGerm
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.ext_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] {f g : M [⋀^ι]→L[R] N}, f = g ↔ ∀ (x : ι → M), f x = g x
-- Init.Data.UInt.Lemmas
UInt8.div_one : ∀ {a : UInt8}, a / 1 = a
-- Mathlib.Data.Bool.Basic
Bool.not_eq_true_eq_eq_false : ∀ (a : Bool), ((!a) = true) = (a = false)
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.instNeg.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : Zero M] [inst_1 : NegZeroClass N],
  ZeroHom.instNeg = { neg := fun f => { toFun := fun m => -f m, map_zero' := ⋯ } }
-- Mathlib.Data.Finset.Card
List.Nodup.card_eq_countP : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {P : α → Prop} [inst_1 : DecidablePred P],
  l.Nodup → (Finset.filter P l.toFinset).card = List.countP (fun b => decide (P b)) l
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.concat_comp_IccInclusionRight : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E]
  {f : C(↑(Set.Icc a b), E)} {g : C(↑(Set.Icc b c), E)},
  f ⊤ = g ⊥ → (f.concat g).comp ContinuousMap.IccInclusionRight = g
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_union : ∀ {G : Type u_1} [inst : AddGroup G] (s t : Set G),
  AddSubgroup.closure (s ∪ t) = AddSubgroup.closure s ⊔ AddSubgroup.closure t
-- Mathlib.Algebra.GroupWithZero.Subgroup
Subgroup.le_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {G : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Group G] [inst_2 : MulDistribMulAction G₀ G]
  {S T : Subgroup G} {a : G₀}, a ≠ 0 → (S ≤ a • T ↔ a⁻¹ • S ≤ T)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLTOffset : LT Std.Time.Nanosecond.Offset
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instModuleHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        [inst_2 : CategoryTheory.Preadditive C] →
          {R : Type u_1} →
            [inst_3 : Semiring R] →
              [inst_4 : CategoryTheory.Linear R C] →
                [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                  [∀ (n : ℤ), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)] → Module R (T₁ ⟶ T₂)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.IsOpenImmersion.eq_1 : ∀ (x x_1 : AlgebraicGeometry.Scheme) (f : x ⟶ x_1),
  AlgebraicGeometry.IsOpenImmersion f =
    AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (AlgebraicGeometry.Scheme.Hom.toLRSHom f)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.isBigO : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l : Filter α}, Asymptotics.IsBigOWith c l f g → f =O[l] g
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.instEmptyCollection : EmptyCollection Aesop.RuleBuilderOptions
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.Option.pmap_or.match_1.splitter : {α : Type u_1} →
  {p : α → Prop} →
    {o' : Option α} →
      (motive : (o : Option α) → {h : ∀ (a : α), o.or o' = some a → p a} → Sort u_2) →
        (o : Option α) →
          {h : ∀ (a : α), o.or o' = some a → p a} →
            ((h : ∀ (a : α), none.or o' = some a → p a) → motive none) →
              ((a : α) → (h : ∀ (a_1 : α), (some a).or o' = some a_1 → p a_1) → motive (some a)) → motive o
-- Init.Data.Fin.Lemmas
_private.Init.Data.Fin.Lemmas.0.Nat.mod_eq_sub_of_lt_two_mul : ∀ {x n : ℕ}, n ≤ x → x < 2 * n → x % n = x - n
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isPosSemidef_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Preorder R], LinearMap.BilinForm.IsPosSemidef 0
-- Mathlib.Algebra.Ring.Parity
Even.add_one : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a → Odd (a + 1)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides.  -/
InnerProductGeometry.tan_angle_add_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → Real.tan (InnerProductGeometry.angle x (x + y)) = ‖y‖ / ‖x‖
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.map_apply : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {I₀ : WithTop (BoxIntegral.Box ι)} (f : BoxIntegral.BoxAdditiveMap ι M I₀) (g : M →+ N), ⇑(f.map g) = ⇑g ∘ ⇑f
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpoly_inv : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (A : Matrix n n R),
  IsUnit A → A⁻¹.charpoly = (-1) ^ Fintype.card n * Polynomial.C (Ring.inverse A.det) * A.charpolyRev
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.bot : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], Module.Finite R ↥⊥
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.mem_centralizer_iff : ∀ {G : Type u_1} [inst : Group G] {g : G} {s : Set G}, g ∈ Subgroup.centralizer s ↔ ∀ h ∈ s, h * g = g * h
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.autoImplicitCtx.injEq : ∀ (autoImplicits autoImplicits_1 : Array Lean.Expr),
  (Lean.Elab.PartialContextInfo.autoImplicitCtx autoImplicits =
      Lean.Elab.PartialContextInfo.autoImplicitCtx autoImplicits_1) =
    (autoImplicits = autoImplicits_1)
-- Mathlib.Analysis.Normed.Field.Lemmas
NormedDivisionRing.to_continuousInv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α], ContinuousInv₀ α
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.nodup_toList : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x : α), (p.toList x).Nodup
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the image of `perfectClosure F E`
under the map `i` is contained in `perfectClosure F K`.  -/
perfectClosure.map_le_of_algHom : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E →ₐ[F] K), IntermediateField.map i (perfectClosure F E) ≤ perfectClosure F K
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.instLawfulMonadLift : ∀ {m : Type w → Type w'} {n : Type w → Type w''} [inst : MonadLift m n] [inst_1 : Monad m] [inst_2 : Monad n]
  [LawfulMonad m] [LawfulMonad n] [LawfulMonadLift m n],
  LawfulMonadLift (Std.Iterators.PostconditionT m) (Std.Iterators.PostconditionT n)
-- Std.Sat.AIG.Basic
/-- Transform an `Entrypoint` into a graphviz string. Useful for debugging purposes.
 -/
Std.Sat.AIG.toGraphviz : {α : Type} → [inst : DecidableEq α] → [ToString α] → [inst_2 : Hashable α] → Std.Sat.AIG.Entrypoint α → String
-- Mathlib.Combinatorics.Quiver.Path.Weight
/-- If all edge weights (given by a function on vertices) are non-negative,
so is the path weight.  -/
Quiver.Path.weightOfEPs_nonneg : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  {w : V → V → R}, (∀ (i j : V), 0 ≤ w i j) → ∀ {i j : V} (p : Quiver.Path i j), 0 ≤ Quiver.Path.weightOfEPs w p
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
/-- The quadratic polynomial $$\sum_i c_i X_i Y_i$$.  -/
MvPolynomial.sumSMulXSMulY : {n : Type u_1} → {R : Type u_2} → [inst : CommRing R] → (n →₀ R) →ₗ[R] MvPolynomial (n ⊕ n) R
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.dense_domain : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y), Dense ↑f.domain
-- Init.Data.Array.Basic
Array.instGetElemUSizeLtNatToNatSize : {α : Type u} → GetElem (Array α) USize α fun xs i => i.toNat < xs.size
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.neg_add_cancel : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → -a + b + a = b
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.quasiIso_πTruncGE_iff_isSupported : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], QuasiIso (K.πTruncGE e) ↔ K.IsSupported e
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- A continuous representation of a group `G` on a `R`-module `V` which is a topological addgroup
is a homomorphism `G →* V →L[R] V`.  -/
ContRepresentation : (R : Type u_1) →
  (G : Type u_2) →
    (V : Type u_3) →
      [Monoid G] →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : TopologicalSpace V] → [IsTopologicalAddGroup V] → [Module R V] → Type (max u_2 u_3)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.comp_apply : ∀ {X : TopCat} {U V W : TopologicalSpace.Opens ↑X} (f : U ⟶ V) (g : V ⟶ W) (x : ↥U),
  (CategoryTheory.CategoryStruct.comp f g) x = g (f x)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instNeg : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N' : Type u_6} → [inst_3 : AddCommGroup N'] → [inst_4 : Module R N'] → {ι : Type u_7} → Neg (M [⋀^ι]→ₗ[R] N')
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph.0.SimpleGraph.Walk.toSubgraph.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2) (v v_1 : V) (h : G.Adj u v_1)
  (p : G.Walk v_1 v) (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_2 : V) → (h : G.Adj u v_2) → (p : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons h p)),
  (match v, SimpleGraph.Walk.cons h p with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h p => h_2 v v_2 h p) =
    h_2 v v_1 h p
-- Mathlib.Data.Fintype.List
fintypeNodupList : {α : Type u_1} → [Fintype α] → Fintype { l // l.Nodup }
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.prod_smul : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (g : Monoid.PushoutI φ) (w : Monoid.PushoutI.NormalWord d),
  (g • w).prod = g * w.prod
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.State : Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.filter_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool},
  m.WF → ((Std.DHashMap.Raw.filter f m).Equiv m ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = true)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.hasSum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α], HasSumUniformlyOn f g s → x ∈ s → HasSum (fun x_1 => f x_1 x) (g x)
-- Init.Control.Lawful.Instances
Option.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α), Option.map f (some x) = some (f x)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.shape_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  (S : J.Cover X) (I : S.Relation), S.shape.fst I = I.fst
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.bernoulli_add_indicator_eq_sub : ∀ {k p : ℕ},
  k > 0 →
    ∀ [Fact (Nat.Prime p)],
      ∃ T,
        bernoulli (2 * k) + Bernoulli.vonStaudtIndicator✝ (2 * k) p / ↑p =
          ↑T - ∑ i ∈ Finset.range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsMaximal.isPrime : ∀ {P : Type u_1} [inst : DistribLattice P] {I : Order.Ideal P} [I.IsMaximal], I.IsPrime
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.id_mapId_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : B),
  ((CategoryTheory.StrictPseudofunctor.id B).mapId a).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
-- Mathlib.Data.Multiset.Fintype
Multiset.coe_consEquiv_of_eq_of_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {v : α} (x : (v ::ₘ m).ToType),
  x.fst = v → ↑x.snd = Multiset.count v m → Multiset.consEquiv x = none
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceMod : Lean.Meta.Simp.DSimproc
-- Init.Data.Int.Bitwise.Basic
Int.instComplement : Complement ℤ
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
SetRel.comp.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ),
  R.comp S = {(a, c) | ∃ b, (a, b) ∈ R ∧ (b, c) ∈ S}
-- Mathlib.Algebra.Free
FreeMagma.toFreeSemigroup_map : ∀ {α : Type u} {β : Type v} (f : α → β) (x : FreeMagma α),
  FreeMagma.toFreeSemigroup ((FreeMagma.map f) x) = (FreeSemigroup.map f) (FreeMagma.toFreeSemigroup x)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.sup_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → SemilatticeSup (α i)]
  (f g : Π₀ (i : ι), α i) (i : ι), (f ⊔ g) i = f i ⊔ g i
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_diseq_subst1_cert.eq_1 : ∀ (k : ℤ) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_diseq_subst1_cert k p₁ p₂ p₃ = (p₃ == (p₁.mul k).combine p₂)
-- Std.Time.Date.PlainDate
/-- Creates a `PlainDate` from a year and a day ordinal within that year.
 -/
Std.Time.PlainDate.ofYearOrdinal : (year : Std.Time.Year.Offset) → Std.Time.Day.Ordinal.OfYear year.isLeap → Std.Time.PlainDate
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_measurable_edist : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} [MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ℕ), Measurable fun a => edist (f n a) (g a)) →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
      MeasureTheory.TendstoInMeasure μ f Filter.atTop g
-- Mathlib.Order.CompleteLattice.Defs
lt_sInf_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {l : α}, l < sInf s ↔ ∃ b, l < b ∧ b ∈ lowerBounds s
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadLift_refl : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {x : m α} {Q : Std.Do.PostCond α ps}
  [inst : Std.Do.WP m ps], (Std.Do.wp (monadLift x)).apply Q = (Std.Do.wp x).apply Q
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_lt_tsub_right_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable c → c ≤ a → a < b → a - c < b - c
-- Mathlib.Order.SymmDiff
disjoint_symmDiff_inf : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), Disjoint (symmDiff a b) (a ⊓ b)
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The inclusion functor `FibrantObject C ⥤ C`.  -/
HomotopicalAlgebra.FibrantObject.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] →
      [inst_2 : CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Functor (HomotopicalAlgebra.FibrantObject C) C
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} [inst_2 : SizeOf C] (hom : M.X ⟶ N.X) [isComonHom_hom : CategoryTheory.IsComonHom hom],
  sizeOf { hom := hom, isComonHom_hom := isComonHom_hom } = 1 + sizeOf hom + sizeOf isComonHom_hom
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- The universal property of `MonoidHom.noncommPiCoprod`

Given monoid morphisms `φᵢ : Nᵢ → M` whose images pairwise commute,
there exists a unique monoid morphism `φ : Πᵢ Nᵢ → M` that induces the `φᵢ`,
and it is given by `MonoidHom.noncommPiCoprod`.  -/
MonoidHom.noncommPiCoprodEquiv : {M : Type u_1} →
  [inst : Monoid M] →
    {ι : Type u_2} →
      [Fintype ι] →
        {N : ι → Type u_3} →
          [inst_2 : (i : ι) → Monoid (N i)] →
            [DecidableEq ι] →
              { ϕ // Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y) } ≃ (((i : ι) → N i) →* M)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.mem_stabilizer_finset_iff_subset_vadd_finset : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} [inst_2 : DecidableEq α]
  {s : Finset α}, a ∈ AddAction.stabilizer G s ↔ s ⊆ a +ᵥ s
-- Mathlib.Algebra.Lie.Prod
LieHom.prod_apply : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L]
  [inst_6 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂) (i : L), (f.prod g) i = (f i, g i)
-- Init.Coe
instCoeOTCOfCoeOut : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → [CoeOut α β] → [CoeOTC β γ] → CoeOTC α γ
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.CAlgHom_apply : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A),
  Polynomial.CAlgHom a = Polynomial.C a
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {V W : QuadraticModuleCat R} {x y : V.Hom W}, x.toIsometry' = y.toIsometry' → x = y
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.not_reachable_of_neighborSet_left_eq_empty : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, u ≠ v → G.neighborSet u = ∅ → ¬G.Reachable u v
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
_private.Mathlib.Analysis.Calculus.FormalMultilinearSeries.0.FormalMultilinearSeries.removeZero.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Order.WellFounded
WellFounded.instAsymmRel_mathlib : ∀ {α : Type u_1} [inst : WellFoundedRelation α], Std.Asymm WellFoundedRelation.rel
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.scriptSteps? : Aesop.RuleApplication → Option (Array Aesop.Script.LazyStep)
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_comp_val_Ici_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] {a : α} {f : α → β} {l : Filter β},
  Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coim_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {f g : CategoryTheory.Arrow C} (u : f ⟶ g),
  CategoryTheory.Abelian.coim.map u =
    CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left u) (CategoryTheory.Abelian.coimage.π g.hom)) ⋯