mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.linearDeriv.congr_simp : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f f_1 : ContinuousMultilinearMap R M₁ M₂),
  f = f_1 →
    ∀ [inst_7 : ContinuousAdd M₂] [inst_8 : DecidableEq ι] [inst_9 : Fintype ι] (x x_1 : (i : ι) → M₁ i),
      x = x_1 → f.linearDeriv x = f_1.linearDeriv x_1
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_pi_empty : ∀ {ι : Type u} {α : ι → Type v} [inst : Fintype ι] [inst_1 : IsEmpty ι] {m : (i : ι) → MeasurableSpace (α i)}
  (μ : (i : ι) → MeasureTheory.Measure (α i)),
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit))
    (MeasureTheory.Measure.pi μ) (MeasureTheory.Measure.dirac ())
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.funMap_one : ∀ {M : Type u_2} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] {v : Fin 0 → M},
  FirstOrder.Language.Structure.funMap FirstOrder.presburgerFunc.one v = 1
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Int.Internal.Linear.Poly.denoteExpr : (ℕ → Lean.Expr) → Int.Internal.Linear.Poly → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.IsoCat
/-- An isomorphism of categories: a pair of functors whose composites are equal to the
identity functors.  -/
CategoryTheory.IsoCat : (C : Type u_1) →
  (D : Type u_2) →
    [CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.Category.{v_2, u_2} D] → Type (max (max (max u_1 u_2) v_1) v_2)
-- Mathlib.Topology.Constructions.SumProd
TopologicalSpace.prod_mono : ∀ {α : Type u_5} {β : Type u_6} {σ₁ σ₂ : TopologicalSpace α} {τ₁ τ₂ : TopologicalSpace β},
  σ₁ ≤ σ₂ → τ₁ ≤ τ₂ → instTopologicalSpaceProd ≤ instTopologicalSpaceProd
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.«termλ» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The opcycles functor `ShortComplex C ⥤ C` which sends a short complex `S` to `S.opcycles`
which is a cokernel of `S.f : S.X₁ ⟶ S.X₂`.  -/
CategoryTheory.ShortComplex.opcyclesFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasKernels C] →
        [CategoryTheory.Limits.HasCokernels C] → CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
-- Mathlib.Algebra.Order.Monovary
monovaryOn_neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn (-f) (-g) s ↔ MonovaryOn f g s
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.mk.sizeOf_spec : ∀ {m : Type u → Type u} [inst : (a : Type u) → SizeOf (m a)] (listM : Type u → Type u) (nil : {α : Type u} → listM α)
  (cons : {α : Type u} → α → listM α → listM α) (thunk : {α : Type u} → (Unit → listM α) → listM α)
  (squash : {α : Type u} → (Unit → m (listM α)) → listM α)
  (uncons : {α : Type u} → [Monad m] → listM α → m (Option (α × listM α)))
  (uncons? : {α : Type u} → listM α → Option (Option (α × listM α))),
  sizeOf
      { listM := listM, nil := nil, cons := cons, thunk := thunk, squash := squash, uncons := uncons,
        uncons? := uncons? } =
    1
