mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.inv_mul_le_iff : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a b : M}, ↑u⁻¹ * a ≤ b ↔ a ≤ ↑u * b
-- Mathlib.Order.Sublocale
/-- The restriction from the locale X into a sublocale is a nucleus.  -/
Sublocale.toNucleus : {X : Type u_1} → [inst : Order.Frame X] → Sublocale X → Nucleus X
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The free product of finitely presented groups is finitely presented  -/
Group.IsFinitelyPresented.instCoprod : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] [Group.IsFinitelyPresented G]
  [Group.IsFinitelyPresented H], Group.IsFinitelyPresented (Monoid.Coprod G H)
-- Init.System.IO
/-- The size of the file in bytes.  -/
IO.FS.Metadata.byteSize : IO.FS.Metadata → UInt64
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.sumSMulInv_single_id : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Fintype G] [inst_3 : DecidableEq G] {X : FDRep k G}
  (v : ↑X.V), ∑ s, Pi.single 1 1 s • (X.ρ s⁻¹) v = v
-- Lean.Parser.Command
Lean.Parser.Command.initializeKeyword.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.SInt.Lemmas
Int32.toInt_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 31 → (Int32.ofNat n).toInt = ↑n
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- Replace the sub-expression at the given position by a fresh meta-variable.  -/
insertMetaVar : Lean.Expr → Lean.SubExpr.Pos → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle_assoc_comp_left_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv)
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv =
    CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g
-- Init.System.IOError
/-- Some other error occurred.  -/
IO.Error.userError : String → IO.Error
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a | 1)` has the value `1`.  -/
jacobiSym.one_right : ∀ (a : ℤ), jacobiSym a 1 = 1
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_sUnion_iff_of_orderTop : ∀ {α : Type v} [inst : LinearOrder α] [OrderTop α] {s : Set (Set α)}, IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_span_natCast : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  (n : ℕ), Ideal.absNorm (Ideal.span {↑n}) = n ^ Module.finrank ℤ S
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_scomp_three : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {s t : Set 𝕜} {x : 𝕜},
  ContDiffWithinAt 𝕜 3 g t (f x) →
    ContDiffWithinAt 𝕜 3 f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              iteratedDerivWithin 3 (g ∘ f) s x =
                derivWithin f s x ^ 3 • iteratedDerivWithin 3 g t (f x) +
                    3 • iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x) +
                  iteratedDerivWithin 3 f s x • derivWithin g t (f x)
-- Mathlib.Order.Category.Lat
Lat.Iso.mk_inv : ∀ {α β : Lat} (e : ↑α ≃o ↑β), (Lat.Iso.mk e).inv = Lat.ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }
-- Mathlib.Order.KrullDimension
Order.krullDim_ne_bot_of_finiteDimensionalOrder : ∀ {α : Type u_1} [inst : Preorder α] [FiniteDimensionalOrder α], Order.krullDim α ≠ ⊥
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Complex.ofRealLI.eq_1 : Complex.ofRealLI = { toLinearMap := Complex.ofRealAm.toLinearMap, norm_map' := Complex.norm_real }
-- Mathlib.Data.Multiset.Count
Multiset.countP.congr_simp : ∀ {α : Type u_1} (p p_1 : α → Prop),
  p = p_1 →
    ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (s s_1 : Multiset α),
      s = s_1 → Multiset.countP p s = Multiset.countP p_1 s_1
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- This is the **Unfolding Trick**: Given an additive subgroup `Γ'` of an additive group `G'`, the
integral of a function `f` on `G'` times the lift to `G'` of a function `g` on the quotient
`G' ⧸ Γ'` with respect to a right-invariant measure `μ` on `G'`, is equal to the integral over
the quotient of the automorphization of `f` times `g`.  -/
QuotientAddGroup.integral_mul_eq_integral_automorphize_mul : ∀ {G' : Type u_1} [inst : AddGroup G'] [inst_1 : MeasurableSpace G'] [inst_2 : TopologicalSpace G']
  [IsTopologicalAddGroup G'] [BorelSpace G'] {μ' : MeasureTheory.Measure G'} {Γ' : AddSubgroup G'} {𝓕' : Set G'},
  MeasureTheory.IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ' →
    ∀ [Countable ↥Γ'] [inst_6 : MeasurableSpace (G' ⧸ Γ')] [BorelSpace (G' ⧸ Γ')] {K : Type u_2}
      [inst_8 : NormedField K] [inst_9 : NormedSpace ℝ K] [μ'.IsAddRightInvariant] {f : G' → K},
      MeasureTheory.Integrable f μ' →
        ∀ {g : G' ⧸ Γ' → K},
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) →
            essSup (fun x => ‖g x‖ₑ) (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) ≠ ⊤ →
              MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f)
                  (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) →
                ∫ (x : G'), g ↑x * f x ∂μ' =
                  ∫ (x : G' ⧸ Γ'),
                    g x *
                      QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toLinearEquiv_injective : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  Function.Injective ⇑SpecialLinearGroup.toLinearEquiv
-- Mathlib.RingTheory.Unramified.Basic
/-- Localization at an element is unramified.  -/
Algebra.Unramified.of_isLocalization_Away : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] (r : R)
  [IsLocalization.Away r A], Algebra.Unramified R A
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.below.trans : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}
  {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop} {x y z : R} (a : RingConGen.Rel r x y)
  (a_1 : RingConGen.Rel r y z),
  RingConGen.Rel.below a → motive x y a → RingConGen.Rel.below a_1 → motive y z a_1 → RingConGen.Rel.below ⋯
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.transpose_mem_unitaryGroup_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  {U : Matrix n n α}, U.transpose ∈ Matrix.unitaryGroup n α ↔ U ∈ Matrix.unitaryGroup n α
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_modify : ∀ {α : Type u} {β : Type v} {m : Std.DHashMap.Internal.Raw₀ α fun x => β} [inst : BEq α] [EquivBEq α]
  [inst_2 : Hashable α] [LawfulHashable α],
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : β → β},
      (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.Const.modify m a f)).buckets).Perm
        (Std.Internal.List.Const.modifyKey a f (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.IsHadamard.congr_simp : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : Semiring R] [inst_4 : StarRing R] (A A_1 : Matrix n n R), A = A_1 → A.IsHadamard = A_1.IsHadamard
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The presheaf induced by a sieve is a subobject of the yoneda embedding.  -/
CategoryTheory.Sieve.uliftFunctorInclusion_is_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X),
  CategoryTheory.Mono S.uliftFunctorInclusion
