mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The ring equiv `R/I ≃+* S/J` induced by a ring equiv `f : R ≃+* S`, where `J = f(I)`.  -/
Ideal.quotientEquiv : {R : Type u} →
  [inst : Ring R] →
    {S : Type v} →
      [inst_1 : Ring S] →
        (I : Ideal R) →
          (J : Ideal S) →
            [inst_2 : I.IsTwoSided] → [inst_3 : J.IsTwoSided] → (f : R ≃+* S) → J = Ideal.map (↑f) I → R ⧸ I ≃+* S ⧸ J
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.sigmaIsoSigma_hom_ι : ∀ {ι : Type v} (α : ι → TopCat) (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι α i) (TopCat.sigmaIsoSigma α).hom =
    TopCat.sigmaι α i
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimitCoconeIsColimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat),
  GrpCat.FilteredColimits.colimitCoconeIsColimit F =
    CategoryTheory.Limits.isColimitOfReflects (CategoryTheory.forget₂ GrpCat MonCat)
      (MonCat.FilteredColimits.colimitCoconeIsColimit (F.comp (CategoryTheory.forget₂ GrpCat MonCat)))
-- Mathlib.Topology.Connected.PathConnected
/-- A path-connected set is connected.

(See `Counterexamples.TopologistsSineCurve` for the standard counterexample showing that the
converse is false.)  -/
IsPathConnected.isConnected : ∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X}, IsPathConnected F → IsConnected F
-- Mathlib.Algebra.Central.Basic
Algebra.IsCentral.mem_center_iff : ∀ (K : Type u) [inst : CommSemiring K] {D : Type v} [inst_1 : Semiring D] [inst_2 : Algebra K D]
  [h : Algebra.IsCentral K D] {x : D}, x ∈ Subalgebra.center K D ↔ ∃ a, x = (algebraMap K D) a
-- Mathlib.Tactic.GCongr.Core
/-- Structure recording the data for a "generalized congruence" (`gcongr`) lemma.  -/
Mathlib.Tactic.GCongr.GCongrLemma : Type
-- Init.Data.Int.Gcd
Int.gcd_eq_iff : ∀ {a b : ℤ} {g : ℕ}, a.gcd b = g ↔ ↑g ∣ a ∧ ↑g ∣ b ∧ ∀ (c : ℤ), c ∣ a → c ∣ b → c ∣ ↑g
-- Mathlib.Analysis.Calculus.Deriv.Comp
deriv.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {g₁ : 𝕜' → F},
  DifferentiableAt 𝕜' g₁ (h x) → DifferentiableAt 𝕜 h x → deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_X_index : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] {f : ℕ → R → S},
  f 1 0 = 0 → Polynomial.X.sum f = f 1 1
-- Lean.Declaration
Lean.Declaration.axiomDecl.injEq : ∀ (val val_1 : Lean.AxiomVal), (Lean.Declaration.axiomDecl val = Lean.Declaration.axiomDecl val_1) = (val = val_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.lt_rpow_inv_iff_of_pos : ∀ {z : ℝ} {y : NNReal}, 0 ≤ y → 0 < z → ∀ (x : NNReal), x < y ^ z⁻¹ ↔ x ^ z < y
-- Mathlib.Order.Hom.CompleteLattice
/-- The type of `⨆`-preserving functions from `α` to `β`.  -/
sSupHom : (α : Type u_8) → (β : Type u_9) → [SupSet α] → [SupSet β] → Type (max u_8 u_9)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatTrans_app_assoc : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF' LF : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) (X : C) {Z : H} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((LF'.leftDerivedNatTrans LF α' α W τ).app (L.obj X))
      (CategoryTheory.CategoryStruct.comp (α.app X) h) =
    CategoryTheory.CategoryStruct.comp (α'.app X) (CategoryTheory.CategoryStruct.comp (τ.app X) h)
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- A consequence of the special adjoint functor theorem: if `C` is cocomplete, well-copowered and
has a small separating set, then it is complete.  -/
CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C]
  [CategoryTheory.WellPowered.{v, v, u} Cᵒᵖ] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{v, v, u} P], P.IsSeparating → CategoryTheory.Limits.HasLimits C
-- Init.Data.Fin.Fold
Fin.foldl_congr : ∀ {α : Sort u_1} {n k : ℕ} (w : n = k) (f : α → Fin n → α), Fin.foldl n f = Fin.foldl k fun x i => f x (Fin.cast ⋯ i)
-- Mathlib.Analysis.Matrix.PosDef
/-- A positive semi-definite matrix `M` induces an inner product `⟪x, y⟫ = xᴴMy`.  -/
Matrix.toInnerProductSpace : {n : Type u_2} →
  {𝕜 : Type u_3} →
    [inst : Fintype n] → [inst_1 : RCLike 𝕜] → (M : Matrix n n 𝕜) → (hM : M.PosSemidef) → InnerProductSpace 𝕜 (n → 𝕜)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.exists_fin_pow_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [Finite α], f.SameCycle x y → ∃ i, (f ^ ↑i) x = y
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.mctxAfter : Lean.Elab.TacticInfo → Lean.MetavarContext
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.limitConePtAux.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}),
  ProfiniteAddGrp.limitConePtAux F =
    { carrier := {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (ProfiniteAddGrp.Hom.hom (F.map π)) (x i) = x j}, add_mem' := ⋯,
      zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.ΓObjEquivHom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type w)] [inst_2 : CategoryTheory.HasGlobalSectionsFunctor J (Type w)]
  (X : Type w) [inst_3 : Unique X] {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G)
  (x : (CategoryTheory.Sheaf.Γ J (Type w)).obj F),
  (CategoryTheory.Sheaf.ΓObjEquivHom J G X)
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Sheaf.Γ J (Type w)).map f)) x) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sheaf.ΓObjEquivHom J F X) x) f
-- Init.Data.Array.Basic
/-- Syntax for `Array α`. 

