mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.NAry
/-- The other direction does not hold because of the `h`-`h` cross terms on the RHS.  -/
Filter.map₂_distrib_le_right : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9}
  {f : Filter α} {g : Filter β} {h : Filter γ} {m : δ → γ → ε} {n : α → β → δ} {m₁ : α → γ → α'} {m₂ : β → γ → β'}
  {n' : α' → β' → ε},
  (∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)) →
    Filter.map₂ m (Filter.map₂ n f g) h ≤ Filter.map₂ n' (Filter.map₂ m₁ f h) (Filter.map₂ m₂ g h)
-- Init.Prelude
Nat.ble_succ_eq_true : ∀ {n m : ℕ}, n.ble m = true → n.ble m.succ = true
-- Mathlib.Order.Fin.Basic
Fin.natAdd_lt_natAdd_iff : ∀ {n : ℕ} (m : ℕ) {i j : Fin n}, Fin.natAdd m i < Fin.natAdd m j ↔ i < j
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.lift_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (hP : CategoryTheory.IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (hP.lift h k w) snd = k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_eq_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α} {fallback : β} {h : a ∈ m},
  Std.DHashMap.Const.get m a h = Std.DHashMap.Const.getD m a fallback
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `HasDerivAt.fun_finsetProd`. -/
HasDerivAt.fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'},
  (∀ i ∈ u, HasDerivAt (f i) (f' i) x) →
    HasDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNontrivial : ∀ {α : Type u_1} {l : Filter α} {R : Type u_5} [Nontrivial R] [l.NeBot], Nontrivial (l.Germ R)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.of_isAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [h : AlgebraicGeometry.IsAffineHom f], AlgebraicGeometry.IsSeparated f
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toReal_add : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f g : CompactlySupportedContinuousMap α NNReal),
  (f + g).toReal = f.toReal + g.toReal
-- Init.Omega.IntList
Lean.Omega.IntList.sum_neg : ∀ (xs : Lean.Omega.IntList), (-xs).sum = -xs.sum
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_counitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).counitIso =
    CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The only `R`-alternating map from two or more copies of `R` is the zero map.  -/
AlternatingMap.uniqueOfCommRing : {N : Type u_3} →
  [inst : AddCommMonoid N] →
    {ι : Type u_7} →
      {R : Type u_12} →
        [inst_1 : CommSemiring R] → [inst_2 : Module R N] → [Finite ι] → [Nontrivial ι] → Unique (R [⋀^ι]→ₗ[R] N)
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.terminal.subsingleton_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] {A : C}, Subsingleton (⊤_ C ⟶ A)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.copy_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (m : F.I ⟶ Y) (e : X ⟶ F.I)
  (hm : autoParam (m = F.m) CategoryTheory.Limits.IsImage.copy._auto_1)
  (he : autoParam (e = F.e) CategoryTheory.Limits.IsImage.copy._auto_3)
  (F' : CategoryTheory.Limits.MonoFactorisation f), (hF.copy m e hm he).lift F' = hF.lift F'
-- Mathlib.Algebra.Homology.Single
/-- Constructor for morphisms from a single homological complex.  -/
HomologicalComplex.mkHomFromSingle : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            {c : ComplexShape ι} →
              {K : HomologicalComplex V c} →
                {j : ι} →
                  {A : V} →
                    (φ : A ⟶ K.X j) →
                      (∀ (k : ι), c.Rel j k → CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0) →
                        ((HomologicalComplex.single V c j).obj A ⟶ K)
-- Mathlib.Order.KrullDimension
Order.height_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
  Order.height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n
-- Std.Data.ExtHashMap.Lemmas
_private.Std.Data.ExtHashMap.Lemmas.0.GetElem?.match_1.eq_2 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match none with
    | some e => h_1 e
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.Complex.Basic
Complex.re_le_re : ∀ {x y : ℂ}, x ≤ y → x.re ≤ y.re
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.getKey? t.maxKey! = some t.maxKey!
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_sum : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) {ι : Type u_2} (s : Finset ι) (φ : ι → MvPolynomial σ R),
  (MvPolynomial.aeval f) (∑ i ∈ s, φ i) = ∑ i ∈ s, (MvPolynomial.aeval f) (φ i)
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.iterate_derivative_at_1_eq_zero_of_lt : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ) {ν k : ℕ},
  k < n - ν → Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0
