mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
/-- This is Lemma 2.5 (b) from [Geck](Geck2017).  -/
RootPairing.Base.root_add_root_mem_of_mem_of_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [CharZero R] [IsDomain R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [Finite ι] [P.IsCrystallographic] {b : P.Base} (i j k : ι),
  i ≠ j →
    i ∈ b.support →
      j ∈ b.support →
        P.root k + P.root i - P.root j ∈ Set.range ⇑P.root →
          P.root k ≠ -P.root i → P.root k - P.root j ∈ Set.range ⇑P.root → P.root k + P.root i ∈ Set.range ⇑P.root
-- Mathlib.Tactic.Algebraize
/-- A user attribute that is used to tag `RingHom` properties that can be converted to `Algebra`
properties. Using an (optional) parameter, it will also generate a `Name` of a declaration which
will help the `algebraize` tactic access the corresponding `Algebra` property.

There are two cases for what declaration corresponding to this `Name` can be.

1. An inductive type (i.e. the `Algebra` property itself), in this case it is assumed that the
   `RingHom` and the `Algebra` property are definitionally the same, and the tactic will construct
   the `Algebra` property by giving the `RingHom` property as a term.
2. A lemma (or constructor) proving the `Algebra` property from the `RingHom` property. In this case
   it is assumed that the `RingHom` property is the final argument, and that no other explicit
   argument is needed. The tactic then constructs the `Algebra` property by applying the lemma or
   constructor.

Finally, if no argument is provided to the `algebraize` attribute, it is assumed that the tagged
declaration has name `RingHom.Property` and that the corresponding `Algebra` property has name
`Algebra.Property`. The attribute then returns `Algebra.Property` (so assume case 1 above).  -/
Lean.Attr.algebraizeAttr : Lean.ParametricAttribute Lean.Name
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.AlternatingMap.postcomp_apply : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} (φ : M.AlternatingMap N n)
  {N' : ModuleCat R} (g : N ⟶ N') (x : Fin n → ↑M), (φ.postcomp g) x = (CategoryTheory.ConcreteCategory.hom g) (φ x)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Copy of a `CuspForm` with a new `toFun` equal to the old one, optionally transporting