-- Lean.Elab.Binders
Lean.Elab.Term.elabLetDelayedDecl : Lean.Elab.Term.TermElab
-- Init.Prelude
Array.appendCore.loop : {α : Type u} → Array α → ℕ → ℕ → Array α → Array α
-- Mathlib.FieldTheory.Perfect
coe_iterateFrobeniusEquiv : ∀ (R : Type u_1) (p n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  ⇑(iterateFrobeniusEquiv R p n) = ⇑(iterateFrobenius R p n)
-- Std.Time.Format.Modifier
Std.Time.Modifier.V.inj : ∀ {presentation presentation_1 : Std.Time.ZoneId},
  Std.Time.Modifier.V presentation = Std.Time.Modifier.V presentation_1 → presentation = presentation_1
-- Mathlib.RingTheory.FormalGroup.Basic
/-- `F.Point σ` represents the mathematical space of points of a formal group $F$
taking values in the formal power series ring `MvPowerSeries σ R` with the property
that constant coefficient is nilpotent.

TODO: Mathematically, a 1-dimensional formal group law $F$ over a ring $R$ defines a group
structure on the elements of a complete local $R$-algebra (specifically, its maximal ideal)
via the substitution operation $x +_F y = F(x, y)$.  -/
FormalGroup.Point : {R : Type u_1} → [inst : CommRing R] → FormalGroup R → Type u_6 → Type (max 0 u_1 u_6)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.incMod : ℕ → ℕ → ℕ
-- Mathlib.Dynamics.Flow
Flow.cont' : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (self : Flow τ α), Continuous (Function.uncurry self.toFun)
-- Mathlib.GroupTheory.Finiteness
Subgroup.FG.eq_1 : ∀ {G : Type u_3} [inst : Group G] (P : Subgroup G), P.FG = ∃ S, Subgroup.closure ↑S = P
-- Mathlib.Order.Lex
instDecidableEqColex : (α : Type u_2) → [DecidableEq α] → DecidableEq (Colex α)
-- Mathlib.Computability.TuringMachine.Tape
Turing.Dir.ofNat_ctorIdx : ∀ (x : Turing.Dir), Turing.Dir.ofNat x.ctorIdx = x
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instIsCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsCancelMul α], IsCancelMul (Colex α)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Build an isomorphism in the category `MonCat` from a `MulEquiv` between `Monoid`s.  -/
MulEquiv.toMonCatIso : {X Y : Type u} → [inst : Monoid X] → [inst_1 : Monoid Y] → X ≃* Y → (MonCat.of X ≅ MonCat.of Y)
-- Mathlib.Order.SupClosed
/-- **Alias** of the reverse direction of `infClosure_eq_self`. -/
InfClosed.infClosure_eq : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α}, InfClosed s → infClosure s = s
-- Mathlib.Order.Filter.Prod
Filter.prod_map_map_eq' : ∀ {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} (f : α₁ → α₂) (g : β₁ → β₂) (F : Filter α₁)
  (G : Filter β₁), Filter.map f F ×ˢ Filter.map g G = Filter.map (Prod.map f g) (F ×ˢ G)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.mk_inv_mul_mk_eq_one : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units),
  ⟨(Units.coeHom M) x⁻¹, ⋯⟩ * ⟨(Units.coeHom M) x, ⋯⟩ = 1
-- Std.Http.Internal.IndexMultiMap
_private.Std.Http.Internal.IndexMultiMap.0.Std.Internal.IndexMultiMap.insert.match_1.congr_eq_2 : ∀ (motive : Option (Array ℕ) → Sort u_1) (x : Option (Array ℕ)) (h_1 : (idxs : Array ℕ) → motive (some idxs))
  (h_2 : Unit → motive none),
  x = none →
    (match x with
      | some idxs => h_1 idxs
      | none => h_2 ()) ≍
      h_2 ()
-- Mathlib.AlgebraicGeometry.Artinian
/-- **Alias** of `AlgebraicGeometry.IsLocallyArtinian.discreteTopology`. -/
AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyArtinian X], DiscreteTopology ↥X
-- Init.Data.String.Basic
String.Slice.Pos.byte.eq_1 : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos), pos.byte h = s.getUTF8Byte pos.offset ⋯
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The pushforward of sheaves of modules by the identity morphism identifies
to the identity functor.  -/
AlgebraicGeometry.Scheme.Modules.pushforwardId : (X : AlgebraicGeometry.Scheme) →
  AlgebraicGeometry.Scheme.Modules.pushforward (CategoryTheory.CategoryStruct.id X) ≅
    CategoryTheory.Functor.id X.Modules