Conventions for notations in identifiers:

 * The recommended spelling of `#[]` in identifiers is `empty`.

 * The recommended spelling of `#[x]` in identifiers is `singleton`. -/
«term#[_,]» : Lean.ParserDescr
-- Mathlib.Computability.NFA
/-- The NFA's transition function  -/
NFA.step : {α : Type u} → {σ : Type v} → NFA α σ → σ → α → Set σ
-- Mathlib.Data.Finmap
Finmap.disjoint_union_right : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (x y z : Finmap β),
  x.Disjoint (y ∪ z) ↔ x.Disjoint y ∧ x.Disjoint z
-- Mathlib.Algebra.Homology.HomologySequence
/-- Given a short exact short complex `S : HomologicalComplex C c`, and degrees `i` and `j`
such that `c.Rel i j`, this is the snake diagram whose four lines are respectively
obtained by applying the functors `homologyFunctor C c i`, `opcyclesFunctor C c i`,
`cyclesFunctor C c j`, `homologyFunctor C c j` to `S`. Applying the snake lemma to this
gives the homology sequence of `S`.  -/
HomologicalComplex.HomologySequence.snakeInput : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            S.ShortExact → (i j : ι) → c.Rel i j → CategoryTheory.ShortComplex.SnakeInput C
-- Mathlib.Algebra.Order.Hom.TypeTags
/-- The additive version of a multiplicativized ordered additive monoid is
order-add-equivalent to itself.  -/
OrderAddMonoidIso.toAdditive_toMultiplicative : {G : Type u_1} → [inst : AddCommMonoid G] → [inst_1 : PartialOrder G] → Additive (Multiplicative G) ≃+o G
-- Mathlib.FieldTheory.Galois.Basic
/-- The map `K ↦ Gal(E/K)` is inclusion-reversing.  -/
IntermediateField.fixingSubgroup_le : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  {K1 K2 : IntermediateField F E}, K1 ≤ K2 → K2.fixingSubgroup ≤ K1.fixingSubgroup
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.fold : {α : Type u_1} → [inst : BEq α] → {σ : Type u_2} → (σ → α → σ) → σ → Aesop.UnorderedArraySet α → σ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the identity `Iso.refl f`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.id₂M' : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Init.Data.SInt.Lemmas
Int32.toISize_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int32.maxValue.toInt → (Int32.ofNat n).toISize = ISize.ofNat n
-- Mathlib.Topology.WithTopology
WithTopology.instInhabited : {X : Type u_1} → (t : TopologicalSpace X) → [Inhabited X] → Inhabited (WithTopology X t)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toList_ensureTermination_eq_match_step : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toList =
    match ↑it.step with
    | Std.IterStep.yield it' out => out :: it'.toList
    | Std.IterStep.skip it' => it'.toList
    | Std.IterStep.done => []
