mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.hom_ext'_iff : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {Z : C} {g h : ⨁ f ⟶ Z},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) g =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) h
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Embedding of a magma with zero into its magma algebra.  -/
AddMonoidAlgebra.of : (R : Type u_8) →
  (M : Type u_9) → [inst : Semiring R] → [inst_1 : AddZeroClass M] → Multiplicative M →* AddMonoidAlgebra R M
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.spanning_iff : ∀ {α : Type u_2} (M : Matroid α) (S : Set α), M.Spanning S ↔ M.closure S = M.E ∧ S ⊆ M.E
-- Lean.Setup
/-- Two nested arrays of variable size: `#[#[olean, oleanServer?, oleanPrivate?], #[irSig, ir?]]`
     -/
Lean.ImportArtifacts.toArrays : Lean.ImportArtifacts → Array (Array System.FilePath)
-- Mathlib.RingTheory.Congruence.Defs
/-- Coercion from a type with addition and multiplication to its quotient by a congruence relation.

See Note [use has_coe_t].  -/
RingCon.instCoeTCQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → (c : RingCon R) → CoeTC R c.Quotient
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α},
  List.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Const.toList t) = none ↔ k ∉ t
-- Mathlib.Logic.Equiv.Prod
Equiv.pprodEquivProd_apply : ∀ {α : Type u_9} {β : Type u_10} (x : α ×' β), Equiv.pprodEquivProd x = (x.fst, x.snd)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiff.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝕜' : Type u_4} [inst_3 : NormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {f : E → 𝕜'}, ContDiff 𝕜 n f → (∀ (x : E), f x ≠ 0) → ContDiff 𝕜 n f⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.coprod.desc_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F₁ F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ ⟶ F)
  (τ₂ : F₂ ⟶ F) (a : C),
  (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂).app a =
    TypeCat.ofHom
      (Sum.elim ⇑(CategoryTheory.ConcreteCategory.hom (τ₁.app a)) ⇑(CategoryTheory.ConcreteCategory.hom (τ₂.app a)))
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.sourceAffineLocally_respectsIso : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (AlgebraicGeometry.sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => P).toProperty.RespectsIso
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.zeta_of_le : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : One 𝕜] [inst_2 : LE α] [inst_3 : DecidableLE α] {a b : α},
  a ≤ b → (IncidenceAlgebra.zeta 𝕜) a b = 1
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- Prelax functors preserve compositions of 2-morphisms.  -/
CategoryTheory.PrelaxFunctor.map₂_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
-- Mathlib.Analysis.Convex.Basic
Antitone.convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Antitone f → ∀ (r : β), Convex 𝕜 {x | f x ≤ r}
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.y_continuous : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} [inst : TopologicalSpace S] [inst_1 : TopologicalSpace T]
  [inst_2 : TopologicalSpace X] (π : T → S × OnePoint X),
  autoParam (Continuous π) InternalProjectivityProof.y_continuous._auto_1✝ → Continuous (InternalProjectivityProof.y✝ π)
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- Removing an edge from `G` for each subgraph isomorphic to `H` results in a subgraph of `G`.  -/
SimpleGraph.killCopies_le_left : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, G.killCopies H ≤ G
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.spanning_iff_spanning : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I X → (M.Spanning I ↔ M.Spanning X)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- A family of elements for a presheaf `P` given a collection of arrows `R` with fixed codomain `X`
consists of an element of `P Y` for every `f : Y ⟶ X` in `R`.
A presheaf is a sheaf (resp, separated) if every *compatible* family of elements has exactly one
(resp, at most one) amalgamation.

This data is referred to as a `family` in [MM92], Chapter III, Section 4. It is also a concrete
version of the elements of the middle object in the Stacks entry which is
more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Elephant].
 -/
CategoryTheory.Presieve.FamilyOfElements : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Functor Cᵒᵖ (Type w) → CategoryTheory.Presieve X → Type (max (max u₁ w) v₁)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.List.takeWhile₂.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          ((a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)) →
            ((x : List α) →
                (x_2 : List β) →
                  (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_2 = b :: bs → False) → motive x x_2) →
              motive x x_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.udiv.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinOp.udiv = 1
-- Mathlib.Data.Num.ZNum
ZNum.cast_pos : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α] (n : PosNum), ↑(ZNum.pos n) = ↑n
-- Batteries.Tactic.Congr
/-- If `closePre := true`, it will attempt to close new goals using `Eq.refl`, `HEq.refl`, and
`assumption` with reducible transparency.  -/
Batteries.Tactic.Congr.Config.closePre : Batteries.Tactic.Congr.Config → Bool
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'}
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g),
  CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.factorizationData g).p =
    CategoryTheory.CategoryStruct.comp (data.factorizationData f).p (CategoryTheory.Arrow.Hom.right φ)
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  (K : CategoryTheory.Precoverage C) [self : P.IsLocalAtSource K],
  P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)
