mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_mul : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : Mul β],
  MeasureTheory.stoppedValue (u * v) τ = MeasureTheory.stoppedValue u τ * MeasureTheory.stoppedValue v τ
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), Function.Bijective (WithAbs.toAbs v)
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.of_prod_one_sub : ∀ {R : Type u_1} [inst : CommRing R] {I : Type u_3} [inst_1 : Fintype I] {e : I → R},
  OrthogonalIdempotents e → ∏ i, (1 - e i) = 0 → CompleteOrthogonalIdempotents e
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.propagateUp : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.postAdjunctionRight_unit_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasPushouts D] {Y : D} {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (a : F ⊣ G) (X : CategoryTheory.Under ((CategoryTheory.Functor.id C).obj (G.1 Y))),
  ((CategoryTheory.Under.postAdjunctionRight a).unit.app X).right =
    CategoryTheory.CategoryStruct.comp (a.unit.app X.right)
      (G.map (CategoryTheory.Limits.pushout.inl (F.map X.hom) (a.counit.app Y)))
-- Init.Data.Dyadic.Basic
Rat.toDyadic.eq_1 : ∀ (x : ℚ) (n : ℕ), x.toDyadic (Int.ofNat n) = Dyadic.ofIntWithPrec (x.num <<< n / ↑x.den) (Int.ofNat n)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.coe_ofContinuousOpenRestrict_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)) (hs : IsOpen e.source),
  ↑(OpenPartialHomeomorph.ofContinuousOpenRestrict e hc ho hs).symm = ↑e.symm
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.ParserContext.mk : Lean.Parser.ParserContextCore → Lean.Parser.ParserContext
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instMulAction.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α],
  OrderDual.instMulAction = { toSMul := OrderDual.instSMul', mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Dynamics.Flow
/-- The forward orbit of a point `x` is contained in the orbit of `x`.  -/
Flow.forwardOrbit_subset_orbit : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) [inst_3 : Preorder τ] [inst_4 : AddLeftMono τ] (x : α), ϕ.forwardOrbit x ⊆ ϕ.orbit x
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.combineMinIdxOn.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 →
    ∀ {xs xs_1 : List α} (e_xs : xs = xs_1) {ys ys_1 : List α} (e_ys : ys = ys_1) (i i_1 : ℕ) (e_i : i = i_1)
      (j j_1 : ℕ) (e_j : j = j_1) (hi : i < xs.length) (hj : j < ys.length),
      List.combineMinIdxOn✝ f i j hi hj = List.combineMinIdxOn✝ f_1 i_1 j_1 ⋯ ⋯
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalSemiring.toContinuousAdd : ∀ {R : Type u_1} {inst : TopologicalSpace R} {inst_1 : NonUnitalNonAssocSemiring R} [self : IsTopologicalSemiring R],
  ContinuousAdd R
-- Mathlib.Algebra.Group.Prod
MonoidHom.comp_coprod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommMonoid P]
  {Q : Type u_6} [inst_3 : CommMonoid Q] (h : P →* Q) (f : M →* P) (g : N →* P),
  h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
/-- Simplifies `c = Nat.digitChar n` to `False` when `c` is a concrete character
not in the range of `digitChar` (i.e., not one of `'0'`-`'9'`, `'a'`-`'f'`, `'*'`).  -/
Char.Nat.reduceEqDigitChar : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_comp_left : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u v : V →ₗ[K] V₂} {u' : V₂ →ₗ[K] V₃}, u ≈ v → u' ∘ₗ u ≈ u' ∘ₗ v
-- Mathlib.Computability.RegularExpressions
RegularExpression.matchEpsilon.eq_6 : ∀ {α : Type u_1} (P : RegularExpression α), P.star.matchEpsilon = true
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_pos : ∀ {a : ENNReal}, 0 < a⁻¹ ↔ a ≠ ⊤
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instMulAction : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] →
          {𝕜 : Type u_5} →
            [inst_2 : Monoid 𝕜] → [inst_3 : MulAction 𝕜 γ] → [ContinuousConstSMul 𝕜 γ] → MulAction 𝕜 (α →ₘ[μ] γ)