-- Mathlib.Analysis.Normed.Ring.Lemmas
Int.instNormedCommRing : NormedCommRing ℤ
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_finset_subset_smul_finset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s t : Finset β}
  {a : α}, a • s ⊆ a • t ↔ s ⊆ t
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instIsMultiplicativeSchemeLocallyOfFiniteType : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.LocallyOfFiniteType
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Only assumes right strict covariance.  -/
Right.mul_lt_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightStrictMono α] {a b c d : α},
  a < b → c < d → a * c < b * d
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- The unique maximum-length word over the symbols above `0` is `Fin.succ`.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.S_zero_eq_singleton : ∀ {p : ℕ}, BirdDet.S✝ p 0 = {Fin.succ}
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.ColimitType.instAdd : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → Add (CommRingCat.Colimits.ColimitType F)
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_prodMk : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] (f : ι → M) (g : ι → N),
  (Function.mulSupport fun x => (f x, g x)) = Function.mulSupport f ∪ Function.mulSupport g
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.instHasShiftInt : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          CategoryTheory.HasShift (CategoryTheory.Pretriangulated.Triangle C) ℤ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.valuation.eq_1 : ∀ (R : Type u_2) [inst : Ring R] [inst_1 : ValuativeRel R],
  ValuativeRel.valuation R =
    { toFun := fun r => ValuativeRel.ValueGroupWithZero.mk r 1, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯,
      map_add_le_max' := ⋯ }
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLESpan : LE Std.Time.Nanosecond.Span
-- Mathlib.MeasureTheory.Constructions.Pi
MeasurableEquiv.arrowCongr'.eq_1 : ∀ {α₁ : Type u_8} {β₁ : Type u_9} {α₂ : Type u_10} {β₂ : Type u_11} [inst : MeasurableSpace β₁]
  [inst_1 : MeasurableSpace β₂] (hα : α₁ ≃ α₂) (hβ : β₁ ≃ᵐ β₂),
  MeasurableEquiv.arrowCongr' hα hβ = { toEquiv := hα.arrowCongr' ↑hβ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.CharP.intCast_eq_mod : ∀ (R : Type u_1) [inst : Ring R] (p : ℕ) [CharP R p] (k : ℤ), ↑k = ↑(k % ↑p)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ h₁' : S.LeftHomologyData) (h₂ h₂' : S.RightHomologyData),
  CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h₁ h₁')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂')
        (CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h₂' h₂))
-- Mathlib.GroupTheory.FiniteAbelian.Basic
AddCommGroup.finite_of_fg_isAddTorsion : ∀ (G : Type u) [inst : AddCommGroup G] [hG' : AddGroup.FG G], IsAddTorsion G → Finite G
-- Init.Data.Rat.Lemmas
Rat.ext : ∀ {p q : ℚ}, p.num = q.num → p.den = q.den → p = q
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.ichildren_mk : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (x : ↑F F.M) (i : F.Idx),
  PFunctor.M.ichildren i (PFunctor.M.mk x) = x.iget i
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback a `CompleteBooleanAlgebra` along an injection.  -/
Function.Injective.completeBooleanAlgebra : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : SupSet α] →
              [inst_5 : InfSet α] →
                [inst_6 : Top α] →
                  [inst_7 : Bot α] →
                    [inst_8 : Compl α] →
                      [inst_9 : HImp α] →
                        [inst_10 : SDiff α] →
                          [inst_11 : CompleteBooleanAlgebra β] →
                            (f : α → β) →
                              Function.Injective f →
                                (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                                  (∀ {x y : α}, f x < f y ↔ x < y) →
                                    (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                      (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                        (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
                                          (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) →
                                            f ⊤ = ⊤ →
                                              f ⊥ = ⊥ →
                                                (∀ (a : α), f aᶜ = (f a)ᶜ) →
                                                  (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) →
                                                    (∀ (a b : α), f (a \ b) = f a \ f b) → CompleteBooleanAlgebra α
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.mul_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f g : X ≃ₜ X) (x : X), (f * g) x = f (g x)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.inv_apply_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (e : α ≃ᵢ α) (x : α), e⁻¹ (e x) = x
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.copy_eq : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) (s : Set G) (hs : s = ↑K), K.copy s hs = K
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.coprod_inl_rightDistrib_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (∂R X Y Z).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.instSetLike : {α : Type u_1} → [inst : TopologicalSpace α] → SetLike (TopologicalSpace.PositiveCompacts α) α
-- Mathlib.Topology.Instances.EReal.Lemmas
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_top_top : ContinuousAt (fun p => p.1 * p.2) (⊤, ⊤)
-- Init.Grind.ToInt
Lean.Grind.IntInterval.co.sizeOf_spec : ∀ (lo hi : ℤ), sizeOf (Lean.Grind.IntInterval.co lo hi) = 1 + sizeOf lo + sizeOf hi
-- Mathlib.Algebra.Ring.Action.Basic
toRingHom_injective : ∀ (M : Type u_1) [inst : Monoid M] (R : Type v) [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R]
  [FaithfulSMul M R], Function.Injective (MulSemiringAction.toRingHom M R)
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.symm : ∀ {n a b : ℕ}, a ≡ b [MOD n] → b ≡ a [MOD n]
-- Mathlib.Analysis.Calculus.Deriv.Add
HasStrictDerivAt.fun_sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F},
  (∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x) → HasStrictDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinset_E : ∀ {α : Type u_1} [inst : DecidableEq α] (E : Set α) (Indep : Finset α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E),
  (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).E = E
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projective_iff_hasProjectiveDimensionLE_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.Projective X ↔ CategoryTheory.HasProjectiveDimensionLE X 0
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, panicking if no such element exists.
 -/
Std.TreeSet.getGE! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet α cmp → α → α
-- Mathlib.Data.Nat.Factorial.Basic
/-- Avoid in favor of `Nat.factorial_mul_descFactorial` if you can. ℕ-division isn't worth it.  -/
Nat.descFactorial_eq_div : ∀ {n k : ℕ}, k ≤ n → n.descFactorial k = n.factorial / (n - k).factorial
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.inlineIfReduceAttr : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Bool
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.add_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y y' : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F y y' → CommRingCat.Colimits.Relation F (x.add y) (x.add y')
-- Mathlib.SetTheory.Cardinal.NatCard
/-- NB: `Nat.card` is defined to be `0` for infinite types.  -/
Finite.card_eq_zero_of_embedding : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] (f : α ↪ β), Nat.card α = 0 → Nat.card β = 0
-- Batteries.Data.List.Lemmas
List.findIdxNth_cons : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {n : ℕ} {a : α},
  List.findIdxNth p (a :: xs) n =
    if n = 0 then if p a = true then 0 else List.findIdxNth p xs 0 + 1
    else if p a = true then List.findIdxNth p xs (n - 1) + 1 else List.findIdxNth p xs n + 1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a a_1 : NumberField.mixedEmbedding.mixedSpace K),
  a = a_1 → NumberField.mixedEmbedding.fundamentalCone K a = NumberField.mixedEmbedding.fundamentalCone K a_1
-- Mathlib.CategoryTheory.MarkovCategory.Basic
/-- Any morphism to the unit equals discard.  -/
CategoryTheory.MarkovCategory.eq_discard : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MarkovCategory C] (X : C) (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
  f = CategoryTheory.ComonObj.counit
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.bind.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok a s => h_1 a s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.State.mk.sizeOf_spec : ∀ (cache : Lean.Meta.Simp.Cache) (failureCache : Lean.ExprSet) (numSteps : ℕ) (msgLog : List String)
  (morTheorems transitionTheorems : Mathlib.Meta.FunProp.GeneralTheorems),
  sizeOf
      { cache := cache, failureCache := failureCache, numSteps := numSteps, msgLog := msgLog,
        morTheorems := morTheorems, transitionTheorems := transitionTheorems } =
    1 + sizeOf cache + sizeOf failureCache + sizeOf numSteps + sizeOf msgLog + sizeOf morTheorems +
      sizeOf transitionTheorems
-- Init.Data.List.Nat.Modify
List.modify_eraseIdx_of_lt : ∀ {α : Type u_1} (f : α → α) (i j : ℕ) (l : List α), j < i → (l.eraseIdx i).modify j f = (l.modify j f).eraseIdx i
-- Batteries.Util.ProofWanted
DerivedWanted.ofVal : {α : Sort u} → α → DerivedWanted α
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.antilipschitzConstant_of_injective_of_isClosed_range.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_5} {F : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace E]
  [inst_6 : CompleteSpace F] (f f_1 : E →L[𝕜] F) (e_f : f = f_1) (hf : Function.Injective ⇑f)
  (hf' : IsClosed (Set.range ⇑f)),
  f.antilipschitzConstant_of_injective_of_isClosed_range hf hf' =
    f_1.antilipschitzConstant_of_injective_of_isClosed_range ⋯ ⋯
-- Std.Time.DateTime
/-- Add `Day.Offset` to a `DateTime`.
 -/
Std.Time.DateTime.addDays : Std.Time.DateTime → Std.Time.Day.Offset → Std.Time.DateTime
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstHPowInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Given `x : X` and `y : Y` such that `f x = s = g y`, this is `κ(x) ⊗[κ(s)] κ(y)`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.tensor : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} → {g : Y ⟶ S} → AlgebraicGeometry.Scheme.Pullback.Triplet f g → CommRingCat
-- Lean.Meta.Match.Basic
/-- Original alternative index. Alternatives can be split, this index is the original
position of the alternative that generated this one.
 -/
