mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
/-- For a principal ideal `I`, `R ⧸ I ≃ₗ[R] I ^ n ⧸ I ^ (n + 1)`. To convert into a form
that uses the ideal of `R ⧸ I ^ (n + 1)`, compose with
`Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow`.  -/
Ideal.quotEquivPowQuotPowSucc : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDomain R] → {I : Ideal R} → Submodule.IsPrincipal I → I ≠ ⊥ → (n : ℕ) → (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.isPerfectMatching_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph}, M.IsPerfectMatching ↔ ∀ (v : V), ∃! w, M.Adj v w
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.congr_preservesColimitsOfShape : ∀ (J : Type u_1) (C : Type u_3) {K : Type u_5} {K' : Type u_6} [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_2, u_6} K'] [inst_2 : CategoryTheory.Category.{v_3, u_1} J]
  [inst_3 : CategoryTheory.Category.{v_5, u_3} C] (e : K ≌ K'),
  CategoryTheory.ObjectProperty.preservesColimitsOfShape K = CategoryTheory.ObjectProperty.preservesColimitsOfShape K'
-- Mathlib.Algebra.Order.Sub.Defs
le_tsub_add : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [OrderedSub α] {a b : α}, b ≤ b - a + a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_insert_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.insert k).size ≤ t.size + 1
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.one_sub_inv_inv : ∀ {a : ENNReal}, a ≤ 1 → (1 - a)⁻¹.HolderConjugate a⁻¹
-- Mathlib.Data.Finset.Union
Finset.biUnion_val : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (t : α → Finset β),
  (s.biUnion t).val = (s.val.bind fun a => (t a).val).dedup
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count_prod : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {ι : Type u_3}
  (s : Finset ι) (I : ι → FractionalIdeal (nonZeroDivisors R) K),
  (∀ i ∈ s, I i ≠ 0) → FractionalIdeal.count K v (∏ i ∈ s, I i) = ∑ i ∈ s, FractionalIdeal.count K v (I i)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.instQuasiCompactMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.QuasiCompact (f ∣_ V)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.top_eq_mk_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M},
  ⊤ = ArchimedeanClass.mk a ↔ a = 0
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β),
  (CompleteLatticeHom.id β).comp f = f
-- Lean.Elab.Term.TermElabM
/-- List of data to be able to localize universe level metavariable errors to particular expressions.  -/
Lean.Elab.Term.State.levelMVarErrorInfos : Lean.Elab.Term.State → List Lean.Elab.Term.LevelMVarErrorInfo
-- Init.Data.UInt.Bitwise
UInt64.ofFin_xor : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a ^^^ b) = UInt64.ofFin a ^^^ UInt64.ofFin b
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedCommAux_comp_gradedCommAux : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)],
  TensorProduct.gradedCommAux R 𝒜 ℬ ∘ₗ TensorProduct.gradedCommAux R ℬ 𝒜 = LinearMap.id
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z}
  (f f_1 : P.complex ⟶ Q.complex) (e_f : f = f_1) (n : ℕ) (g g_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) (e_g : g = g_1)
  (g' g'_1 : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) (e_g' : g' = g'_1)
  (w :
    f.f (n + 1) =
      CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g +
        CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))),
  CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc f n g g' w =
    CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc f_1 n g_1 g'_1 ⋯
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.divMod_spec : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {a b c : FractionalIdeal (nonZeroDivisors R) K},
  a ≤ c → a ≠ 0 → b ≠ 0 → a + FractionalIdeal.spanSingleton (nonZeroDivisors R) (c.divMod b a) * b = c
-- Mathlib.RingTheory.Jacobson.Ring
IsJacobsonRing.out' : ∀ {R : Type u_3} {inst : CommRing R} [self : IsJacobsonRing R] (I : Ideal R), I.IsRadical → I.jacobson = I
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X),
  CategoryTheory.Sieve.ofArrows Y f = CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows Y f)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.lit.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {value value_1 : Lean.Compiler.LCNF.LitValue},
  Lean.Compiler.LCNF.LetValue.lit value = Lean.Compiler.LCNF.LetValue.lit value_1 → value = value_1