-- Init.Data.Nat.Basic
Nat.succ_pred_eq_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → n.pred.succ = n
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.ne_infty_iff_exists : ∀ {X : Type u_1} {x : OnePoint X}, x ≠ OnePoint.infty ↔ ∃ y, ↑y = x
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.find?_eq_findM? : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  {it : Std.Iter β} {f : β → Bool}, it.find? f = (it.findM? fun x => pure { down := f x }).run
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Constructs the array of values of the map.  -/
RBTree.RBMap.Values.toArray : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → Array β
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_neg : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalRing R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  cfc (fun x => -f x) a = -cfc f a
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourier_comp_linearIsometry : ∀ {V : Type u_1} {W : Type u_2} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  [inst_2 : NormedAddCommGroup V] [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V]
  [inst_6 : NormedAddCommGroup W] [inst_7 : InnerProductSpace ℝ W] [inst_8 : MeasurableSpace W] [inst_9 : BorelSpace W]
  [inst_10 : FiniteDimensional ℝ W] [inst_11 : FiniteDimensional ℝ V] (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W),
  FourierTransform.fourier (f ∘ ⇑A) w = FourierTransform.fourier f (A w)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_2 : ∀ (S : Finset Turing.PartrecToTM2.Λ') (k : Turing.PartrecToTM2.K')
  (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.push k s q) = Turing.PartrecToTM2.Λ'.Supports S q
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.compCreatesFiniteCoproducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                [CategoryTheory.Limits.CreatesFiniteCoproducts F] →
                  [CategoryTheory.Limits.CreatesFiniteCoproducts G] →
                    CategoryTheory.Limits.CreatesFiniteCoproducts (F.comp G)
-- Mathlib.RingTheory.DedekindDomain.Different
differentIdeal.congr_simp : ∀ (A : Type u_1) (B : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain B] [inst_5 : Module.IsTorsionFree A B], differentIdeal A B = differentIdeal A B
-- Lean.Compiler.LCNF.Basic
/-- Given `fvarId : [t]object`, obtain the underlying scalar value.  -/
Lean.Compiler.LCNF.LetValue.unbox : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_23 →
      Lean.Compiler.LCNF.LetValue pu
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.associatorNatIsoMiddleCat_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d)
  (X : ↑(CategoryTheory.Cat.of (b ⟶ c))),
  (CategoryTheory.Bicategory.associatorNatIsoMiddleCat f h).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator f X h).inv
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.instIsMarkovKernel_toKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {x : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β}
  {hf : ProbabilityTheory.IsCondKernelCDF f κ ν},
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.IsCondKernelCDF.toKernel f hf)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the
cardinality of the basis.  -/
Module.finrank_eq_card_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type w} [inst_4 : Fintype ι] (h : Module.Basis ι R M), Module.finrank R M = Fintype.card ι
-- Std.Time.Date.PlainDate
/-- Adds a given number of months to a `PlainDate`, rolling over any excess days into the following month.
 -/
Std.Time.PlainDate.addMonthsRollOver : Std.Time.PlainDate → Std.Time.Month.Offset → Std.Time.PlainDate
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A closed subset of a countably compact space is countably compact.  -/
IsClosed.isCountablyCompact : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E} [CountablyCompactSpace E], IsClosed A → IsCountablyCompact A
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.preimage_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y Z : C} [inst_2 : F.Full] [F.Faithful] (f : F.obj X ⟶ F.obj Y)
  (g : F.obj Y ⟶ F.obj Z),
  F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)