-- Init.Data.SInt.Bitwise
Int64.not_eq_comm : ∀ {a b : Int64}, ~~~a = b ↔ a = ~~~b
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.update_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] [inst_1 : Mul α] (u : m → α) (v : n → α) (i : m)
  (a : α), Matrix.vecMulVec (Function.update u i a) v = (Matrix.vecMulVec u v).updateRow i (a • v)
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_5.splitter : (motive : Option (List Lean.MVarId) → Sort u_1) →
  (procResult? : Option (List Lean.MVarId)) →
    ((curr' : List Lean.MVarId) → motive (some curr')) → (Unit → motive none) → motive procResult?
-- Init.Data.List.Lemmas
List.head?_eq_some_iff : ∀ {α : Type u_1} {xs : List α} {a : α}, xs.head? = some a ↔ ∃ ys, xs = a :: ys
-- Mathlib.CategoryTheory.SingleObj
/-- Monoid laws become category laws for the single object category.  -/
CategoryTheory.SingleObj.category : (M : Type u) → [Monoid M] → CategoryTheory.Category.{u, 0} (CategoryTheory.SingleObj M)
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
QuadraticForm.dualProdIsometry_invFun : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M ≃ₗ[R] N) (a : Module.Dual R N × N),
  (QuadraticForm.dualProdIsometry f).invFun a = (f.symm.dualMap.toAddEquiv.prodCongr f.toAddEquiv).symm a
-- Mathlib.Data.Ineq
Mathlib.instReprIneq.repr : Mathlib.Ineq → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Cones
/-- A cocone extended by an isomorphism is isomorphic to the original cone.  -/
CategoryTheory.Limits.Cocone.extendIso : {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 : CategoryTheory.Limits.Cocone F) → {X : C} → (f : s.pt ≅ X) → s ≅ s.extend f.hom
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_next_right : ∀ {s : String.Slice} (p : s.Pos) (hp : p ≠ s.endPos),
  p.Splits (s.sliceTo p).copy (String.singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy)
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNorm'_const_smul : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {𝕜 : Type u_3} [inst_1 : NormedDivisionRing 𝕜] [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F]
  {f : α → F} (c : 𝕜), 0 < q → MeasureTheory.eLpNorm' (c • f) q μ = ‖c‖ₑ * MeasureTheory.eLpNorm' f q μ
-- Mathlib.Data.NNRat.Defs
NNRat.den_coe : ∀ {q : ℚ≥0}, (↑q).den = q.den
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.stuck.injEq : ∀ (val val_1 : Lean.Expr),
  (Lean.Meta.ReduceMatcherResult.stuck val = Lean.Meta.ReduceMatcherResult.stuck val_1) = (val = val_1)
-- Mathlib.Order.WithBot
WithTop.linearOrder : {α : Type u_1} → [LinearOrder α] → LinearOrder (WithTop α)
-- Mathlib.Order.Lattice
Pi.inf_apply : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Min (α' i)] (f g : (i : ι) → α' i) (i : ι), (f ⊓ g) i = f i ⊓ g i
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Weighted generalized mean inequality, version for two elements of `ℝ≥0∞` and real
exponents.  -/
ENNReal.rpow_arith_mean_le_arith_mean2_rpow : ∀ (w₁ w₂ z₁ z₂ : ENNReal), w₁ + w₂ = 1 → ∀ {p : ℝ}, 1 ≤ p → (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.instGroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H],
  Monoid.Coprod.instGroup =
    { toMonoid := Monoid.Coprod.inst, toInv := Monoid.Coprod.instInv, div := DivInvMonoid.div', zpow := zpowRec,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Lean.Meta.ForEachExpr
/-- Auxiliary method for (temporarily) setting the user facing name of metavariables.
Let `?m` be a metavariable in `isTarget.contains ?m`, and `?m` does not have a user facing name.
Then, we try to find an application `f ... ?m` in `e`, and (temporarily) use the
corresponding parameter name (with a fresh macro scope) as the user facing name for `?m`.
This method returns all metavariables whose user facing name has been updated.
 -/
Lean.Meta.setMVarUserNamesAt : Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.MonoidalClosed.linearHomEquivComm_hom : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G)
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C),
  (Rep.Hom.hom ((Rep.MonoidalClosed.linearHomEquivComm A B C) f)).toLinearMap =
    TensorProduct.curry (Rep.Hom.hom f).toLinearMap
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π), MeasurableSet {ω | τ ω ≤ π ω}
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q], AlgebraicGeometry.IsZariskiLocalAtSource P
-- Mathlib.RepresentationTheory.Basic
Representation.leftRegular_norm_eq_zero_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G] (x : MonoidAlgebra k G),
  (Representation.leftRegular k G).norm x = 0 ↔ (Finsupp.linearCombination k fun x => 1) x.coeff = 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- The right injection into a product is a continuous linear map.  -/
