mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- `Ext` commutes with binary biproducts on the second variable.  -/
CategoryTheory.Abelian.Ext.addEquivBiprod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y₁ Y₂ : C} →
          {n : ℕ} →
            CategoryTheory.Abelian.Ext X (Y₁ ⊞ Y₂) n ≃+
              CategoryTheory.Abelian.Ext X Y₁ n × CategoryTheory.Abelian.Ext X Y₂ n
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitAnchorRefInfo.numDigits : Lean.Meta.Grind.SplitAnchorRefInfo → ℕ
-- Mathlib.Algebra.Lie.Extension
/-- The 2-cocycle attached to an extension with a linear section.  -/
LieAlgebra.Extension.twoCocycleOf : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing M] →
              [inst_4 : LieAlgebra R M] →
                [inst_5 : IsLieAbelian M] →
                  (E : LieAlgebra.Extension R M L) →
                    {s : L →ₗ[R] E.L} →
                      Function.LeftInverse ⇑E.proj ⇑s →
                        have this := ⋯;
                        ↥(LieModule.Cohomology.twoCocycle R L M)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.con.eq_1 : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal],
  QuotientGroup.con N = { toSetoid := QuotientGroup.leftRel N, mul' := ⋯ }
-- Init.Data.List.TakeDrop
List.getElem?_take_of_lt : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, i < j → (List.take j l)[i]? = l[i]?
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.piEquivalenceFunctorDiscrete_inverse_obj : ∀ (J : Type u₂) (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) (j : J),
  (CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.obj F j = F.obj { as := j }
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_of_mem_tail : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α}, a ∈ s.tail → a ∈ s
-- Mathlib.MeasureTheory.Measure.Support
/-- Any compact set contained in the complement of the support has zero measure.  -/
MeasureTheory.Measure.measure_eq_zero_of_isCompact_subset_compl_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} {K : Set X},
  IsCompact K → K ⊆ μ.supportᶜ → μ K = 0
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.add.injEq : ∀ (a b a_1 b_1 : Nat.Internal.Linear.Expr), (a.add b = a_1.add b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.CategoryTheory.Galois.Basic
/-- `C` has a terminal object (G1).  -/
CategoryTheory.PreGaloisCategory.hasTerminal : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.PreGaloisCategory C],
  CategoryTheory.Limits.HasTerminal C
-- Mathlib.FieldTheory.Galois.Abelian
IsAbelianGalois.toIsGalois : ∀ {K : Type u_4} {L : Type u_5} {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L} [self : IsAbelianGalois K L],
  IsGalois K L
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.realSize.eq_def : ∀ {α : Type u_1} (x : Batteries.BinomialHeap.Imp.Heap α),
  x.realSize =
    match x with
    | Batteries.BinomialHeap.Imp.Heap.nil => 0
    | Batteries.BinomialHeap.Imp.Heap.cons rank val c s => c.realSize + 1 + s.realSize
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.reassocMax.maxArgs : Lean.Level → Array Lean.Level → Array Lean.Level
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.mem_darts_iff_fst_snd_infix_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {d : G.Dart},
  d ∈ p.darts ↔ [d.toProd.1, d.toProd.2] <:+: p.support
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.setBlack_idem : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.setBlack.setBlack = t.setBlack
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_inclusion : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H ≤ K) (a : ↥H), ↑((Subgroup.inclusion h) a) = ↑a
-- Mathlib.Analysis.Normed.Field.Lemmas
Filter.tendsto_inv₀_nhdsNE_zero : ∀ {α : Type u_1} [inst : NormedDivisionRing α], Filter.Tendsto Inv.inv (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueGroup.mk.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B) (r s : A)
  (hr : f r ≠ 0) (hs : f s ≠ 0),
  MonoidWithZeroHom.valueGroup.mk f r s hr hs = ⟨(Units.mk0 (f r) hr)⁻¹ * Units.mk0 (f s) hs, ⋯⟩
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_eq_Ioo_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc a b = Set.Ioo a b ↔ ¬a ≤ b
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_iff_exists_one_le_mul : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftMono α]
  [MulLeftReflectLE α], a ≤ b ↔ ∃ c, 1 ≤ c ∧ a * c = b
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Lift a `ZeroHom` to `Finset` via `image`  -/
Finset.imageZeroHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Zero α] →
        [DecidableEq β] →
          [inst_2 : Zero β] → [inst_3 : FunLike F α β] → [ZeroHomClass F α β] → F → ZeroHom (Finset α) (Finset β)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.ofHom_zero : ∀ {R : Type u} [inst : Ring R] {M N : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : AddCommGroup N]
  [inst_4 : Module R N], ModuleCat.ofHom 0 = 0