-- Mathlib.Analysis.InnerProductSpace.l2Space
IsHilbertSum.ofSurjective : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (OrthogonalFamily : OrthogonalFamily 𝕜 G V), Function.Surjective ⇑OrthogonalFamily.linearIsometry → IsHilbertSum 𝕜 G V
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
Derivation.mk'.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCancelCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] (D D_1 : A →ₗ[R] M) (e_D : D = D_1)
  (h : ∀ (a b : A), D (a * b) = a • D b + b • D a), Derivation.mk' D h = Derivation.mk' D_1 ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.category : {R : Type u} → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (QuadraticModuleCat R)
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.trans_isIntegral : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsAlgebraic R S] [int : Algebra.IsIntegral S A], Algebra.IsAlgebraic R A
-- Mathlib.Data.Rel
SetRel.refl : ∀ {α : Type u_1} (R : SetRel α α) [R.IsRefl] (a : α), (a, a) ∈ R
-- Mathlib.Algebra.Torsor.Basic
Prod.snd_smul : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'] (v : G × G') (p : P × P'), (v • p).2 = v.2 • p.2
-- Mathlib.Algebra.GCDMonoid.Basic
/-- If a monoid's only unit is `1`, then it is isomorphic to its associates.  -/
associatesEquivOfUniqueUnits : {α : Type u_1} → [inst : CommMonoidWithZero α] → [Subsingleton αˣ] → Associates α ≃* α
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_self_le : ∀ {x k : ℤ}, 0 ≤ x → k * x.tdiv k ≤ x
-- Mathlib.Algebra.Order.Group.PosPart
posPart_add_negPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α), a⁺ + a⁻ = |a|
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le : {α : Type u_1} → [LE α] → LE (WithZero α)
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.mk.injEq : ∀ (X : Type u) (point : X) (X_1 : Type u) (point_1 : X_1),
  ({ X := X, point := point } = { X := X_1, point := point_1 }) = (X = X_1 ∧ point ≍ point_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.pointEquivSubtype_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {x y : R} {h : W'.Equation x y} {p : W'.Point → Prop}
  (p0 : p WeierstrassCurve.Affine.Point.zero) (ph : p (WeierstrassCurve.Affine.Point.mk h)),
  (WeierstrassCurve.Affine.pointEquivSubtype p0) ⟨WeierstrassCurve.Affine.Point.mk h, ph⟩ = some ⟨(x, y), ⋯⟩
-- Mathlib.Analysis.RCLike.Basic
RCLike.enorm_conj : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ‖(starRingEnd K) z‖ₑ = ‖z‖ₑ
-- Mathlib.Order.SupClosed
InfClosed.insert_upperBounds : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α} {a : α}, InfClosed s → a ∈ upperBounds s → InfClosed (insert a s)
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_map_left_right : ∀ {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 : B.op.obj X₃ ⟶ R.op.obj X₂) {f f' : (w.op.StructuredArrowRightwards g)ᵒᵖ} (φ : f ⟶ f'),
  ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g).map φ).left.right =
    (CategoryTheory.StructuredArrow.Hom.right φ.unop).left.unop
-- Mathlib.Algebra.Notation
/-- A notation class for the *negative part* function (multiplicative version): `a⁻ᵐ`.  -/
LeOnePart : Type u_1 → Type u_1
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.coe_centralizer : ∀ {M : Type u_1} (S : Set M) [inst : Semigroup M], ↑(Subsemigroup.centralizer S) = S.centralizer
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln_mono : ∀ {k₁ k₂ : ℕ} {c : Nat.Partrec.Code} {n x : ℕ},
  k₁ ≤ k₂ → x ∈ Nat.Partrec.Code.evaln k₁ c n → x ∈ Nat.Partrec.Code.evaln k₂ c n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.category_id_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'),
  (CategoryTheory.CategoryStruct.id ψ).base = CategoryTheory.CategoryStruct.id ψ.base
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_upperBounds_eq_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  BddAbove s → s.Nonempty → sInf (upperBounds s) = sSup s
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_submatrix : ∀ {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} {n : Type un} [inst : Semiring R] (A : Matrix m n R)
  (em : m₀ ≃ m) (en : n₀ ≃ n), (A.submatrix ⇑em ⇑en).eRank = A.eRank
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_zero : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Nonempty n],
  Matrix.det 0 = 0
-- Mathlib.Data.Set.Image
Set.range_ite_subset' : ∀ {α : Type u_1} {β : Type u_2} {p : Prop} [inst : Decidable p] {f g : α → β},
  Set.range (if p then f else g) ⊆ Set.range f ∪ Set.range g
-- Mathlib.Order.Monotone.Defs
Monotone.iterate : ∀ {α : Type u} [inst : Preorder α] {f : α → α}, Monotone f → ∀ (n : ℕ), Monotone f^[n]
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
CFC.monotoneOn_one_sub_one_add_inv : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A],
  MonotoneOn (cfcₙ fun x => 1 - (1 + x)⁻¹) (Set.Ici 0)
-- Mathlib.Analysis.Convex.StrictConvexBetween
eq_midpoint_of_dist_eq_half : ∀ {E : Type u_3} {PE : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E]
  [inst_3 : MetricSpace PE] [inst_4 : NormedAddTorsor E PE] {x y z : PE},
  dist x y = dist x z / 2 → dist y z = dist x z / 2 → y = midpoint ℝ x z
-- Aesop.Stats.Extension
Aesop.StatsExtensionEntry.mk.inj : ∀ {aesopStx : Lean.Syntax} {fileName : String} {position? : Option Lean.Position} {stats : Aesop.Stats}
  {aesopStx_1 : Lean.Syntax} {fileName_1 : String} {position?_1 : Option Lean.Position} {stats_1 : Aesop.Stats},
  { aesopStx := aesopStx, fileName := fileName, position? := position?, stats := stats } =
      { aesopStx := aesopStx_1, fileName := fileName_1, position? := position?_1, stats := stats_1 } →
    aesopStx = aesopStx_1 ∧ fileName = fileName_1 ∧ position? = position?_1 ∧ stats = stats_1