-- Mathlib.Logic.Unique
/-- In a `Unique` type, every term is equal to the default element (from `Inhabited`).  -/
Unique.uniq : ∀ {α : Sort u} (self : Unique α) (a : α), a = default
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMul.eq_1 : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β], Matrix.kroneckerTMul R = Matrix.kroneckerMap fun x1 x2 => x1 ⊗ₜ[R] x2
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- Let `i : Fin (n + 2)`. Given a compatible family of morphisms `Δ[n] ⟶ X` for `j ≠ i`,
this is the glued morphism `Λ[n + 1, i] ⟶ X`.  -/
SSet.horn.IsCompatible.desc : {n : ℕ} →
  {X : SSet} →
    {i : Fin (n + 2)} →
      {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)} →
        SSet.horn.IsCompatible f → ((SSet.horn (n + 1) i).toSSet ⟶ X)
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.of.injEq : ∀ (carrier : Type u) [commSemiring : CommSemiring carrier] (carrier_1 : Type u)
  (commSemiring_1 : CommSemiring carrier_1),
  (CommSemiRingCat.of carrier = CommSemiRingCat.of carrier_1) = (carrier = carrier_1 ∧ commSemiring ≍ commSemiring_1)
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput.mk : Lean.Term → Aesop.RuleBuilderOptions → Aesop.PhaseSpec → Aesop.RuleBuilderInput
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The 2-morphism filling the triangle diagram.  -/
CategoryTheory.Bicategory.LeftExtension.unit : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          (t : CategoryTheory.Bicategory.LeftExtension f g) → g ⟶ CategoryTheory.CategoryStruct.comp f t.extension
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv_op_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (r : R),
  (Polynomial.opRingEquiv R) (MulOpposite.op ((Polynomial.monomial n) r)) = (Polynomial.monomial n) (MulOpposite.op r)
-- Mathlib.Algebra.Order.Monovary
Antivary.div_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β}, Antivary f₁ g → Monovary f₂ g → Antivary (f₁ / f₂) g
-- Mathlib.GroupTheory.ArchimedeanDensely
LinearOrderedCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] (g : G),
  ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)
-- Std.Data.Iterators.Producers.Monadic.Empty
/-- The internal state of the `IterM.empty` iterator.
 -/
Std.Iterators.Types.Empty : (Type w → Type w') → Type w → Type w
-- Mathlib.Order.SuccPred.Basic
isMax_of_succ_notMem : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Set α} [s.OrdConnected] [inst_2 : SuccOrder α] {a : ↑s},
  Order.succ ↑a ∉ s → IsMax a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sInf_singleton_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α], sInf {⊤} = ⊤
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_sub_left : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (a b c : G), nndist (a - b) (a - c) = nndist b c
-- Mathlib.Probability.Distributions.Exponential
/-- The exponential pdf is positive for all positive reals  -/
ProbabilityTheory.exponentialPDFReal_pos : ∀ {x r : ℝ}, 0 < r → 0 < x → 0 < ProbabilityTheory.exponentialPDFReal r x
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLiftEquiv_algebraMap_apply : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : IsIntegralClosure B₂ A L₂] [inst_22 : Algebra.IsAlgebraic K L] [inst_23 : Algebra.IsAlgebraic K L₂]
  (σ : B ≃ₐ[A] B₂) (x : B), (galLiftEquiv K L L₂ σ) ((algebraMap B L) x) = (algebraMap B₂ L₂) (σ x)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'XIso.congr_simp : ∀ {ι : 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']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i), K.truncGE'XIso e hi' hi = K.truncGE'XIso e hi' hi
-- Mathlib.Algebra.Order.Group.Cone
GroupConeClass.toSubmonoidClass : ∀ {S : Type u_1} {G : outParam (Type u_2)} {inst : CommGroup G} {inst_1 : SetLike S G} [self : GroupConeClass S G],
  SubmonoidClass S G
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PushoutCocone.op_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g), c.op.pt = Opposite.op c.pt
-- Mathlib.LinearAlgebra.Pi
/-- A linear map into `Fin n.succ → M₃` can be built out of a map into `M₃` and a map into
`Fin n → M₃`.  -/
LinearMap.vecCons : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] →
              [inst_4 : Module R M₂] → {n : ℕ} → (M →ₗ[R] M₂) → (M →ₗ[R] Fin n → M₂) → M →ₗ[R] Fin n.succ → M₂
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
FormalMultilinearSeries.derivSeries_coeff_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 𝕜 F) (n : ℕ),
  (p.derivSeries.coeff n) 1 = (n + 1) • p.coeff (n + 1)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.isoMk.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : Q.RespectsIso] {A B : P.Under Q X} (f f_1 : A.right ≅ B.right) (e_f : f = f_1)
  (w : CategoryTheory.CategoryStruct.comp A.hom f.hom = B.hom),
  CategoryTheory.MorphismProperty.Under.isoMk f w = CategoryTheory.MorphismProperty.Under.isoMk f_1 ⋯