-- Mathlib.Tactic.Linter.Style
/-- The `setOption` linter emits a warning on a `set_option` command, term or tactic
which sets a `pp`, `profiler` or `trace` option.
It also warns on an option containing `maxHeartbeats`
(as these should be scoped as `set_option ... in` instead).  -/
Mathlib.Linter.linter.style.setOption : Lean.Option Bool
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- `S ⧸ P` embeds into the quotient by `P^(i+1) ⧸ P^e` as a subspace of `P^i ⧸ P^e`.  -/
Ideal.quotientToQuotientRangePowQuotSucc : {R : Type u} →
  [inst : CommRing R] →
    {S : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            (P : Ideal S) →
              [hfp : NeZero (p.ramificationIdx' P)] →
                {i : ℕ} →
                  {a : S} →
                    a ∈ P ^ i →
                      S ⧸ P →ₗ[R ⧸ p]
                        ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ i)) ⧸
                          (p.powQuotSuccInclusion P i).range
-- Mathlib.CategoryTheory.Monoidal.Linear
CategoryTheory.MonoidalLinear.whiskerLeft_smul : ∀ {R : Type u_1} {inst : Semiring R} {C : Type u_2} {inst_1 : CategoryTheory.Category.{v_1, u_2} C}
  {inst_2 : CategoryTheory.Preadditive C} {inst_3 : CategoryTheory.Linear R C}
  {inst_4 : CategoryTheory.MonoidalCategory C} {inst_5 : CategoryTheory.MonoidalPreadditive C}
  [self : CategoryTheory.MonoidalLinear R C] (X : C) {Y Z : C} (r : R) (f : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (r • f) =
    r • CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f
-- Mathlib.CategoryTheory.Category.ULift
/-- The functorial version of `ULift.up`.  -/
CategoryTheory.ULift.upFunctor : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (ULift.{u₂, u₁} C)
-- Mathlib.Order.Filter.Defs
/-- `filter_upwards [h₁, ⋯, hₙ]` replaces a goal of the form `s ∈ f` and terms
`h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f` with `∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s`.
The list is an optional parameter, `[]` being its default value.

`filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ` is a short form for
`{ filter_upwards [h₁, ⋯, hₙ], intro a₁ a₂ ⋯ aₖ }`.

`filter_upwards [h₁, ⋯, hₙ] using e` is a short form for
`{ filter_upwards [h1, ⋯, hn], exact e }`.

Combining both shortcuts is done by writing `filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e`.
Note that in this case, the `aᵢ` terms can be used in `e`.
 -/
Mathlib.Tactic.filterUpwards : Lean.ParserDescr
-- Mathlib.Data.EReal.Operations
EReal.sub_le_iff_le_add : ∀ {a b c : EReal}, b ≠ ⊥ ∨ c ≠ ⊤ → b ≠ ⊤ ∨ c ≠ ⊥ → (a - b ≤ c ↔ a ≤ c + b)
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An inequality of subobjects is witnessed by some morphism between the corresponding objects.  -/
CategoryTheory.Subobject.ofMkLE : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B A : C} →
      (f : A ⟶ B) →
        [inst_1 : CategoryTheory.Mono f] →
          (X : CategoryTheory.Subobject B) →
            CategoryTheory.Subobject.mk f ≤ X → (A ⟶ CategoryTheory.Subobject.underlying.obj X)
-- Mathlib.Topology.Connected.TotallyDisconnected
instTotallyDisconnectedSpaceMultiplicative : ∀ {α : Type u} [inst : TopologicalSpace α] [TotallyDisconnectedSpace α], TotallyDisconnectedSpace (Multiplicative α)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Module.Finite.addMonoidHom : ∀ (M : Type v) (N : Type w) [inst : AddCommGroup M] [Module.Finite ℤ M] [Module.Free ℤ M] [inst_3 : AddCommGroup N]
  [Module.Finite ℤ N], Module.Finite ℤ (M →+ N)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.const_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q] (q : Q),
  (ContinuousAffineMap.const R P q).contLinear = 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder c = Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder c_1) =
    (c = c_1)