-- Lean.Elab.Tactic.Basic
/-- Use `parentTag` to tag untagged goals at `newGoals`.
If there are multiple new untagged goals, they are named using `<parentTag>.<newSuffix>_<idx>` where `idx > 0`.
If there is only one new untagged goal, then we just use `parentTag`  -/
Lean.Elab.Tactic.tagUntaggedGoals : Lean.Name → Lean.Name → List Lean.MVarId → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instInvolutiveNeg.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveNeg α], Lex.instInvolutiveNeg = { toNeg := Lex.instNeg, neg_neg := ⋯ }
-- Init.Data.List.Sublist
List.drop_suffix : ∀ {α : Type u_1} (i : ℕ) (l : List α), List.drop i l <:+ l
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p`, `choose (p ^ k * a) (p ^ k * b)` is congruent to `choose a b` modulo `p`.
Also see `choose_pow_mul_pow_mul_modEq_choose` for the version with `ZMOD`.  -/
Choose.choose_pow_mul_pow_mul_modEq_choose_nat : ∀ {k a b p : ℕ} [Fact (Nat.Prime p)], (p ^ k * a).choose (p ^ k * b) ≡ a.choose b [MOD p]
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {newWidth : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig newWidth → Sort u_1) →
            (target : Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig newWidth) →
              ((w n : ℕ) →
                  (inner : aig.RefVec w) → (h : newWidth = w * n) → motive { w := w, n := n, inner := inner, h := h }) →
                motive target
-- Lean.Expr
Lean.instReprLiteral : Repr Lean.Literal
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- Given a finite collection of finite subsets $B_1, \ldots, B_k$
and, for every $x \in \bigcup_i B_i$, let $C_x$ be the set of indices
of the $B_i$'s that contain $x$.  Then, $\sum_i |B_i| = \sum_x |C_x|$.  -/
Finset.sum_card_eq_sum_biUnion_card : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableEq β] (B : α → Finset β)
  (s : Finset α), ∑ j ∈ s, (B j).card = ∑ x ∈ s.biUnion B, {j | j ∈ s ∧ x ∈ B j}.card
-- Init.Data.String.Decode
UInt8.utf8ByteSize : (c : UInt8) → c.IsUTF8FirstByte → ℕ
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.liftNCAlgHom.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} {B : Type u_5}
  [inst_2 : Semiring A] [inst_3 : Algebra k A] [inst_4 : Semiring B] [inst_5 : Algebra k B]
  [inst_6 : MulSemiringAction G A] [inst_7 : SMulCommClass G k A] (f : A →ₐ[k] B) (g : G →* B)
  (h_comm : ∀ {x : A} {y : G}, f (y • x) * g y = g y * f x),
  SkewMonoidAlgebra.liftNCAlgHom f g h_comm = { toRingHom := SkewMonoidAlgebra.liftNCRingHom (↑f) g ⋯, commutes' := ⋯ }
-- Mathlib.RingTheory.Ideal.Int
Int.card_ideal_quot : ∀ (n : ℕ), Nat.card (ℤ ⧸ Ideal.span {↑n}) = n
-- Mathlib.Algebra.Group.Pi.Basic
Pi.mulOneClass : {I : Type u} → {f : I → Type v₁} → [(i : I) → MulOneClass (f i)] → MulOneClass ((i : I) → f i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_smul_eq : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {𝕜' : Type u_6} {c : 𝕜'} [inst_5 : NormedDivisionRing 𝕜'] [inst_6 : Module 𝕜' F]
  [inst_7 : NormSMulClass 𝕜' F] [inst_8 : SMulCommClass 𝕜 𝕜' F], c ≠ 0 → (c • p).radius = p.radius
-- Mathlib.Algebra.Ring.Defs
/-- **Alias** of `mul_sub_right_distrib`. -/
sub_mul : ∀ {α : Type u} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * c
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunital : ∀ {R : Type u_1} [inst : NonUnitalRing R] {s : Set R} {z : R},
  z ∈ TwoSidedIdeal.span s ↔ z ∈ AddSubgroup.closure (s ∪ s * Set.univ ∪ Set.univ * s ∪ Set.univ * s * Set.univ)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- The functor `forgetToPresheafedSpace : SheafedSpace C ⥤ PresheafedSpace C`
is fully faithful.  -/
AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.FullyFaithful