along an equality of subgroups. Useful to fix definitional equalities.  -/
CuspForm.copy : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    {Γ' : Subgroup (GL (Fin 2) ℝ)} →
      (f : CuspForm Γ k) →
        (f' : UpperHalfPlane → ℂ) → f' = ⇑f → autoParam (Γ' = Γ) CuspForm.copy._auto_1 → CuspForm Γ' k
-- Batteries.Data.Random.MersenneTwister
/-- Middle word (`m`).  -/
Batteries.Random.MersenneTwister.Config.shiftSize : (self : Batteries.Random.MersenneTwister.Config) → Fin self.stateSize
-- Mathlib.Order.RelIso.Basic
acc_lift₂_iff : ∀ {α : Type u_1} {x : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂}
  {a : α}, Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_div : ∀ {α : Type u_2} [inst : Div α] (S : Set (Set α)) (t : Set α), ⋃₀ S / t = ⋃ s ∈ S, s / t
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β}, m.WF → (k ∈ m.alter k f ↔ (f m[k]?).isSome = true)
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- A centroid, over the image of an embedding, equals a centroid with
the same points and weights over the original `Finset`.  -/
Finset.centroid_map : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (p : ι → P),
  Finset.centroid k (Finset.map e s₂) p = Finset.centroid k s₂ (p ∘ ⇑e)
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_eq_on_Ico' : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (n : ℤ),
  ∀ a ∈ Set.Ico (↑n) (↑n + 1), ↑⌊a⌋ = ↑n
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]` (also called Jacobi identity).  -/
VectorField.leibniz_identity_mlieBracket_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (minSmoothness 𝕜 3) M]
  [CompleteSpace E] {U V W : (x : M) → TangentSpace I x} {x : M},
  ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x => ⟨x, U x⟩) x →
    ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x => ⟨x, V x⟩) x →
      ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x => ⟨x, W x⟩) x →
        VectorField.mlieBracket I U (VectorField.mlieBracket I V W) x =
          VectorField.mlieBracket I (VectorField.mlieBracket I U V) W x +
            VectorField.mlieBracket I V (VectorField.mlieBracket I U W) x
-- Mathlib.Order.Concept
Concept.instSemilatticeInf : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → SemilatticeInf (Concept α β r)
-- Init.Data.SInt.Lemmas
Int64.toInt_one : Int64.toInt 1 = 1
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.toJordanDecompositionEquiv_apply : ∀ (α : Type u_2) [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
  (MeasureTheory.SignedMeasure.toJordanDecompositionEquiv α) s = s.toJordanDecomposition
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] [inst_5 : Fact (1 ≤ p)], IsIsometricVAdd Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_eq_inertiaDeg : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [q.LiesOver p] [p.IsMaximal] [q.IsMaximal], p.inertiaDeg' q = q.inertiaDeg R
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.noncommPiCoprodEquiv.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] [inst_3 : DecidableEq ι],
  MonoidHom.noncommPiCoprodEquiv =
    { toFun := fun ϕ => MonoidHom.noncommPiCoprod ↑ϕ ⋯,
      invFun := fun f => ⟨fun i => f.comp (MonoidHom.mulSingle N i), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.mem_nonDegenerate_iff_mono : ∀ {n d : ℕ} (s : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })),
  s ∈ (SSet.stdSimplex.obj { len := n }).nonDegenerate d ↔ CategoryTheory.Mono (SSet.stdSimplex.objEquiv s)
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.comp_mul : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : MulOneClass M] [inst_1 : CommMonoid N] [inst_2 : CommMonoid P]
  (g : N →* P) (f₁ f₂ : M →* N), g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_polynomial : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (q : Polynomial R)
  (a : A), autoParam (p a) cfc_polynomial._auto_1 → cfc (fun x => Polynomial.eval x q) a = (Polynomial.aeval a) q
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_top : ∀ {G : Type u_1} [inst : Group G], ↑⊤ = Set.univ
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Show that there is a Galois insertion (generate, underlying presieve).  -/
CategoryTheory.Sieve.giGenerate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → GaloisInsertion CategoryTheory.Sieve.generate CategoryTheory.Sieve.arrows
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.le_ciSup_of_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] {a : α} {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → BddAbove (Set.range f) → ∀ (c : ι), a ≤ f c → a ≤ iSup f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.ins.eq_2 : ∀ {α : Type u_1} (x : RBTree.RBNode α) (parent : RBTree.RBNode.Path α) (y : α) (b : RBTree.RBNode α),
  (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b).ins x =
    parent.ins (RBTree.RBNode.node RBTree.RBColor.red x y b)
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.coe_mulLeft : ∀ {G : Type u_5} [inst : Group G] (a : G), ⇑(Equiv.mulLeft a) = fun x => a * x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.ordered_alter : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α}
  {f : Option β → Option β} (htb : t.Balanced),
  t.Ordered → (Std.DTreeMap.Internal.Impl.Const.alter a f t htb).impl.Ordered
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.hasRightExtension_iff_of_iso₂ : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (L : CategoryTheory.Functor C D) {F F' : CategoryTheory.Functor C H} (iso₂ : F ≅ F'),
  L.HasRightKanExtension F ↔ L.HasRightKanExtension F'
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.neg : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r → (-x).IsSt (-r)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_finset_coe : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (f : ι → M) (s : Finset ι), ∑ i, f ↑i = ∑ i ∈ s, f i
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `β` is an additive group, then any function from `α` to `β` extends uniquely to an
additive group homomorphism from the free additive group over `α` to `β`  -/
FreeAddGroup.lift : {α : Type u} → {β : Type v} → [inst : AddGroup β] → (α → β) ≃ (FreeAddGroup α →+ β)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iio_add_bij : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Set.BijOn (fun x => x + a) (Set.Iio b) (Set.Iio (b + a))
-- Std.Time.Duration
Std.Time.instDecidableEqDuration.decEq : (x x_1 : Std.Time.Duration) → Decidable (x = x_1)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubalgebra_strictMono : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  StrictMono IntermediateField.toSubalgebra
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_self_ofReal_re : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), ↑(RCLike.re (inner 𝕜 x x)) = inner 𝕜 x x
-- Mathlib.Topology.Algebra.Group.Basic
/-- A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the right, if
it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also
`DiscreteTopology`.)

If `G` is Hausdorff, this can be combined with `t2Space_of_properlyDiscontinuousSMul_of_t2Space`
to show that the quotient group `G ⧸ S` is Hausdorff.  -/
Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (S : Subgroup G),
  Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G) → ProperlyDiscontinuousSMul (↥S.op) G
-- Lean.Parser.Attr
Lean.Parser.Priority.numPrio.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Aesop.Forward.RuleInfo
Aesop.ForwardRuleInfo.mk : ℕ →
  ℕ →
    Array (Array Aesop.Slot) →
      Array Aesop.PremiseIndex → Option (Aesop.RulePattern × Aesop.PremiseIndex) → Aesop.ForwardRuleInfo
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_neg : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Neg β], MeasureTheory.stoppedProcess (-u) τ = -MeasureTheory.stoppedProcess u τ
-- Lean.Elab.PreDefinition.TerminationMeasure
_private.Lean.Elab.PreDefinition.TerminationMeasure.0.Lean.Elab.TerminationMeasure.delab.go : Lean.Elab.TerminationMeasure →
  ℕ →
    Lean.TSyntaxArray `ident →
      Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `Lean.Parser.Termination.terminationBy)
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.CSLift.mk : {α : Type u} → {β : outParam (Type u)} → (lift : α → β) → Function.Injective lift → Mathlib.Tactic.Ring.CSLift α β
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.cocyclesMap_comp : ∀ {k : Type u} {G H K : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] [inst_8 : Group K] [inst_9 : TopologicalSpace K] [inst_10 : IsTopologicalGroup K]
  {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y)
  (g : TopRep.res (↑ψ) Y ⟶ Z) (n : ℕ),
  ContinuousCohomology.cocyclesMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map f) g) n =
    CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cocyclesMap φ f n) (ContinuousCohomology.cocyclesMap ψ g n)
-- Mathlib.Logic.Equiv.Set
Equiv.ofLeftInverse_symm_apply : ∀ {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv : Nonempty α → β → α)
  (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) (b : ↑(Set.range f)),
  (Equiv.ofLeftInverse f f_inv hf).symm b = f_inv ⋯ ↑b
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_trans_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (f : M ≃ₗ[R] P)
  (g : N ≃ₗ[R] Q), LinearEquiv.rTensor N f ≪≫ₗ LinearEquiv.lTensor P g = TensorProduct.congr f g
-- Mathlib.RingTheory.PowerSeries.Catalan
PowerSeries.catalanSeries_constantCoeff : PowerSeries.constantCoeff PowerSeries.catalanSeries = 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.modify.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → ∀ (f f_1 : β → β), f = f_1 → t.modify a f = t_1.modify a_1 f_1
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofNatLT : ∀ {n : ℕ} (h : n < UInt8.size), (UInt8.ofNatLT n h).toUInt32 = UInt32.ofNatLT n ⋯
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (S : CategoryTheory.Sieve Y) {Z : C} (f : Z ⟶ Y.left),
  ((CategoryTheory.Sieve.overEquiv Y) S).arrows f ↔ S.arrows (CategoryTheory.Over.homMk f ⋯)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_prod_le : ∀ {R : Type u_7} {A : Type u_8} {B : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : SemilatticeSup B] [inst_4 : OrderBot B] [AddLeftMono B] [AddRightMono B]
  {D : A → B},
  D 0 = 0 →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      ∀ {ι : Type u_10} {s : Finset ι} {f : ι → AddMonoidAlgebra R A},
        AddMonoidAlgebra.supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, AddMonoidAlgebra.supDegree D (f i)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split.eq_1 : ONote.zero.split = (0, 0)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.Universal.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {d : M.Derivation φ}
  {desc : {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} → M'.Derivation φ → (M ⟶ M')}
  {fac :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation φ),
        d.postcomp (desc d') = d')
      PresheafOfModules.Derivation.Universal.fac._autoParam}
  {postcomp_injective :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (φ_1 φ' : M ⟶ M'),
        d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ')
      PresheafOfModules.Derivation.Universal.postcomp_injective._autoParam}
  {desc_1 : {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} → M'.Derivation φ → (M ⟶ M')}
  {fac_1 :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation φ),
        d.postcomp (desc_1 d') = d')
      PresheafOfModules.Derivation.Universal.fac._autoParam}
  {postcomp_injective_1 :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (φ_1 φ' : M ⟶ M'),
        d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ')
      PresheafOfModules.Derivation.Universal.postcomp_injective._autoParam},
  { desc := desc, fac := fac, postcomp_injective := postcomp_injective } =
      { desc := desc_1, fac := fac_1, postcomp_injective := postcomp_injective_1 } →
    desc = desc_1
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instReprCnstrRHS.repr : Lean.Meta.Grind.CnstrRHS → ℕ → Std.Format
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ↔ ∃ c, (a, b, c) ∈ t
-- Init.Data.Order.Classes
Std.LawfulOrderLeftLeaningMin.min_eq_right : ∀ {α : Type u} {inst : Min α} {inst_1 : LE α} [self : Std.LawfulOrderLeftLeaningMin α] (a b : α), ¬a ≤ b → a ⊓ b = b
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.ite : Lean.Meta.SplitKind
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 1 → G) → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).inv
      (CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 1) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.i
        (groupCohomology.cochainsIso₁ A).inv)
      h
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
/-- Universally closed satisfies fpqc descent.  -/
AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.UniversallyClosed)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_iSup_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {x : ι → Filter α} {y : ι → Filter β},
  (∀ (i : ι), Filter.Tendsto f (x i) (y i)) → Filter.Tendsto f (iSup x) (iSup y)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- The first projection of the weak pullback of `f` and `g`.  -/
CategoryTheory.Limits.weakPullback.fst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) → [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] → CategoryTheory.Limits.weakPullback f g ⟶ X
-- Mathlib.GroupTheory.Complement
/-- `S` and `T` are complements if `(+) : S × T → G` is a bijection

If `S` and `T` are `SetLike`s such as `AddSubgroup`s, see `isComplement_iff_bijective` for a
more ergonomic way to unfold.  -/
AddSubgroup.IsComplement : {G : Type u_1} → [AddGroup G] → Set G → Set G → Prop
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.not_isUnit_X_pow_sub_one : ∀ (R : Type u_1) [inst : Ring R] [Nontrivial R] (n : ℕ), ¬IsUnit (Polynomial.X ^ n - 1)
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
trdeg_add_le : ∀ {R : Type u_3} {S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Nontrivial R]
  {A : Type u} [inst_4 : CommRing A] [inst_5 : Algebra R A] [inst_6 : Algebra S A] [FaithfulSMul R S] [FaithfulSMul S A]
  [IsScalarTower R S A], Algebra.trdeg R S + Algebra.trdeg S A ≤ Algebra.trdeg R A
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict_precomp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K K' : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (α : K' ⟶ K) (ψ : K ⟶ L.extend e),
  e.homRestrict (CategoryTheory.CategoryStruct.comp α ψ) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap α e) (e.homRestrict ψ)
-- Mathlib.Data.Set.Image
Set.image_subset_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s ⊆ Set.range f
-- Mathlib.Combinatorics.Configuration
Configuration.instInhabitedDual : (P : Type u_1) → [h : Inhabited P] → Inhabited (Configuration.Dual P)
-- Mathlib.RingTheory.FreeRing
FreeRing.of_ne_one : ∀ {α : Type u} (x : α), FreeRing.of x ≠ 1
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.piBinderNames : Lean.Option Bool
-- Init.Omega.Int
Lean.Omega.Int.ofNat_mul_nonneg : ∀ {a b : ℕ}, 0 ≤ ↑a * ↑b
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.homCategory_comp_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : Bᵒᵖ) {X Y Z : a ⟶ b} (η : Bicategory.Opposite.Hom2 X Y)
  (θ : Bicategory.Opposite.Hom2 Y Z),
  (CategoryTheory.CategoryStruct.comp η θ).unop2 = CategoryTheory.CategoryStruct.comp η.unop2 θ.unop2
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div.sizeOf_spec : ∀ (k : ℤ) (y? : Option Int.Internal.Linear.Var) (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div k y? c) = 1 + sizeOf k + sizeOf y? + sizeOf c
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If `M` is finite, `finrank M = rank M`.  -/
Module.finrank_eq_rank : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M], ↑(Module.finrank R M) = Module.rank R M
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesMk₁_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥(groupHomology.cycles₁ A)),
  groupHomology.cyclesMk 1 0 groupHomology.cyclesMk₁_eq._proof_1
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₁ A).inv) ↑x) ⋯ =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₁ A).inv) x
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_single_one_mul`. -/
MonoidAlgebra.single_one_mul_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (x : MonoidAlgebra R M) (r : R) (m : M),
  (MonoidAlgebra.single 1 r * x).coeff m = r * x.coeff m