ContinuousLinearMap.inr : (R : Type u_1) →
  [inst : Semiring R] →
    (M₁ : Type u_2) →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R M₁] →
            (M₂ : Type u_3) →
              [inst_4 : TopologicalSpace M₂] → [inst_5 : AddCommMonoid M₂] → [inst_6 : Module R M₂] → M₂ →L[R] M₁ × M₂
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.aeval_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R) [inst_2 : Algebra R S],
  (MvPolynomial.aeval g) ((MvPolynomial.rename k) p) = (MvPolynomial.aeval (g ∘ k)) p
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.coe_single_apply : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι)
  (x : G i) (j : ι), (RestrictedProduct.single A i x) j = Pi.single i x j
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
/-- The exact sequence with six terms starting from `(F.shift n₀).obj T.obj₁` until
`(F.shift n₁).obj T.obj₃` when `T` is a distinguished triangle and `F` a homological functor.  -/
CategoryTheory.Functor.homologySequenceComposableArrows₅ : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.HasShift C ℤ] →
        [inst_2 : CategoryTheory.Category.{v_3, u_3} A] →
          (F : CategoryTheory.Functor C A) →
            [F.ShiftSequence ℤ] →
              CategoryTheory.Pretriangulated.Triangle C →
                (n₀ n₁ : ℤ) → n₀ + 1 = n₁ → CategoryTheory.ComposableArrows A 5
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.ofAdd_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α], Multiplicative.ofAdd ⊤ = ⊤
-- Mathlib.FieldTheory.SeparableDegree
/-- If `x` and `y` are both separable elements, then `x + y` is also a separable element.  -/
Field.isSeparable_add : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x y : E},
  IsSeparable F x → IsSeparable F y → IsSeparable F (x + y)
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms an array of mappings into a tree map.  -/
Std.ExtDTreeMap.ofArray : {α : Type u} →
  {β : α → Type v} →
    Array ((a : α) × β a) →
      (cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap.ofArray._auto_1) → Std.ExtDTreeMap α β cmp
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_injective : ∀ {M : Type u_2} [inst : AddZeroClass M], Function.Injective AddSubmonoid.unop
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.eq_iff_le : ∀ {α : Type u} [inst : Semiring α] {I J : Ideal α}, I.IsMaximal → J ≠ ⊤ → (I = J ↔ I ≤ J)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A set of points in a two-dimensional space is coplanar.  -/
coplanar_of_fact_finrank_eq_two : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P) [h : Fact (Module.finrank k V = 2)], Coplanar k s
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.integerNormalization_coeff : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (p : Polynomial S) (i : ℕ),
  (IsLocalization.integerNormalization M p).coeff i = IsLocalization.coeffIntegerNormalization M p i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t t_1 : Std.TreeMap α β cmp) (e_t : t = t_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ t), t.getKey a h = t_1.getKey a_1 ⋯
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.unattach_eq_toIter_unattach_toIterM : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out}, it.attachWith P hP = (it.toIterM.attachWith P ⋯).toIter
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- `MeromorphicNFAt` is invariant under translation.  -/
meromorphicNFAt_comp_add_const_iff_meromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E}, MeromorphicNFAt (f ∘ fun x => x + c) x ↔ MeromorphicNFAt f (x + c)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.mem_factors'_iff_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a p : α},
  a ≠ 0 → ∀ (hp : Irreducible p), ⟨Associates.mk p, ⋯⟩ ∈ Associates.factors' a ↔ p ∣ a
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Criterion for checking that an adic Cauchy sequence is mapped to zero in the adic completion.  -/
AdicCompletion.mk_zero_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : AdicCompletion.AdicCauchySequence I M),
  (∃ k, ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤) → (AdicCompletion.mk I M) f = 0
-- Lean.Meta.SynthInstance
Lean.Meta.synthInstance.maxSize : Lean.Option ℕ
-- Mathlib.Algebra.Lie.Basic
lie_lie : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x y : L) (m : M),
  ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.map_ncard_setBernoulli_apply : ∀ {ι : Type u_1} [Countable ι] (u : Set ι) (p : ↑unitInterval) (s : Set ℕ),
  (MeasureTheory.Measure.map Set.ncard (ProbabilityTheory.setBernoulli u p)) s =
    (ProbabilityTheory.setBernoulli u p) {t | t ⊆ u ∧ t.ncard ∈ s}
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosReflectLE.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α]
  [toContravariantClass : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2],
  MulPosReflectLE α