-- Mathlib.Data.Seq.Computation
Computation.terminates_map_iff : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Computation α), (Computation.map f s).Terminates ↔ s.Terminates
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_sub_ofNat : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  [inst_4 : Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) [inst_7 : n.AtLeastTwo],
  ⌈a - OfNat.ofNat n⌉₊ = ⌈a⌉₊ - OfNat.ofNat n
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  (i : Fin (1 + 1 + 1)),
  (G.mapComposableArrowsObjMk₂Iso f g).inv.app i =
    match i with
    | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj X)
    | ⟨i.succ, hi⟩ =>
      match ⟨i, ⋯⟩ with
      | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Y)
      | ⟨1, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Z)
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of the projection is smaller or equal to the norm of the original element.  -/
QuotientGroup.norm_mk_le_norm : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} {m : M}, ‖↑m‖ ≤ ‖m‖
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given two Localization maps `f : M →* N, k : M →* P` for a Submonoid `S ⊆ M`, the hom
from `P` to `N` induced by `f` is left inverse to the hom from `N` to `P` induced by `k`.  -/
Submonoid.LocalizationMap.lift_left_inverse : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} (z : N), (k.lift ⋯) ((f.lift ⋯) z) = z
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Finpartition.card_parts_equitabilise_subset_le : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {m a b : ℕ} (P : Finpartition s)
  (h : a * m + b * (m + 1) = s.card),
  t ∈ P.parts → (t \ {u ∈ (Finpartition.equitabilise h).parts | u ⊆ t}.biUnion id).card ≤ m
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.equivOfIso_symm_apply : ∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) (a : ↑W), (CategoryTheory.Quiv.equivOfIso e).symm a = e.inv.obj a
-- Lean.Elab.ParseImportsFast
Lean.PrintImportResult.mk.sizeOf_spec : ∀ (result? : Option Lean.ModuleHeader) (errors : Array String),
  sizeOf { result? := result?, errors := errors } = 1 + sizeOf result? + sizeOf errors
-- Mathlib.Logic.Basic
ne_and_eq_iff_right : ∀ {α : Sort u_1} {a b c : α}, b ≠ c → (a ≠ b ∧ a = c ↔ a = c)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.ext_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Closeds α}, s = t ↔ ↑s = ↑t
-- Mathlib.Algebra.Quaternion
Quaternion.re_one : ∀ {R : Type u_3} [inst : CommRing R], QuaternionAlgebra.re 1 = 1
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.add_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F)
  (x : ↥(f.domain ⊓ g.domain)), ↑(f + g) x = ↑f ⟨↑x, ⋯⟩ + ↑g ⟨↑x, ⋯⟩
-- Std.Time.Date.Unit.Year
Std.Time.Year.instAddOffset : Add Std.Time.Year.Offset
-- Batteries.Data.String.Lemmas
String.next_of_valid : ∀ (cs : List Char) (c : Char) (cs' : List Char),
  String.Pos.Raw.next (String.ofList (cs ++ c :: cs')) { byteIdx := String.utf8Len cs } =
    { byteIdx := String.utf8Len cs + c.utf8Size }
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_one_left_iff : ∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] {f : α → E} {l : Filter α}
  [inst_2 : One F] [NormOneClass F], (fun _x => 1) =o[l] f ↔ Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.map_id : ∀ (n : SimplexCategory),
  SSet.stdSimplex.map (SimplexCategory.Hom.mk OrderHom.id) = CategoryTheory.CategoryStruct.id (SSet.stdSimplex.obj n)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.union_eq_union! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF),
  t₁.union t₂ ⋯ ⋯ = t₁.union! t₂
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.foldUntil.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a))
  (h_2 : (x : Option α) → motive x),
  (match some a with
    | some a => h_1 a
    | x => h_2 x) =
    h_1 a
-- Init.Data.String.Slice
/-- If `pat` matches a suffix of `s`, returns the position at the beginning of the suffix.
Returns `none` otherwise.

This function is generic over all currently supported patterns.
 -/
