mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_zero_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, orderOf x = 0 ↔ ¬IsOfFinOrder x
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.WF.singleton : ∀ {α : Type u_1} {a : α} {le : α → α → Bool},
  Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.singleton a)
-- Mathlib.CategoryTheory.Category.RelCat
/-- The morphisms in the relation category are relations.  -/
CategoryTheory.RelCat.Hom : CategoryTheory.RelCat → CategoryTheory.RelCat → Type u
-- Init.Data.BitVec.Lemmas
BitVec.or_append : ∀ {w v : ℕ} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v}, x₁ ++ y₁ ||| x₂ ++ y₂ = (x₁ ||| x₂) ++ (y₁ ||| y₂)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.mono : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l l' : Filter α}, Asymptotics.IsBigOWith c l' f g → l ≤ l' → Asymptotics.IsBigOWith c l f g
-- Mathlib.Order.RelIso.Basic
RelHom.coeFn_mk : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β)
  (h : ∀ {a b : α}, r a b → s (f a) (f b)), ⇑{ toFun := f, map_rel' := h } = f
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ResultingUniverseResult.mk.injEq : ∀ (u : Lean.Level) (assign? : Option (Lean.LMVarId × Lean.Level)) (u_1 : Lean.Level)
  (assign?_1 : Option (Lean.LMVarId × Lean.Level)),
  ({ u := u, assign? := assign? } = { u := u_1, assign? := assign?_1 }) = (u = u_1 ∧ assign? = assign?_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ext_getKey?_unit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m₁ m₂ : Std.ExtDHashMap α fun x => Unit}, (∀ (k : α), m₁.getKey? k = m₂.getKey? k) → m₁ = m₂
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_getConstant : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {assign : α → Bool} {ref : aig.Ref}
  {b : Bool}, aig.getConstant ref = some b → ⟦assign, { aig := aig, ref := ref }⟧ = b
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- Given `M : SheafOfModules R` and `X : D`, this is the restriction of `M`
over the sheaf of rings `R.over X` on the category `Over X`.  -/
SheafOfModules.over : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      {R : CategoryTheory.Sheaf K RingCat} → SheafOfModules R → (X : D) → SheafOfModules (R.over X)
-- Mathlib.Order.Grade
/-- The grading function.  -/
GradeOrder.grade : {𝕆 : Type u_5} → {α : Type u_6} → {inst : Preorder 𝕆} → {inst_1 : Preorder α} → [self : GradeOrder 𝕆 α] → α → 𝕆
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.associator_hom_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y Z : CategoryTheory.Center C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.f =
    (CategoryTheory.MonoidalCategoryStruct.associator X.fst Y.fst Z.fst).hom
-- Lean.Elab.DefView
Lean.Elab.DefViewElabHeaderData.mk.inj : ∀ {shortDeclName declName : Lean.Name} {levelNames : List Lean.Name} {binderIds : Array Lean.Syntax} {numParams : ℕ}
  {type : Lean.Expr} {shortDeclName_1 declName_1 : Lean.Name} {levelNames_1 : List Lean.Name}
  {binderIds_1 : Array Lean.Syntax} {numParams_1 : ℕ} {type_1 : Lean.Expr},
  { shortDeclName := shortDeclName, declName := declName, levelNames := levelNames, binderIds := binderIds,
        numParams := numParams, type := type } =
      { shortDeclName := shortDeclName_1, declName := declName_1, levelNames := levelNames_1, binderIds := binderIds_1,
        numParams := numParams_1, type := type_1 } →
    shortDeclName = shortDeclName_1 ∧
      declName = declName_1 ∧
        levelNames = levelNames_1 ∧ binderIds = binderIds_1 ∧ numParams = numParams_1 ∧ type = type_1
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
List.smul_prod' : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulDistribMulAction M N] {r : M}
  {l : List N}, r • l.prod = (List.map (fun x => r • x) l).prod
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_zero : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  ↑0 = 0
-- Mathlib.Data.Fintype.Card
Fintype.card_pempty : Fintype.card PEmpty.{u_4 + 1} = 0
-- Mathlib.Order.Filter.Bases.Basic
Filter.inf_neBot_iff_frequently_left : ∀ {α : Type u_1} {f g : Filter α}, (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x
-- Mathlib.Algebra.Ring.Commute
sq_ne_one_iff : ∀ {R : Type u} [inst : Ring R] {a : R} [NoZeroDivisors R], a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_isoIsPushout_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : CategoryTheory.IsPushout f g inl inr)
  (h' : CategoryTheory.IsPushout f g inl' inr'),
  CategoryTheory.CategoryStruct.comp inr (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom = inr'
-- Mathlib.CategoryTheory.Limits.ColimitLimit
/-- Since `colimit_limit_to_limit_colimit` is a morphism from a colimit to a limit,
this lemma characterises it.
 -/
CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (j : J)
  (k : K),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F)
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k)
        j)
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k)
-- Mathlib.Algebra.Squarefree.Basic
exists_squarefree_dvd_pow_of_ne_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R},
  x ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