-- Lean.CoreM
/-- If set, used to cancel elaboration from outside when results are not needed anymore.  -/
Lean.Core.Context.cancelTk? : Lean.Core.Context → Option IO.CancelToken
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_inter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Mathlib.Order.Category.HeytAlg
HeytAlg.ext_iff : ∀ {X Y : HeytAlg} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Analysis.Convex.Hull
convexHull_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (s : Set E), (convexHull 𝕜) (-s) = -(convexHull 𝕜) s
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).i =
    CategoryTheory.Limits.Fork.ι kf
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.dropPrefix?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (list : List α) (h_1 : (list : List α) → motive list [])
  (h_2 : (head : α) → (tail : List α) → motive [] (head :: tail))
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match list, [] with
    | list, [] => h_1 list
    | [], head :: tail => h_2 head tail
    | a :: as, b :: bs => h_3 a as b bs) =
    h_1 list
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.mono' : ∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph},
  (∀ (v w : V), H.Adj v w → H'.Adj v w) → H.verts = H'.verts → H.Connected → H'.Connected
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_mul_gcd_of_dvd_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {m n k : α}, k ∣ m * n → k ∣ m * gcd k n
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (J : Type v) →
      (U : J → C) →
        (V : J × J → C) →
          (f : (i j : J) → V (i, j) ⟶ U i) →
            autoParam (∀ (i j : J), CategoryTheory.Mono (f i j)) CategoryTheory.GlueData.f_mono._autoParam →
              (f_hasPullback :
                  autoParam (∀ (i j k : J), CategoryTheory.Limits.HasPullback (f i j) (f i k))
                    CategoryTheory.GlueData.f_hasPullback._autoParam) →
                autoParam (∀ (i : J), CategoryTheory.IsIso (f i i)) CategoryTheory.GlueData.f_id._autoParam →
                  (t : (i j : J) → V (i, j) ⟶ V (j, i)) →
                    (∀ (i : J), t i i = CategoryTheory.CategoryStruct.id (V (i, i))) →
                      (t' :
                          (i j k : J) →
                            CategoryTheory.Limits.pullback (f i j) (f i k) ⟶
                              CategoryTheory.Limits.pullback (f j k) (f j i)) →
                        (∀ (i j k : J),
                            CategoryTheory.CategoryStruct.comp (t' i j k)
                                (CategoryTheory.Limits.pullback.snd (f j k) (f j i)) =
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f i j) (f i k))
                                (t i j)) →
                          (∀ (i j k : J),
                              CategoryTheory.CategoryStruct.comp (t' i j k)
                                  (CategoryTheory.CategoryStruct.comp (t' j k i) (t' k i j)) =
                                CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f i j) (f i k))) →
                            CategoryTheory.GlueData C
-- Lean.Parser.Basic
/-- Gives the "unterminated raw string literal" error.
 -/
_private.Lean.Parser.Basic.0.Lean.Parser.rawStrLitFnAux.errorUnterminated : String.Pos.Raw → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Order.Filter.Pointwise
Filter.div_le_div_right : ∀ {α : Type u_2} [inst : Div α] {f₁ f₂ g : Filter α}, f₁ ≤ f₂ → f₁ / g ≤ f₂ / g
-- Mathlib.Algebra.Ring.Equiv
/-- This is `Equiv.piOptionEquivProd` as a `RingEquiv`.  -/
RingEquiv.piOptionEquivProd : {ι : Type u_7} →
  {R : Option ι → Type u_8} →
    [inst : (i : Option ι) → NonUnitalNonAssocSemiring (R i)] →
      ((i : Option ι) → R i) ≃+* R none × ((i : ι) → R (some i))
-- Mathlib.Combinatorics.Derangements.Finite
instDecidablePredPermMemSetDerangements : {α : Type u_1} → [DecidableEq α] → [Fintype α] → DecidablePred fun x => x ∈ derangements α
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.range_inclusion : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p q : Submodule R M) (h : p ≤ q), (Submodule.inclusion h).range = Submodule.comap q.subtype p
-- Init.Core
instSubsingleton : ∀ (p : Prop), Subsingleton p
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsRightQuasiInverse.equiv : ∀ {K : Type u_1} {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₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃},
  u.IsRightQuasiInverse v → v ∘ₗ u ≈ LinearMap.id
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.tensorProd_map_right : ∀ (R S : CommRingCat) [inst : Algebra ↑R ↑S] {X Y : CategoryTheory.Under R} (f : X ⟶ Y),
  ((R.tensorProd S).map f).right =
    CommRingCat.ofHom ↑(Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom f))