Lean.Meta.Match.Alt.idx : Lean.Meta.Match.Alt → ℕ
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.mem_ae_dirac_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α},
  MeasurableSet s → (s ∈ MeasureTheory.ae (MeasureTheory.Measure.dirac a) ↔ a ∈ s)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Set.Functor
instLawfulAlternativeSetM : LawfulAlternative SetM
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_sigmaCurry : ∀ {ι : Type u_6} {κ : ι → Type u_7} {X : (i : ι) → κ i → Type u_8}
  [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)], Measurable Sigma.curry
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.pointReflection_symm : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (x : P₁), (AffineEquiv.pointReflection k x).symm = AffineEquiv.pointReflection k x
-- Lean.Elab.MutualInductive
/-- Performs the assignment that may be recorded in the result, while normalizing the level.  -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ResultingUniverseResult.assign : Lean.Elab.Command.ResultingUniverseResult✝ → Lean.MetaM Unit
-- Init.Data.Int.Order
Int.not_le : ∀ {a b : ℤ}, ¬a ≤ b ↔ b < a
-- Mathlib.Algebra.Star.StarAlgHom
/-- Copy of a `StarAlgHom` with a new `toFun` equal to the old one. Useful
to fix definitional equalities.  -/
StarAlgHom.copy : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] →
              [inst_4 : Semiring B] →
                [inst_5 : Algebra R B] → [inst_6 : Star B] → (f : A →⋆ₐ[R] B) → (f' : A → B) → f' = ⇑f → A →⋆ₐ[R] B
-- Lean.MetavarContext
Lean.getLevelMVarAssignment? : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.LMVarId → m (Option Lean.Level)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.traceState : Lean.Meta.Match.Problem → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.Cocone.ofPushoutCocone_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
  (t :
    CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
      (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)),
  (CategoryTheory.Limits.Cocone.ofPushoutCocone t).ι =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagramIsoSpan F).hom t.ι