/-- The Radon-Nikodym derivative `∂(μ.map g)/∂(ν.map g)` of the pushforward of measures by
a function `g : 𝓧 → 𝓨` evaluated at `g x` is a.e.-equal to the conditional expectation of `∂μ/∂ν`
with respect to the comap by `g` of the sigma-algebra on `𝓨`.

See `toReal_rnDeriv_map` for the same statement, but with a.e. equality with respect to
the measure `ν`.  -/
MeasureTheory.toReal_rnDeriv_map_ae_eq_trim : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ],
  μ.AbsolutelyContinuous ν →
    ∀ {g : 𝓧 → 𝓨} (hg : Measurable g) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g ν)],
      (fun a => ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g a)).toReal) =ᵐ[ν.trim ⋯]
        ν[fun a => (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
-- Lean.Compiler.NoncomputableAttr
Lean.noncomputableExt : Lean.TagDeclarationExtension
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBy_iff_mem_ker_lsmul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Module.IsTorsionBy R M a ↔ a ∈ (LinearMap.lsmul R M).ker
-- Init.Data.Int.DivMod.Lemmas
Int.neg_mul_emod_left : ∀ (a b : ℤ), -(a * b) % b = 0
-- Std.Time.Date.Unit.Basic
/-- Convert `Week.Offset` into `Day.Offset`.
 -/
Std.Time.Day.Offset.ofWeeks : Std.Time.Week.Offset → Std.Time.Day.Offset
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBoundP?_exists : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut], (∃ x, t.lowerBoundP? cut = some x) ↔ ∃ x ∈ t, cut x ≠ Ordering.lt
-- Mathlib.Dynamics.Ergodic.Ergodic
MeasureTheory.MeasurePreserving.preErgodic_conjugate_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {β : Type u_2}
  {m' : MeasurableSpace β} {μ' : MeasureTheory.Measure β} {e : α ≃ᵐ β},
  MeasureTheory.MeasurePreserving (⇑e) μ μ' → (PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ)
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.liftExtend.comm : ∀ {ι : 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 : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L),
  e.HasLift φ →
    ∀ (i' j' : ι'),
      CategoryTheory.CategoryStruct.comp (ComplexShape.Embedding.liftExtend.f φ i') ((L.extend e).d i' j') =
        CategoryTheory.CategoryStruct.comp (K.d i' j') (ComplexShape.Embedding.liftExtend.f φ j')
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ ^ 2 ^ k - 1` in a `2 ^ (k + 1)`-th cyclotomic extension of `ℚ`
is `(-2) ^ 2 ^ k`.  -/
IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two : ∀ {k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : CharZero K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K]
  (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))), (Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
-- Mathlib.Order.SuccPred.Basic
Order.Ici_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] (a : α),
  Set.Ici (Order.pred a) = insert (Order.pred a) (Set.Ici a)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
instFactPrimeValNat : ∀ (p : Nat.Primes), Fact (Nat.Prime ↑p)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
_private.Mathlib.Analysis.InnerProductSpace.TwoDim.0.Orientation.termω_1 : Lean.ParserDescr
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.upperBound?.eq_def : ∀ {α : Type u_1} (cut : α → Ordering) (x : RBTree.RBNode α) (x_1 : Option α),
  RBTree.RBNode.upperBound? cut x x_1 =
    match x, x_1 with
    | RBTree.RBNode.nil, ub => ub
    | RBTree.RBNode.node c a y b, ub =>
      match cut y with
      | Ordering.lt => RBTree.RBNode.upperBound? cut a (some y)
      | Ordering.gt => RBTree.RBNode.upperBound? cut b ub
      | Ordering.eq => some y
-- Mathlib.Algebra.Ring.CentroidHom
/-- Turn a centroid homomorphism into an additive monoid endomorphism.  -/
CentroidHom.toEnd : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → CentroidHom α → AddMonoid.End α
-- Mathlib.Order.Filter.Finite
Filter.mem_iInf_finite' : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} (s : Set α), s ∈ iInf f ↔ ∃ t, s ∈ ⨅ i ∈ t, f i.down
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.codeSuggestionsUnsafe : Lean.Elab.TermElabM (Array (Lean.StrLit → Lean.Doc.DocM (Array Lean.Doc.CodeSuggestion)))
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.desc.congr_simp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F] {X : C}
  (f f_1 : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X) (e_f : f = f_1)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)),
  CategoryTheory.Limits.coend.desc f hf = CategoryTheory.Limits.coend.desc f_1 ⋯
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.pullback.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  {S : CategoryTheory.Sieve X} (f f_1 : Y ⟶ X) (e_f : f = f_1)
  (x x_1 : CategoryTheory.Presieve.FamilyOfElements P S.arrows),
  x = x_1 →
    ∀ ⦃Y_1 : C⦄ (f_2 f_3 : Y_1 ⟶ Y) (e_f_1 : f_2 = f_3) (a : (CategoryTheory.Sieve.pullback f S).arrows f_2),
      CategoryTheory.Presieve.FamilyOfElements.pullback f x f_2 a =
        CategoryTheory.Presieve.FamilyOfElements.pullback f_1 x_1 f_3 ⋯
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.ext_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M N : Matrix m n α}, (∀ (i : m) (j : n), M i j = N i j) ↔ M = N
-- Init.Data.UInt.Lemmas
UInt32.ofNat_toNat : ∀ {x : UInt32}, UInt32.ofNat x.toNat = x
-- Mathlib.Analysis.Complex.Circle
Circle.coe_eq_one : ∀ {x : Circle}, ↑x = 1 ↔ x = 1
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.embedding_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (f : X ⟶ Y) (x : { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x => X }.ι)
  (x_1 : { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x => Y }.ι),
  (CategoryTheory.Mat_.embedding C).map f x x_1 = f
-- Std.Http.Protocol.H1.Reader
/-- Set when no further input bytes will arrive (the remote end has closed the connection).
 -/
Std.Http.Protocol.H1.Reader.noMoreInput : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Bool
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_addSubgroupOf_iff_le_normalizer_inf : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  (H.addSubgroupOf K).Normal ↔ K ≤ AddSubgroup.normalizer ↑(H ⊓ K)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_X_pow_add_C : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, 0 < n → ∀ {r : R}, (Polynomial.X ^ n + Polynomial.C r).leadingCoeff = 1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation on `K` extends the `v`-adic valuation on `R`.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑r = v.intValuation r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_modify_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {fallback : β k} {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).getD k fallback = (Option.map f (t.get? k)).getD fallback
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- Use `Algebra.QuasiFiniteAt.baseChange` instead for `Algebra.QuasiFiniteAt R p`.  -/
Algebra.WeaklyQuasiFiniteAt.baseChange : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S)
  [inst_3 : p.IsPrime] [Algebra.WeaklyQuasiFiniteAt R p] {A : Type u_4} [inst_5 : CommRing A] [inst_6 : Algebra R A]
  (q : Ideal (TensorProduct R A S)) [inst_7 : q.IsPrime],
  p = Ideal.comap Algebra.TensorProduct.includeRight.toRingHom q → Algebra.WeaklyQuasiFiniteAt A q
-- Mathlib.GroupTheory.Congruence.Basic
/-- An additive equivalence `e : α ≃+ β` generates an equivalence between quotient spaces,
if it is compatible with the relations.  -/
AddCon.congr : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] →
      [inst_1 : Add N] →
        {c : AddCon M} → {d : AddCon N} → (e : M ≃+ N) → c = AddCon.comap ⇑e ⋯ d → c.Quotient ≃+ d.Quotient
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.coneOfHasLimitEval_pt_d : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))] (n m : ι),
  (HomologicalComplex.coneOfHasLimitEval F).pt.d n m =
    CategoryTheory.Limits.limMap { app := fun j => (F.obj j).d n m, naturality := ⋯ }
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Given a scalar `r` and a vector measure `v`, `smul r v` is the vector measure corresponding to
the set function `s : Set α => r • (v s)`.  -/
MeasureTheory.VectorMeasure.smul : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          {R : Type u_4} →
            [inst_2 : Semiring R] →
              [inst_3 : DistribMulAction R M] →
                [ContinuousConstSMul R M] → R → MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α M
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The homotopy equivalence of complexes of `k`-modules between the standard resolution of `k` as
a trivial `G`-representation, and the complex which is `k` at 0 and 0 everywhere else, acts as
`∑ nᵢgᵢ ↦ ∑ nᵢ : k[G¹] → k` at 0.  -/
Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  (Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 =
    (CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k)).map (Rep.standardComplex.ε k G)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.bijective : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N), Function.Bijective ⇑e
-- Mathlib.Topology.Basic
IsClosed.inter : ∀ {X : Type u} {s₁ s₂ : Set X} [inst : TopologicalSpace X], IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∩ s₂)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Kernel.Environment.mk.inj : ∀ {constants : Lean.ConstMap} {quotInit : Bool} {diagnostics : Lean.Kernel.Diagnostics}
  {const2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx} {extensions irBaseExts : Array Lean.EnvExtensionState}
  {header : Lean.EnvironmentHeader} {constants_1 : Lean.ConstMap} {quotInit_1 : Bool}
  {diagnostics_1 : Lean.Kernel.Diagnostics} {const2ModIdx_1 : Std.HashMap Lean.Name Lean.ModuleIdx}
  {extensions_1 irBaseExts_1 : Array Lean.EnvExtensionState} {header_1 : Lean.EnvironmentHeader},
  { constants := constants, quotInit := quotInit, diagnostics := diagnostics, const2ModIdx := const2ModIdx,
        extensions := extensions, irBaseExts := irBaseExts, header := header } =
      { constants := constants_1, quotInit := quotInit_1, diagnostics := diagnostics_1, const2ModIdx := const2ModIdx_1,
        extensions := extensions_1, irBaseExts := irBaseExts_1, header := header_1 } →
    constants = constants_1 ∧
      quotInit = quotInit_1 ∧
        diagnostics = diagnostics_1 ∧
          const2ModIdx = const2ModIdx_1 ∧ extensions = extensions_1 ∧ irBaseExts = irBaseExts_1 ∧ header = header_1
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.Pair.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (gp : GenContFract.Pair α),
  GenContFract.Pair.map f gp = { a := f gp.a, b := f gp.b }
-- Mathlib.Computability.Language
Language.compl_compl : ∀ {α : Type u_1} (l : Language α), lᶜᶜ = l
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isNNRat_le_true : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb da db : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a na da →
    Mathlib.Meta.NormNum.IsNNRat b nb db → decide (na.mul db ≤ nb.mul da) = true → a ≤ b
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.surjective_projRestricts : ∀ {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i),
  Function.Surjective (Profinite.NobelingProof.ProjRestricts C h)
-- Mathlib.Algebra.Group.Ext
AddCommGroup.ext : ∀ {G : Type u_1} ⦃g₁ g₂ : AddCommGroup G⦄, HAdd.hAdd = HAdd.hAdd → g₁ = g₂
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Each column sum of a column stochastic matrix is 1.  -/
Matrix.sum_col_of_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.colStochastic R n → ∀ (i : n), ∑ j, M j i = 1
-- Mathlib.CategoryTheory.Monoidal.Rigid.Functor
/-- The left dual functor from `C` to `(Cᵒᵖ)ᴹᵒᵖ`.  -/
CategoryTheory.leftDualFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.LeftRigidCategory C] → CategoryTheory.Functor C Cᵒᵖᴹᵒᵖ
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- Left homotopies are compatible with postcomposition.  -/
HomotopicalAlgebra.Cylinder.LeftHomotopy.postcomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        {P : HomotopicalAlgebra.Cylinder X} →
          {f g : X ⟶ Y} →
            P.LeftHomotopy f g →
              {Z : C} →
                (p : Y ⟶ Z) →
                  P.LeftHomotopy (CategoryTheory.CategoryStruct.comp f p) (CategoryTheory.CategoryStruct.comp g p)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.algebraMap_mk' : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x),
  (algebraMap A B) (IsIntegralClosure.mk' A x hx) = x
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `A` restricts to a `G`-representation on
the kernel of the quotient map to the `S`-coinvariants `A_S`.  -/
Rep.toCoinvariantsKer : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] → [inst_1 : Group G] → Rep.{w, u, v} k G → (S : Subgroup G) → [S.Normal] → Rep.{w, u, v} k G
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_inv_eq_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, (fun x => x⁻¹) '' s = s⁻¹
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.toDescentData_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S) {M M' : ↑(F.obj { as := Opposite.op S })} (φ : M ⟶ M') (i : ι),
  ((F.toDescentData f).map φ).hom i = (F.map (f i).op.toLoc).toFunctor.map φ
-- Mathlib.Tactic.Tauto
Mathlib.Tactic.Tauto.DistribNotState.mk.inj : ∀ {fvars : List Lean.Expr} {currentGoal : Lean.MVarId} {fvars_1 : List Lean.Expr} {currentGoal_1 : Lean.MVarId},
  { fvars := fvars, currentGoal := currentGoal } = { fvars := fvars_1, currentGoal := currentGoal_1 } →
    fvars = fvars_1 ∧ currentGoal = currentGoal_1
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Left homotopy is closed under composition (on the left).  -/
CategoryTheory.Arrow.LeftHomotopy.compLeft : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v w : CategoryTheory.Arrow V} →
        {f g : v ⟶ w} →
          CategoryTheory.Arrow.LeftHomotopy f g →
            (e : u ⟶ v) →
              CategoryTheory.Arrow.LeftHomotopy (CategoryTheory.CategoryStruct.comp e f)
                (CategoryTheory.CategoryStruct.comp e g)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce.not : ∀ {α : Type u_1} [inst : DecidableEq α] {p : Prop} {L₁ L₂ L₃ : List (α × Bool)} {x : α} {b : Bool},
  FreeGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p