-- Mathlib.Algebra.Ring.BooleanRing
/-- The Boolean algebra structure on a Boolean ring.

The data is defined so that:
* `a ⊔ b` unfolds to `a + b + a * b`
* `a ⊓ b` unfolds to `a * b`
* `a ≤ b` unfolds to `a + b + a * b = b`
* `⊥` unfolds to `0`
* `⊤` unfolds to `1`
* `aᶜ` unfolds to `1 + a`
* `a \ b` unfolds to `a * (1 + b)`
 -/
BooleanRing.toBooleanAlgebra : {α : Type u_1} → [BooleanRing α] → BooleanAlgebra α
-- Lean.Elab.Term.TermElabM
/-- Store in the `InfoTree` that `e` is a "dot"-completion target. `stx` should cover the entire term.  -/
Lean.Elab.Term.addDotCompletionInfo : Lean.Syntax → Lean.Expr → Option Lean.Expr → Lean.Elab.TermElabM Unit
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.nil : Lean.Grind.Linarith.Poly
-- Mathlib.Analysis.InnerProductSpace.StarOrder
ContinuousLinearMap.instNonnegSpectrumClassRealId : ∀ {𝕜 : Type u_1} {H : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [CompleteSpace H] [inst_4 : Algebra ℝ (H →L[𝕜] H)] [IsScalarTower ℝ 𝕜 (H →L[𝕜] H)], NonnegSpectrumClass ℝ (H →L[𝕜] H)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.one_toLinearMap : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  AlgEquiv.toLinearMap 1 = 1
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ratio_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  Dilation.ratio e.symm = (Dilation.ratio e)⁻¹
-- Mathlib.Analysis.Normed.Group.Defs
/-- The distance function is induced by the norm.  -/
NormedAddGroup.dist_eq : ∀ {E : Type u_8} [self : NormedAddGroup E] (x y : E), dist x y = ‖-x + y‖
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j₁ j₂ : J}
  (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (k : J) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂),
  iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], m₁.contains k = false → (m₁.inter m₂).get! k = default
-- Mathlib.Order.Partition.Finpartition
/-- A setoid over a finite type induces a finpartition of the type's elements,
where the parts are the setoid's equivalence classes.  -/
Finpartition.ofSetSetoid : {α : Type u_1} → [inst : DecidableEq α] → (s : Setoid α) → (x : Finset α) → [DecidableRel ⇑s] → Finpartition x
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- Lift a ring hom to `WithVal`.  -/
WithVal.map : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : Ring R] →
        (v : Valuation R Γ₀) →
          {S : Type u_3} →
            [inst_2 : Ring S] →
              {Λ₀ : Type u_4} →
                [inst_3 : LinearOrderedCommGroupWithZero Λ₀] →
                  (w : Valuation S Λ₀) → (R →+* S) → WithVal v →+* WithVal w
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.jointly_surjective : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (x : t.pt),
  ∃ j y, (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) y = x
-- Mathlib.Algebra.Module.ULift
ULift.smulWithZero : {R : Type u} →
  {M : Type v} → [inst : Zero R] → [inst_1 : Zero M] → [SMulWithZero R M] → SMulWithZero (ULift.{u_1, u} R) M
-- Mathlib.Computability.RecursiveIn
ComputableIn.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {O : Set (ℕ →. ℕ)},
  ComputableIn O Prod.fst
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Raw.Const.getD_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ},
  t.WF →
    Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.filterMap f t) k fallback =
      ((Std.DTreeMap.Raw.Const.get? t k).bind (f k)).getD fallback