String.Slice.skipSuffix? : {ρ : Type} → (s : String.Slice) → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Option s.Pos
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_map_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {Y : ι → Type u_3} [inst : (i : ι) → MeasurableSpace (Y i)]
  {f : (i : ι) → X i → Y i},
  (∀ (i : ι), Measurable (f i)) →
    MeasureTheory.Measure.map (fun x i => f i (x i)) (MeasureTheory.Measure.infinitePi μ) =
      MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (f i) (μ i)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsIsometricVAdd.mk : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X],
  (∀ (c : M), Isometry fun x => c +ᵥ x) → IsIsometricVAdd M X
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
/-- The exterior algebra is graded by the powers of the submodule `(ExteriorAlgebra.ι R).range`.  -/
ExteriorAlgebra.gradedAlgebra : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → GradedAlgebra fun i => ⋀[R]^i M
-- Mathlib.Algebra.Torsor.Basic
Function.Surjective.torsor.eq_1 : ∀ {G : Type u_1} {P : Type u_2} {Q : Type u_3} [inst : Group G] [inst_1 : Torsor G P] [inst_2 : SMul G Q]
  [inst_3 : SDiv G Q] (f : P → Q) (hf : Function.Surjective f) (smul : ∀ (c : G) (x : P), f (c • x) = c • f x)
  (sdiv : ∀ (x y : P), x /ₛ y = f x /ₛ f y),
  Function.Surjective.torsor f hf smul sdiv =
    { toMulAction := Function.Surjective.mulAction f hf smul, toSDiv := inst_3, nonempty := ⋯, sdiv_smul' := ⋯,
      smul_sdiv' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The type (II) simplices of `h : A.PairingCore`, as a family indexed by `h.ι`.  -/
SSet.Subcomplex.PairingCore.type₂ : {X : SSet} → {A : X.Subcomplex} → (h : A.PairingCore) → h.ι → A.N
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.PosDef.add : ∀ {M : Type u_4} {N : Type u_5} {R₂ : Type u} [inst : CommSemiring R₂] [inst_1 : AddCommMonoid M] [inst_2 : Module R₂ M]
  [inst_3 : PartialOrder N] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] [AddLeftStrictMono N]
  (Q Q' : QuadraticMap R₂ M N), Q.PosDef → Q'.PosDef → (Q + Q').PosDef
-- Mathlib.Algebra.Regular.SMul
/-- **Alias** of the forward direction of `isSMulRegular_map`. -/
IsSMulRegular.of_map : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [inst : SMul R M] [inst_1 : SMul S M] (f : R → S),
  (∀ (m : M), f a • m = a • m) → IsSMulRegular M (f a) → IsSMulRegular M a
-- Mathlib.Analysis.Convex.Between
Sbtw.ne_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P}, Sbtw R x y z → y ≠ z
-- Mathlib.Topology.Order
IndiscreteTopology.mk : ∀ {α : Type u_2} [inst : TopologicalSpace α], inst = ⊤ → IndiscreteTopology α
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.LazyTraceChildren : Type
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
/-- A noncomputable variant of `IterM.step` using the `HetT` monad.
It is used in the definition of the equivalence relations on iterators,
namely `IterM.Equiv` and `Iter.Equiv`.
 -/
Std.IterM.stepAsHetT : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [Std.Iterator α m β] → [Monad m] → Std.IterM m β → Std.Iterators.HetT m (Std.IterStep (Std.IterM m β) β)
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.Ref.flip.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (ref : aig.Ref) (inv : Bool),
  ref.flip inv = { gate := ref.gate, invert := inv ^^ ref.invert, hgate := ⋯ }
-- Mathlib.RepresentationTheory.Intertwining
Representation.IsIntertwiningMap.isIntertwining : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {f : V →ₗ[A] W},
  ρ.IsIntertwiningMap σ f → ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.homEquiv_symm_π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C}
  (f : (CategoryTheory.Functor.const J).obj W ⟶ F) (j : J),
  CategoryTheory.CategoryStruct.comp (h.homEquiv.symm f) (t.π.app j) = f.app j
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (s : Finset α), s +ᵥ ∅ = ∅
-- Batteries.Data.List.Lemmas
List.getElem?_set_eq_of_lt : ∀ {α : Type u_1} (a : α) {n : ℕ} {l : List α}, n < l.length → (l.set n a)[n]? = some a
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedAddCommGroup.Subgroup.negGen.eq_1 : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G] (H : AddSubgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsAddCyclic ↥H], LinearOrderedAddCommGroup.Subgroup.negGen H = ⋯.choose
-- Mathlib.RingTheory.Spectrum.Prime.Basic
_private.Mathlib.RingTheory.Spectrum.Prime.Basic.0.PrimeSpectrum.primeSpectrumProdOfSum.match_1.eq_2 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (motive : PrimeSpectrum R ⊕ PrimeSpectrum S → Sort u_3) (J : Ideal S) (isPrime : J.IsPrime)
  (h_1 : (I : Ideal R) → (isPrime : I.IsPrime) → motive (Sum.inl { asIdeal := I, isPrime := isPrime }))
  (h_2 : (J : Ideal S) → (isPrime : J.IsPrime) → motive (Sum.inr { asIdeal := J, isPrime := isPrime })),
  (match Sum.inr { asIdeal := J, isPrime := isPrime } with
    | Sum.inl { asIdeal := I, isPrime := isPrime } => h_1 I isPrime
    | Sum.inr { asIdeal := J, isPrime := isPrime } => h_2 J isPrime) =
    h_2 J isPrime
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_zero : Polynomial.bernoulli 0 = 1
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instOne : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module A V] → (ρ : Representation A G V) → One (ρ.IntertwiningMap ρ)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddEquiv.ofLeftInverse_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) {g : N → M}
  (h : Function.LeftInverse g ⇑f) (a : M), (AddEquiv.ofLeftInverse f h) a = f.srangeRestrict a