-- Mathlib.RingTheory.Lasker
Submodule.IsMinimalPrimaryDecomposition.distinct : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {t : Finset (Submodule R M)},
  N.IsMinimalPrimaryDecomposition t →
    (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) fun J => (J.colon Set.univ).radical)
-- Init.Data.Option.Lemmas
Option.pmap_none : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), none = some a → p a},
  Option.pmap f none h = none
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.algebraMapCoeffs_repr_apply_apply : ∀ {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (b : Module.Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) (x : M) (a : ι),
  ((Module.Basis.algebraMapCoeffs A b h).repr x) a = (algebraMap R A) ((b.repr x) a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.HashMap.ofList l)[k']? = some v
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.add_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a b : α) (v₁ v₂ v : ℚ),
  (v == v₁ + v₂) = true →
    a = Lean.Grind.Field.NormNum.ofRat v₁ →
      b = Lean.Grind.Field.NormNum.ofRat v₂ → a + b = Lean.Grind.Field.NormNum.ofRat v
-- Mathlib.Data.Nat.Bitwise
Nat.lor_assoc : ∀ (n m k : ℕ), n ||| m ||| k = n ||| (m ||| k)
-- Mathlib.NumberTheory.Dioph
_private.Mathlib.NumberTheory.Dioph.0.«term_⊗_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.DedekindDomain.PID
IsPrincipalIdealRing.of_isDedekindDomain_of_uniqueFactorizationMonoid : ∀ (R : Type u_2) [inst : CommRing R] [IsDedekindDomain R] [UniqueFactorizationMonoid R], IsPrincipalIdealRing R
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.toReal_klDiv_smul_same : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      ∀ (c : NNReal), (InformationTheory.klDiv (c • μ) (c • ν)).toReal = ↑c * (InformationTheory.klDiv μ ν).toReal
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two `affineCombination`
expressions.  -/
Finset.sum_smul_vsub_eq_affineCombination_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ p₂ : ι → P),
  ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (Finset.affineCombination k s p₁) w -ᵥ (Finset.affineCombination k s p₂) w
-- Mathlib.FieldTheory.Perfect
frobeniusEquiv_symm_pow_p : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (frobeniusEquiv R p).symm x ^ p = x
-- Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
CategoryTheory.Limits.hasWidePullback_of_isTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C}
  (arrows : (j : ι) → objs j ⟶ B) [CategoryTheory.Limits.HasProduct objs] (hB : CategoryTheory.Limits.IsTerminal B),
  CategoryTheory.Limits.HasWidePullback B objs arrows
-- Lean.Meta.LitValues
/-- Return `some v` if `e` is a `Float` literal: an `OfScientific` or `OfNat` application, or `Neg.neg`
of either (e.g. `-1.5`).
 -/
Lean.Meta.getFloatValue? : Lean.Expr → Lean.MetaM (Option Float)
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.
This function exists for completeness and always returns false:
The closed upper bound is contained in the range, so
left-unbounded right-closed ranges are never empty.
 -/
Std.Ric.isEmpty : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Ric α → Bool
-- Mathlib.RingTheory.Flat.CategoryTheory
Module.Flat.iff_lTensor_preserves_shortComplex_exact : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R),
  Module.Flat R ↑M ↔
    ∀ (C : CategoryTheory.ShortComplex (ModuleCat R)),
      C.Exact → (C.map (CategoryTheory.MonoidalCategory.tensorLeft M)).Exact
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z},
  IsOpenQuotientMap g → IsOpenQuotientMap f → IsOpenQuotientMap (g ∘ f)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The isomorphism `op (P ⊞ Q) ≅ op P ⊞ op Q`.  -/
CategoryTheory.Limits.biprod.opIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P Q : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] → Opposite.op (P ⊞ Q) ≅ Opposite.op P ⊞ Opposite.op Q
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instHasFactorizationOverTrivialCofibrationsFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)],
  (HomotopicalAlgebra.trivialCofibrations (CategoryTheory.Over S)).HasFactorization
    (HomotopicalAlgebra.fibrations (CategoryTheory.Over S))
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- **Alias** of `Matroid.IsBasis.eq_exchange_of_sdiff_eq_singleton`. -/
Matroid.IsBasis.eq_exchange_of_diff_eq_singleton : ∀ {α : Type u_1} {M : Matroid α} {I X J : Set α} {e : α},
  M.IsBasis I X → M.IsBasis J X → I \ J = {e} → ∃ f ∈ J \ I, J = insert f I \ {e}