-- Mathlib.Order.Defs.Unbundled
/-- `IsLinearOrder X r` means that the binary relation `r` on `X` is a linear order, that is,
`IsPartialOrder X r` and `Std.Total r`.  -/
IsLinearOrder : (α : Sort u_1) → (α → α → Prop) → Prop
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.mk : ℕ →
  ℕ →
    Option Lean.MVarId →
      Lean.Expr → Lean.Expr → Array Lean.Elab.Tactic.ElimApp.Alt → Array Lean.MVarId → Lean.Elab.Tactic.ElimApp.State✝
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_eq_empty_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M}, Function.mulSupport f = ∅ ↔ f = 1
-- Mathlib.Tactic.GCongr.Core
/-- This is used as the default main-goal discharger,
consisting of running `Lean.MVarId.gcongrForward` (trying a term together with limited
forward-reasoning on that term) on each nontrivial hypothesis.
 -/
Mathlib.Tactic.GCongr.gcongrForwardDischarger : Lean.MVarId → Lean.MetaM Bool
-- Init.Data.BitVec.Bitblast
BitVec.umulOverflow_eq : ∀ {w : ℕ} (x y : BitVec w),
  x.umulOverflow y =
    (decide (0 < w) && decide (BitVec.twoPow (w * 2) w ≤ BitVec.zeroExtend (w * 2) x * BitVec.zeroExtend (w * 2) y))
-- Mathlib.Order.SuccPred.Archimedean
BddBelow.exists_isLeast_of_nonempty : ∀ {X : Type u_3} [inst : LinearOrder X] [inst_1 : PredOrder X] [IsPredArchimedean X] {S : Set X},
  BddBelow S → S.Nonempty → ∃ x, IsLeast S x
-- Mathlib.Algebra.Tropical.BigOperators
Multiset.untrop_sum : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : OrderTop R] (s : Multiset (Tropical R)),
  Tropical.untrop s.sum = (Multiset.map Tropical.untrop s).inf
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- **Alias** of the forward direction of `IntermediateField.adjoin_eq_top_iff_of_isAlgebraic`. -/
Algebra.adjoin_eq_top_of_intermediateField : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  (∀ x ∈ S, IsAlgebraic F x) → IntermediateField.adjoin F S = ⊤ → Algebra.adjoin F S = ⊤
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.naturality_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso (α.app X)]
  [inst_3 : CategoryTheory.IsIso (α.app Y)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X)) (F.map f) =
    CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.inv (α.app Y))
-- Mathlib.Algebra.Group.Defs
/-- Multiplication by `(n + 1 : ℕ)` behaves as expected.  -/
AddMonoid.nsmul_succ : ∀ {M : Type u} [self : AddMonoid M] (n : ℕ) (x : M), (n + 1) • x = n • x + x
-- Mathlib.Data.Nat.Factorial.Basic
/-- `n.descFactorial k = n! / (n - k)!` (as seen in `Nat.descFactorial_eq_div`), but
implemented recursively to allow for "quick" computation when using `norm_num`. This is closely
related to `descPochhammer`, but much less general.  -/
Nat.descFactorial : ℕ → ℕ → ℕ
-- Mathlib.Order.Interval.Finset.Defs
Subtype.instLocallyFiniteOrder : {α : Type u_1} →
  [inst : Preorder α] → (p : α → Prop) → [DecidablePred p] → [LocallyFiniteOrder α] → LocallyFiniteOrder (Subtype p)
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).H =
    CategoryTheory.Abelian.coimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
-- Mathlib.Topology.ClusterPt
mem_closure_of_mem_closure_union : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s₁ s₂ : Set X},
  x ∈ closure (s₁ ∪ s₂) → s₁ᶜ ∈ nhds x → x ∈ closure s₂
-- Lean.Parser.Command
Lean.Parser.Command.declModifiersT.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOn.prodMap : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι}
  {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [inst_1 : UniformSpace β'] {F' : ι' → α' → β'} {p' : Filter ι'}
  {s' : Set α'},
  UniformCauchySeqOn F p s →
    UniformCauchySeqOn F' p' s' → UniformCauchySeqOn (fun i => Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')
-- Init.Data.BitVec.Lemmas
BitVec.xor_allOnes : ∀ {w : ℕ} {x : BitVec w}, x ^^^ BitVec.allOnes w = ~~~x