-- Mathlib.Topology.FiberBundle.Basic
/-- The total space of the fiber bundle, as a convenience function for dot notation.
It is by definition equal to `Bundle.TotalSpace F Z.Fiber`.  -/
FiberBundleCore.TotalSpace : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → Type (max u_2 u_3)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : Sublattice α) (h_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier)
  (h_bot : ⊥ ∈ L.carrier), ↑{ toSublattice := L, compl_mem' := h_compl, bot_mem' := h_bot } = ↑L
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, m.contains k = true → m.getKey? k = some k
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.le_normalizer_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H ≤ AddSubgroup.normalizer ↑K ↔ ∀ h ∈ H, ∀ k ∈ K, h + k + -h ∈ K
-- Init.Data.UInt.Lemmas
USize.mul_def : ∀ (a b : USize), a * b = { toBitVec := a.toBitVec * b.toBitVec }
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.finrank_rootSpanIn : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (K : Type u_7)
  {L : Type u_8} [inst_2 : Field K] [inst_3 : Field L] [inst_4 : Algebra K L] [inst_5 : Module L M]
  [inst_6 : Module L N] [inst_7 : Module K M] [inst_8 : Module K N] [IsScalarTower K L M] [IsScalarTower K L N]
  (Q : RootPairing ι L M N) [Q.IsRootSystem] [Q.IsValuedIn K], Module.finrank K ↥(Q.rootSpan K) = Module.finrank L M
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.pointwise_smul_le_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Subsemiring R}, a • S ≤ a • T ↔ S ≤ T
-- Lean.Util.Trace
/-- Determine if tracing is available for a given class, checking ancestor classes if appropriate.  -/
Lean.isTracingEnabledFor : {m : Type → Type} → [Monad m] → [Lean.MonadTrace m] → [Lean.MonadOptions m] → Lean.Name → m Bool
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizerOfOrbitRel.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a b : α} (h : (MulAction.orbitRel G α) a b),
  MulAction.stabilizerEquivStabilizerOfOrbitRel h = (MulAction.stabilizerEquivStabilizer ⋯).symm
-- Mathlib.Algebra.Star.StarAlgHom
/-- The identity map is a star algebra isomorphism.  -/
StarAlgEquiv.refl : (R : Type u_2) →
  (A : Type u_3) → [inst : Add A] → [inst_1 : Mul A] → [inst_2 : SMul R A] → [inst_3 : Star A] → A ≃⋆ₐ[R] A
-- Mathlib.MeasureTheory.Group.FundamentalDomain
_private.Mathlib.MeasureTheory.Group.FundamentalDomain.0.MeasureTheory.termα_mod_G_1 : Lean.ParserDescr
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertMany_list_eq_foldl : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, t.insertMany l = List.foldl (fun acc p => acc.insert p.1 p.2) t l
-- Init.Data.String.Lemmas.Order
String.Pos.ofSlice_ne_startPos : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos},
  p ≠ (s.slice p₀ p₁ h).startPos → String.Pos.ofSlice p ≠ s.startPos
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The natural isomorphism witnessing the pseudo-unity constraint of `Grothendieck.map`.  -/
CategoryTheory.Pseudofunctor.Grothendieck.mapIdIso : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) →
      CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.id F) ≅
        CategoryTheory.Functor.id F.Grothendieck
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- If `f` is almost everywhere strongly measurable and its range is almost everywhere contained
in a nonempty measurable set `s`, then there is a strongly measurable representative `g` of `f`
whose range is contained in `s`.  -/
MeasureTheory.AEStronglyMeasurable.exists_stronglyMeasurable_range_subset : ∀ {α : Type u_5} {β : Type u_6} [inst : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  [mb : MeasurableSpace β] [BorelSpace β] [m : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {s : Set β},
      MeasurableSet s →
        s.Nonempty →
          (∀ᵐ (x : α) ∂μ, f x ∈ s) → ∃ g, MeasureTheory.StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᵐ[μ] g
-- Init.Omega.Constraint
Lean.Omega.instDecidableEqConstraint : DecidableEq Lean.Omega.Constraint
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F] (i : I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).hom
      (CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)) =
    CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovDist_comm : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω),
  MeasureTheory.levyProkhorovDist μ ν = MeasureTheory.levyProkhorovDist ν μ
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_ofNat_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoDiv hp (a - OfNat.ofNat m * p) b = toIcoDiv hp a b + OfNat.ofNat m
-- Mathlib.Data.Set.Defs
/-- Turn a predicate `p : α → Prop` into a set, also written as `{x | p x}`  -/
Set.ofPred : {α : Type u} → (α → Prop) → Set α
-- Mathlib.Algebra.Ring.Parity
odd_neg_one : ∀ {α : Type u_2} [inst : Ring α], Odd (-1)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_toLp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : α → E) (hf : MeasureTheory.MemLp f p μ),
  ‖MeasureTheory.MemLp.toLp f hf‖ = (MeasureTheory.eLpNorm f p μ).toReal
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_insert_zero : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set R), Subsemiring.closure (insert 0 s) = Subsemiring.closure s
-- Mathlib.Algebra.Polynomial.Basic
/-- Ring isomorphism between `R[X]` and `R[ℕ]`. This is just an
implementation detail, but it can be useful to transfer results from `Finsupp` to polynomials.  -/
Polynomial.toFinsuppIso : (R : Type u) → [inst : Semiring R] → Polynomial R ≃+* AddMonoidAlgebra R ℕ
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)}
  (h : μ.FiniteSpanningSetsIn C), IsCountablySpanning C