-- Std.Data.ExtDTreeMap.Basic
/-- Implementation detail of the tree map  -/
Std.ExtDTreeMap.mk' : {α : Type u} →
  {β : α → Type v} →
    {cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap._auto_1} →
      Quotient (Std.DTreeMap.isSetoid α β cmp) → Std.ExtDTreeMap α β cmp
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_bUnion : ∀ {R : Type u} [inst : CommSemiring R] (s : Set (Set R)),
  PrimeSpectrum.zeroLocus (⋃ s' ∈ s, s') = ⋂ s' ∈ s, PrimeSpectrum.zeroLocus s'
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkipWhile_eq_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, ¬String.Slice.Pattern.Model.RevMatchesAt pat pos → pos.revSkipWhile pat = pos
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  {v : β k}, (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ k ∉ m then some (cast ⋯ v) else m.get? a
-- Mathlib.Data.Nat.Cast.Basic
Nat.cast_mul : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (m n : ℕ), ↑(m * n) = ↑m * ↑n
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits an inverse.  -/
Subgroup.inv : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → Inv ↥H
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffAt_piLp' : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [inst_5 : Fintype ι] (p : ENNReal) [inst_6 : Fact (1 ≤ p)] {n : WithTop ℕ∞}
  {f : H → PiLp p E} {y : H}, (∀ (i : ι), ContDiffAt 𝕜 n (fun x => (f x).ofLp i) y) → ContDiffAt 𝕜 n f y
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X)
  (P : CategoryTheory.Functor Cᵒᵖ A) {F : A → A → Type uF} {carrier : A → Type w_1}
  {instFunLike : (X Y : A) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory A F]
  (x_1 : carrier (P.obj (Opposite.op Y))),
  (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P))
      ((CategoryTheory.ConcreteCategory.hom (P.map f.op)) x_1) =
    (CategoryTheory.ConcreteCategory.hom
        (Φ.toPresheafFiber Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) P))
      x_1
-- Init.Data.Iterators.Basic
/-- The relation of plausible successors during skips is well-founded.  -/
Std.Iterators.Productive.wf : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} {inst : Std.Iterator α m β}
  [self : Std.Iterators.Productive α m], WellFounded Std.IterM.IsPlausibleSkipSuccessorOf
-- Mathlib.Topology.Separation.Basic
isClosedMap_const : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] {y : Y},
  IsClosedMap (Function.const X y)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_le_of_nonempty : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : ℝ}, ‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) (Δ : SimplexCategory),
  AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.CategoryStruct.id Δ) =
    CategoryTheory.CategoryStruct.id (K.X Δ.len)
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Perfect.eq_1 : ∀ (n : ℕ), n.Perfect = (∑ i ∈ n.properDivisors, i = n ∧ 0 < n)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.go.goArg : Lean.Expr →
  Bool →
    Lean.Meta.Grind.NormalizePattern.PatternArgKind →
      Lean.Meta.Grind.NormalizePattern.ParentKind✝ → Lean.Meta.Grind.NormalizePattern.M✝ Lean.Expr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.intCast.sizeOf_spec : ∀ (k : ℤ), sizeOf (Lean.Grind.CommRing.Expr.intCast k) = 1 + sizeOf k
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.codRestrict_apply' : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (p : L.Substructure N) (f : L.Embedding M N) {h : ∀ (c : M), f c ∈ p} (x : M),
  (FirstOrder.Language.Embedding.codRestrict p f h) x = ⟨f x, ⋯⟩
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.unitsMulComplexConjInv.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  NumberField.IsCMField.unitsMulComplexConjInv K = NumberField.IsCMField.unitsMulComplexConjInv K
-- Mathlib.Algebra.Ring.Opposite
NonUnitalRingHom.unop.eq_1 : ∀ {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S],
  NonUnitalRingHom.unop = NonUnitalRingHom.op.symm
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {Z : CategoryTheory.Functor C C}
  (h : (t.truncLT n).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncGEπ n) (CategoryTheory.CategoryStruct.comp (t.truncGEδLT n) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.rciIterator : {α : Type u_1} → {β : α → Type u_2} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Std.Iter ((a : α) × β a)
-- Mathlib.Probability.Kernel.Basic
/-- The identity kernel, that maps `x : α` to the Dirac measure at `x`.  -/
ProbabilityTheory.Kernel.id : {α : Type u_1} → {mα : MeasurableSpace α} → ProbabilityTheory.Kernel α α
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool} {k : α},
  (Std.TreeSet.filter f t).get? k = Option.filter f (t.get? k)