-- Mathlib.CategoryTheory.Sites.Whiskering
_private.Mathlib.CategoryTheory.Sites.Whiskering.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.splitter : {J : CategoryTheory.Limits.MulticospanShape} →
  (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3) →
    (j : CategoryTheory.Limits.WalkingMulticospan J) →
      ((i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i)) →
        ((i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)) → motive j
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.instStructure : {M : Type u_2} → [Zero M] → [One M] → [Add M] → FirstOrder.Language.presburger.Structure M
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero : ∀ {𝕜 : 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), (∀ᶠ (n : ℕ) in Filter.atTop, p n = 0) → p.radius = ⊤
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
/-- A finite measure obtained from an s-finite measure `μ`, such that
`μ = μ.toFinite.withDensity (μ.rnDeriv μ.toFinite)`
(see `MeasureTheory.Measure.withDensity_rnDeriv_eq` along with
`MeasureTheory.absolutelyContinuous_toFinite`). If `μ` is non-zero, then `μ.toFinite` is a
probability measure.  -/
MeasureTheory.Measure.toFinite : {α : Type u_1} →
  {mα : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [MeasureTheory.SFinite μ] → MeasureTheory.Measure α
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- When the representation on `A` is trivial, then `H₀(G, A)` is all of `A.`  -/
groupHomology.H0IsoOfIsTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → [A.IsTrivial] → groupHomology.H0 A ≅ ModuleCat.of k ↑A
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.union_compl : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), s ∪ sᶜ = Finset.univ
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Iterates over the whole iterator, applying the monadic effects of each step, discarding all
emitted values.

This function is deprecated. Instead of `it.allowNontermination.drain`, use `it.drain`.
 -/
Std.IterM.Partial.drain : {α : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM.Partial m β → [Std.IteratorLoop α m m] → m PUnit.{w + 1}
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimitInvAux_eq_of_rel : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat) (x y : (j : J) × ↑(F.obj j)),
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget GrpCat)) x y →
    GrpCat.FilteredColimits.colimitInvAux F x = GrpCat.FilteredColimits.colimitInvAux F y
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape_eq_of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {J' : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J']
  (e : J ≌ J'), W.colimitsOfShape J = W.colimitsOfShape J'
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a b = b - toIocDiv hp a b • p
-- Std.Do.WP.Sound
/-- Pure-proposition soundness: from a `MonadAttach.CanReturn` witness for `prog.run r` and a
`wp`-provable postcondition, conclude `P a`.
 -/
Std.Do.ReaderT.of_wp_run : ∀ {m : Type u → Type u_1} {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m ps]
  [Std.Do.WPSound m ps] [inst_4 : MonadAttach m] [LawfulMonadAttach m] {α ρ : Type u} {prog : ReaderT ρ m α} {r : ρ}
  {a : α} (P : α → Prop),
  MonadAttach.CanReturn (prog.run r) a → (⊢ₛ (Std.Do.wp prog).apply (Std.Do.PostCond.mayThrow fun a => ⌜P a⌝) r) → P a
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsRight.inf : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P₁ P₂ Q : CategoryTheory.MorphismProperty C)
  [P₁.RespectsRight Q] [P₂.RespectsRight Q], (P₁ ⊓ P₂).RespectsRight Q
-- Mathlib.Analysis.Normed.Module.Ray
/-- **Alias** of the forward direction of `sameRay_iff_inv_norm_smul_eq_of_ne`.

---

Two nonzero vectors `x y` in a real normed space are on the same ray if and only if the unit
vectors `‖x‖⁻¹ • x` and `‖y‖⁻¹ • y` are equal.  -/
SameRay.inv_norm_smul_eq : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
  x ≠ 0 → y ≠ 0 → SameRay ℝ x y → ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Alternative version of `List.sum_set` when the list is over a group  -/
List.sum_set' : ∀ {G : Type u_7} [inst : AddCommGroup G] (L : List G) (n : ℕ) (a : G),
  (L.set n a).sum = L.sum + if hn : n < L.length then -L[n] + a else 0
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isParabolic_conj'_iff : ∀ {R : Type u_1} [inst : CommRing R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R),
  ((↑g)⁻¹ * m * ↑g).IsParabolic ↔ m.IsParabolic