-- Mathlib.Data.List.Sigma
/-- Insert the pair `⟨a, b⟩` and erase the first pair with the key `a`.  -/
List.kinsert : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → β a → List (Sigma β) → List (Sigma β)
-- Mathlib.Algebra.Group.Defs
eq_inv_of_mul_eq_one_left : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → a = b⁻¹
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.contract_add : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
  p ≠ 0 → ∀ (f g : Polynomial R), Polynomial.contract p (f + g) = Polynomial.contract p f + Polynomial.contract p g
-- Init.Data.List.Erase
List.eraseP_comm : ∀ {α : Type u_1} {p q : α → Bool} {l : List α},
  (∀ a ∈ l, ¬p a = true ∨ ¬q a = true) → List.eraseP q (List.eraseP p l) = List.eraseP p (List.eraseP q l)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldlM_eq_foldlM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  Std.DTreeMap.Raw.foldlM f init t = List.foldlM (fun a b => f a b.fst b.snd) init t.toList
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhds_basis_ball_inv_nat_succ : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α},
  (nhds x).HasBasis (fun x => True) fun n => Metric.ball x (1 / (↑n + 1))
-- Init.Data.BitVec.Folds
BitVec.iunfoldr_getLsbD' : ∀ {w : ℕ} {α : Type u_1} {f : Fin w → α → α × Bool} (state : ℕ → α),
  (∀ (i : Fin w), (f i (state ↑i)).1 = state (↑i + 1)) →
    (∀ (i : Fin w), (BitVec.iunfoldr f (state 0)).2.getLsbD ↑i = (f i (state ↑i)).2) ∧
      (BitVec.iunfoldr f (state 0)).1 = state w
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.verticalClosedStrip.eq_1 : ∀ (a b : ℝ), Complex.HadamardThreeLines.verticalClosedStrip a b = Complex.re ⁻¹' Set.Icc a b
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.basisOf_apply : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (i : ι) (j : { j // j ≠ i }),
  (b.basisOf i) j = b ↑j -ᵥ b i
-- Mathlib.Data.List.Sym
_private.Mathlib.Data.List.Sym.0.List.sym.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (x : ℕ) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (x : ℕ) → motive x []) (h_3 : (n : ℕ) → (x : α) → (xs : List α) → motive n.succ (x :: xs)),
  (x = 0 → False) →
    (match x, [] with
      | 0, x => h_1 x
      | x, [] => h_2 x
      | n.succ, x :: xs => h_3 n x xs) =
      h_2 x
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentItem.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {languageId : String} {version : ℕ} {text : String} {uri_1 : Lean.Lsp.DocumentUri}
  {languageId_1 : String} {version_1 : ℕ} {text_1 : String},
  { uri := uri, languageId := languageId, version := version, text := text } =
      { uri := uri_1, languageId := languageId_1, version := version_1, text := text_1 } →
    uri = uri_1 ∧ languageId = languageId_1 ∧ version = version_1 ∧ text = text_1
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) {g : σ → S}
  {p : MvPolynomial σ R}, (∀ i ∈ p.vars, g i = 0) → (MvPolynomial.eval₂Hom f g) p = f (MvPolynomial.constantCoeff p)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n (Option γ)}
  {g : γ → Std.Iterators.PostconditionT o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapWithPostcondition g (Std.IterM.filterMapWithPostcondition f it)).toList =
    (Std.IterM.filterMapWithPostcondition
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toList
-- Lean.Meta.Tactic.Grind.Extension
/-- Inserts `declName ↦ prio` into `s`.  -/
Lean.Meta.Grind.SymbolPriorities.insert : Lean.Meta.Grind.SymbolPriorities → Lean.Name → ℕ → Lean.Meta.Grind.SymbolPriorities
-- Mathlib.Data.Bundle
/-- The pullback of a bundle `E` over a base `B` under a map `f : B' → B`, denoted by
`Bundle.Pullback f E` or `f *ᵖ E`, is the bundle over `B'` whose fiber over `b'` is `E (f b')`.  -/
Bundle.«term_*ᵖ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.exists_triangle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (A : C) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    ∃ X Y,
      ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y),
        ∃ f g h,
          CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.mk.inj : ∀ {α : Type u} {as as_1 : α}, { as := as } = { as := as_1 } → as = as_1