-- Lean.Elab.InfoTree.Types
Lean.Elab.OptionInfo.mk.injEq : ∀ (stx : Lean.Syntax) (optionName declName : Lean.Name) (stx_1 : Lean.Syntax) (optionName_1 declName_1 : Lean.Name),
  ({ stx := stx, optionName := optionName, declName := declName } =
      { stx := stx_1, optionName := optionName_1, declName := declName_1 }) =
    (stx = stx_1 ∧ optionName = optionName_1 ∧ declName = declName_1)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- **Alias** of `SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_of_one`.

---

The sum of the identity, the adjacency matrix, and its complement is the all-ones matrix.  -/
SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : DecidableEq α] [inst_3 : AddMonoid α] [inst_4 : One α],
  1 + SimpleGraph.adjMatrix α G + (SimpleGraph.adjMatrix α G).compl = Matrix.of 1
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.gluedIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : CategoryTheory.Limits.HasMulticoequalizer D.diagram]
  [inst_3 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F]
  [inst_4 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F],
  D.gluedIso F =
    CategoryTheory.preservesColimitIso F D.diagram.multispan ≪≫
      CategoryTheory.Limits.HasColimit.isoOfNatIso (D.diagramIso F)
-- Mathlib.Data.Num.ZNum
ZNum.zneg_bit1 : ∀ (n : ZNum), -n.bit1 = (-n).bitm1
-- Lean.Meta.Tactic.Subst
Lean.Meta.substVars : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Order.Hom.Units
OrderMonoidIso.val_inv_unitsCongr_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : Preorder β] [inst_3 : Monoid β]
  (e : α ≃*o β) (a : αˣ), ↑(e.unitsCongr a)⁻¹ = e ↑a⁻¹
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instPowInt : {α : Type u_1} → [One α] → [Pow α ℤ] → Pow (WithZero α) ℤ
-- Mathlib.Logic.Denumerable
/-- Any infinite set of naturals is denumerable.  -/
Nat.Subtype.denumerable : (s : Set ℕ) → [DecidablePred fun x => x ∈ s] → [Infinite ↑s] → Denumerable ↑s
-- Mathlib.Logic.Basic
Ne.ite_eq_right_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b : α}, a ≠ b → ((if P then a else b) = b ↔ ¬P)
-- Mathlib.Topology.Algebra.Monoid
/-- The continuous map `fun y => x * y`  -/
ContinuousMap.mulLeft : {X : Type u_5} → [inst : TopologicalSpace X] → [inst_1 : Mul X] → [SeparatelyContinuousMul X] → X → C(X, X)
-- Init.Data.List.Basic
List.Pairwise.below.nil : ∀ {α : Type u} {R : α → α → Prop} {motive : (a : List α) → List.Pairwise R a → Prop}, List.Pairwise.below ⋯
-- Mathlib.Data.Multiset.ZeroCons
Multiset.instLawfulSingleton : ∀ {α : Type u_1}, LawfulSingleton α (Multiset α)
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.normedGroup.eq_1 : ∀ {E : Type u_2} [inst : NormedGroup E],
  OrderDual.normedGroup =
    { toNorm := OrderDual.toNorm, toGroup := OrderDual.instGroup, toMetricSpace := instMetricSpaceOrderDual,
      dist_eq := ⋯ }
-- Std.Data.ExtHashSet.Basic
/-- Creates a hash set from a list of elements. Note that unlike repeatedly calling `insert`, if the
collection contains multiple elements that are equal (with regard to `==`), then the last element
in the collection will be present in the returned hash set.
 -/