-- Mathlib.Analysis.Normed.Group.Hom
/-- The inclusion of `f.equalizer g` as a `NormedAddGroupHom`.  -/
NormedAddGroupHom.Equalizer.ι : {V : Type u_1} →
  {W : Type u_2} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : SeminormedAddCommGroup W] → (f g : NormedAddGroupHom V W) → NormedAddGroupHom (↥(f.equalizer g)) V
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.RightAdjointCommShift.iso'.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [inst_5 : F.CommShift A],
  CategoryTheory.Adjunction.RightAdjointCommShift.iso' adj a b h =
    (CategoryTheory.conjugateIsoEquiv (adj.comp (CategoryTheory.shiftEquiv' D b a h).toAdjunction)
          ((CategoryTheory.shiftEquiv' C b a h).toAdjunction.comp adj)).toFun
      (CategoryTheory.Functor.commShiftIso F b)
-- Mathlib.LinearAlgebra.Projection
Submodule.ker_projectionOnto : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), (p.projectionOnto q h).ker = q
-- Mathlib.Tactic.LinearCombination
Mathlib.Tactic.LinearCombination.Expanded.const.inj : ∀ {c c_1 : Lean.Term},
  Mathlib.Tactic.LinearCombination.Expanded.const c = Mathlib.Tactic.LinearCombination.Expanded.const c_1 → c = c_1
-- Init.Data.Fin.Lemmas
Fin.ofNat_self : ∀ {n : ℕ} [inst : NeZero n], Fin.ofNat n n = 0
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.one_div_pow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R} (n : ℕ), (1 / A) ^ n = 1 / A ^ n
-- Mathlib.Tactic.Widget.CommDiag
/-- Presenter for a commutative square  -/
Mathlib.Tactic.Widget.commutativeSquarePresenter : ProofWidgets.ExprPresenter
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The image of a measurable set under a monotone map is measurable.  -/
MeasurableSet.image_of_monotoneOn : ∀ {α : Type u_6} {β : Type u_7} {t : Set α} {g : α → β} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
  [BorelSpace α] [inst_3 : LinearOrder α] [OrderTopology α] [PolishSpace α] [inst : TopologicalSpace β]
  [inst_5 : MeasurableSpace β] [BorelSpace β] [inst_7 : LinearOrder β] [OrderTopology β] [SecondCountableTopology β],
  MeasurableSet t → MonotoneOn g t → MeasurableSet (g '' t)
-- Lean.Meta.Tactic.Intro
/-- Introduce one binder using `name` as the new hypothesis name.
 -/
Lean.MVarId.intro : Lean.MVarId → Lean.Name → Lean.MetaM (Lean.FVarId × Lean.MVarId)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Coevaluation of an exact pairing.  -/
CategoryTheory.ExactPairing.termη_ : Lean.ParserDescr
-- Init.Data.Option.Attach
Option.map_attachWith_eq_pmap : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {P : α → Prop} {H : ∀ (a : α), o = some a → P a} (f : { x // P x } → β),
  Option.map f (o.attachWith P H) = Option.pmap (fun a h => f ⟨a, ⋯⟩) o ⋯
-- Mathlib.Algebra.Opposites
MulOpposite.unop_bijective : ∀ {α : Type u_1}, Function.Bijective MulOpposite.unop
-- Mathlib.Data.List.Lex
List.LE' : {α : Type u} → [LinearOrder α] → LE (List α)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{max u u_1, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C),
  groupCohomology.mapShortComplexH1 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH1 (MonoidHom.id G) φ)
      (groupCohomology.mapShortComplexH1 (MonoidHom.id G) ψ)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.setOfPred_indep_eq : ∀ {α : Type u_1} (M : Matroid α), {I | M.Indep I} = ↑(lowerClosure {B | M.IsBase B})
-- Mathlib.Algebra.Notation
/-- The *negative part* of an element `a`.  -/
LeOnePart.leOnePart : {α : Type u_1} → [self : LeOnePart α] → α → α
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientQuotientEquivQuotientAux.eq_1 : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M),
  QuotientGroup.quotientQuotientEquivQuotientAux N M h =
    QuotientGroup.lift (Subgroup.map (QuotientGroup.mk' N) M) (QuotientGroup.map N M (MonoidHom.id G) h) ⋯