-- Mathlib.NumberTheory.Niven
/-- `sin(q * π)` for `q : ℚ` is algebraic over `ℤ`, using the complex `sin` function.  -/
Complex.isAlgebraic_sin_rat_mul_pi : ∀ (q : ℚ), IsAlgebraic ℤ (Complex.sin (↑q * ↑Real.pi))
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite' : ∀ {α : Sort u_1} (c0 c1 : Bool) {a b : α}, (bif c0 then a else bif c1 then a else b) = bif !c0 && !c1 then b else a
-- Mathlib.Order.InitialSeg
InitialSeg.transPrincipal_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [inst : IsWellOrder β s] [inst_1 : IsTrans γ t] (f : InitialSeg r s) (g : PrincipalSeg s t) (a : α),
  (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.piCongrRight_symm : ∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [inst : (j : η) → Mul (Ms j)]
  [inst_1 : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j),
  (MulEquiv.piCongrRight es).symm = MulEquiv.piCongrRight fun i => (es i).symm
-- Mathlib.Algebra.Lie.Ideal
LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L)
  {K' : LieSubalgebra R L} (h : K ≤ K'),
  (∃ I, LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- real numbers `0 < rIn < rOut`  -/
ContDiffBump.rOut : {E : Type u_1} → {c : E} → ContDiffBump c → ℝ
-- Mathlib.Topology.Algebra.Module.Complement
/-- An arbitrary choice of topological complement of a topologically complemented submodule.  -/
Submodule.ClosedComplemented.complement : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → {p : Submodule R M} → p.ClosedComplemented → Submodule R M
-- Mathlib.Topology.Algebra.InfiniteSum.Module
ContinuousLinearEquiv.summable : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂} {σ' : R₂ →+* R}
  [inst_8 : RingHomInvPair σ σ'] [inst_9 : RingHomInvPair σ' σ] {L : SummationFilter ι} {f : ι → M} (e : M ≃SL[σ] M₂),
  Summable (fun b => e (f b)) L ↔ Summable f L
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.of_forall_contains_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [LawfulBEq α],
  m₁.WF → m₂.WF → (∀ (k : α), m₁.contains k = m₂.contains k) → m₁.Equiv m₂
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.casesOn_zero : ∀ {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (zero : motive 0)
  (of_add : (x : α) → (xs : FreeAddMonoid α) → motive (FreeAddMonoid.of x + xs)),
  FreeAddMonoid.casesOn 0 zero of_add = zero
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coeFnRingHom_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Semiring β]
  [inst_3 : IsTopologicalSemiring β] (f : C(α, β)) (a : α), ContinuousMap.coeFnRingHom f a = f a
-- Std.Sync.Broadcast
/-- Current number of messages stored in the circular buffer.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.size : {α : Type} → Std.Bounded.State✝ α → ℕ
-- Mathlib.Control.EquivFunctor
EquivFunctor.mapEquiv_apply : ∀ (f : Type u₀ → Type u₁) [inst : EquivFunctor f] {α β : Type u₀} (e : α ≃ β) (x : f α),
  (EquivFunctor.mapEquiv f e) x = EquivFunctor.map e x
-- Mathlib.Data.Num.Lemmas
PosNum.testBit.eq_5 : ∀ (a : PosNum), a.bit1.testBit 0 = true
-- Mathlib.CategoryTheory.Category.Basic
/-- A morphism `f` is an epimorphism if it can be cancelled when precomposed.  -/
CategoryTheory.Epi.left_cancellation : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.Epi f] {Z : C}
  (g h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h → g = h
-- Init.Data.Vector.Find
Vector.findFinIdx?_subtype : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Vector.findFinIdx? f xs = Vector.findFinIdx? g xs.unattach
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.startsWith_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.toSlice.startsWith pat = s.startsWith pat
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution_zero : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F}
  [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F] [inst_9 : AddGroup G],
  MeasureTheory.convolution f 0 L μ = 0
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLEMk.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (h : X ≤ CategoryTheory.Subobject.mk f),
  X.ofLEMk f h =
    CategoryTheory.CategoryStruct.comp (X.ofLE (CategoryTheory.Subobject.mk f) h)
      (CategoryTheory.Subobject.underlyingIso f).hom
-- Init.Data.String.Basic
String.Slice.Pos.ofSlice_le_ofSlice_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {q r : (s.slice p₀ p₁ h).Pos},
  String.Slice.Pos.ofSlice q ≤ String.Slice.Pos.ofSlice r ↔ q ≤ r
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.fun_neg : ∀ {G : Type u_2} {α : Type u_3} [inst : Neg G] [inst_1 : MeasurableSpace G] [MeasurableNeg G] {m : MeasurableSpace α}
  {f : α → G}, Measurable f → Measurable fun i => -f i