Std.ExtHashSet.ofList : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → List α → Std.ExtHashSet α
-- Mathlib.LinearAlgebra.Projection
Submodule.quotientEquivOfIsCompl_comp_mkQ : ∀ {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.quotientEquivOfIsCompl q h) ∘ₗ p.mkQ = q.projectionOnto p ⋯
-- Mathlib.Order.SupClosed
infClosed_sInter : ∀ {α : Type u_3} [inst : SemilatticeInf α] {S : Set (Set α)}, (∀ s ∈ S, InfClosed s) → InfClosed (⋂₀ S)
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The equalizer in `CommRingCat` is the equalizer as sets. This is the equalizer fork.  -/
CommRingCat.equalizerFork : {A B : CommRingCat} → (f g : A ⟶ B) → CategoryTheory.Limits.Fork f g
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.isRegular_of_isLeftRegular_det : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] {A : Matrix n n α},
  IsLeftRegular A.det → IsRegular A
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle K L n) {K' : CochainComplex C ℤ}
  (g : K' ⟶ K),
  CochainComplex.HomComplex.Cocycle.equivHomShift.symm (z.precomp g) =
    CategoryTheory.CategoryStruct.comp g (CochainComplex.HomComplex.Cocycle.equivHomShift.symm z)
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `ExponentExists.isAddTorsion`.

---

If a group exponent exists, the additive group is torsion.  -/
ExponentExists.is_add_torsion : ∀ {G : Type u_1} [inst : AddGroup G], AddMonoid.ExponentExists G → IsAddTorsion G
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.natFactorial_mul_dp_eq : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
  (x : M), ↑n.factorial * DividedPowerAlgebra.dp R n x = DividedPowerAlgebra.dp R 1 x ^ n
-- Mathlib.CategoryTheory.Localization.Predicate
/-- there is a factorisation involving the lifted functor  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac : ∀ {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] {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E) (F : CategoryTheory.Functor C E)
  (hF : W.IsInvertedBy F), L.comp (self.lift F hF) = F
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is weakly between the other two, the oriented angle at the
third point (reversed) is zero.  -/
Wbtw.oangle₁₃₂_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₁ p₃ p₂ = 0
-- Mathlib.Data.FunLike.Equiv
EquivLike.injective_comp : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [inst : EquivLike E α β] (e : E) (f : β → γ),
  Function.Injective (f ∘ ⇑e) ↔ Function.Injective f
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The eigenspace is a subspace of the generalized eigenspace.  -/
Module.End.eigenspace_le_genEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, 0 < k → f.eigenspace μ ≤ (f.genEigenspace μ) ↑k
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfMkEqMk_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
  (h : CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g),
  (CategoryTheory.Subobject.isoOfMkEqMk f g h).hom = CategoryTheory.Subobject.ofMkLEMk f g ⋯
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Mul α} {inst_1 : Add α} {inst_2 : Mul β} {inst_3 : Add β} {inst_4 : LE α}
  {inst_5 : LE β} {toRingEquiv : α ≃+* β}
  {map_le_map_iff' : ∀ {a b : α}, toRingEquiv.toFun a ≤ toRingEquiv.toFun b ↔ a ≤ b} {toRingEquiv_1 : α ≃+* β}
  {map_le_map_iff'_1 : ∀ {a b : α}, toRingEquiv_1.toFun a ≤ toRingEquiv_1.toFun b ↔ a ≤ b},
  { toRingEquiv := toRingEquiv, map_le_map_iff' := map_le_map_iff' } =
      { toRingEquiv := toRingEquiv_1, map_le_map_iff' := map_le_map_iff'_1 } →
    toRingEquiv = toRingEquiv_1
-- Init.Prelude
instSMulOfMul : {α : Type u} → [Mul α] → SMul α α
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyClass.mk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  Function.Surjective HomotopicalAlgebra.LeftHomotopyClass.mk
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprodComparison_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprodComparison F A B) =
    F.map CategoryTheory.Limits.coprod.inr
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.opOpEquivalence_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.opOpEquivalence C).functor = CategoryTheory.unopUnop C
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabValueOf : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G),
  (P.conePointsIsoOfNatIso Q w).inv = CategoryTheory.Limits.IsLimit.map t P w.inv
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsCoseparator G ↔
    ∀ ⦃X Y : C⦄ (f g : X ⟶ Y),
      (∀ (h : Y ⟶ G), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) → f = g
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.integral_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] (f : α → ℝ) (g : α → E),
  ∫ (x : α), g x ∂μ.tilted f = ∫ (x : α), (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) • g x ∂μ
-- Init.Data.Order.FactoriesExtra
/-- Creates an `DecidableLE α` instance using a well-behaved `Ord α` instance.
 -/
DecidableLE.ofOrd : (α : Type u) → [inst : LE α] → [inst_1 : Ord α] → [Std.LawfulOrderOrd α] → DecidableLE α