mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Finite.Basic
/-- Using choice, get the `Finset` that represents this `Set`.  -/
Set.Finite.toFinset : {α : Type u} → {s : Set α} → s.Finite → Finset α
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.multiplicity_add_of_gt : ∀ {α : Type u_1} [inst : Ring α] {p a b : α},
  FiniteMultiplicity p b → multiplicity p b < multiplicity p a → multiplicity p (a + b) = multiplicity p b
-- Init.Data.SInt.Lemmas
Int8.ofNat_add : ∀ (a b : ℕ), Int8.ofNat (a + b) = Int8.ofNat a + Int8.ofNat b
-- Mathlib.Order.SymmDiff
sdiff_symmDiff_right : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), b \ symmDiff a b = a ⊓ b
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.hom_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  (c₁₂ : ComplexShape ι₁₂) {c₂₃ : ComplexShape ι₂₃} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
  [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {j : ι₄} {A : C₄} {f g : ⋯.X j ⟶ A},
  (∀ (i₁ : ι₁), ⋯) → f = g
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- a map `I₁ × I₂ → I₁₂`  -/
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.p : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} →
      {J : Type u_10} →
        {r : I₁ × I₂ × I₃ → J} → (self : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) → I₁ × I₂ → self.I₁₂
-- Init.Data.Dyadic.Basic
Dyadic.mul_assoc : ∀ (x y z : Dyadic), x * y * z = x * (y * z)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_one_tmul : ∀ (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)]
  [inst_8 : GradedMonoid.GOne 𝒜] (b : DirectSum ι fun i => ℬ i),
  (TensorProduct.gradedComm R 𝒜 ℬ) (1 ⊗ₜ[R] b) = b ⊗ₜ[R] 1
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.Subtype.countablySeparated : ∀ {α : Type u_1} [inst : MeasurableSpace α] [h : MeasurableSpace.CountablySeparated α] {s : Set α},
  MeasurableSpace.CountablySeparated ↑s
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.AddMonObj A] {X Y : CategoryTheory.AddMod D A} (f : X ⟶ Y),
  (CategoryTheory.AddMod.forget A).map f = f.hom
-- Lean.Syntax
/-- Returns a synthetic Syntax which has the specified `Lean.Syntax.Range`.  -/
Lean.Syntax.ofRange : Lean.Syntax.Range → optParam Bool true → Lean.Syntax
-- Init.Data.Nat.Div.Basic
Nat.div.go.eq_1 : ∀ (y : ℕ) (hy : 0 < y) (x fuel_2 : ℕ) (hfuel_2 : x < fuel_2.succ),
  Nat.div.go y hy fuel_2.succ x hfuel_2 = if h : y ≤ x then Nat.div.go y hy fuel_2 (x - y) ⋯ + 1 else 0
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.IsReduced.reverse : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {ω : List B},
  cs.IsReduced ω → cs.IsReduced ω.reverse
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodSpec_inr : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (AlgebraicGeometry.coprodSpec R S) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S))
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toListRev`.
 -/
Std.IterM.Total.toListRev : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [Monad m] → [inst : Std.Iterator α m β] → [Std.Iterators.Finite α m] → Std.IterM.Total m β → m (List β)
-- Mathlib.Order.Sublattice
/-- The natural lattice hom from a sublattice to the original lattice.  -/
Sublattice.subtype : {α : Type u_2} → [inst : Lattice α] → (L : Sublattice α) → LatticeHom (↥L) α
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signBijAux.eq_1 : ∀ {n : ℕ} (f : Equiv.Perm (Fin n)) (a : (_ : Fin n) × Fin n),
  f.signBijAux a = if x : f a.snd < f a.fst then ⟨f a.fst, f a.snd⟩ else ⟨f a.snd, f a.fst⟩
-- Mathlib.Analysis.Complex.Exponential
/-- the exponential function as a monoid hom from `Multiplicative ℝ` to `ℝ`  -/
Real.expMonoidHom : Multiplicative ℝ →* ℝ
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.trace.sizeOf_spec : ∀ (indent : ℕ) (cls : Lean.Name) (msg : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) (collapsed : Bool)
  (children :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
      (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)),
  sizeOf (Lean.Widget.MsgEmbed.trace indent cls msg collapsed children) =
    1 + sizeOf indent + sizeOf cls + sizeOf msg + sizeOf collapsed + sizeOf children
-- Mathlib.CategoryTheory.EffectiveEpi.Coproduct
CategoryTheory.instEffectiveEpiDescOfEffectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} (X : α → C)
  (π : (a : α) → X a ⟶ B) [inst_1 : CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpiFamily X π],
  CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π)
-- Mathlib.Util.Notation3
Mathlib.Notation3.instReprDelabKey : Repr Mathlib.Notation3.DelabKey
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.lctx₁ : Aesop.EqualUpToIds.GoalContext → Lean.LocalContext
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_25 : HSub Std.Time.Hour.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Std.Time.Format.Modifier
Std.Time.Modifier.w.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.w presentation = Std.Time.Modifier.w presentation_1 → presentation = presentation_1
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.forgetAdjStar_unit_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] (X : C)
  (Y : CategoryTheory.Over X),
  CategoryTheory.Over.Hom.left ((CategoryTheory.Over.forgetAdjStar X).unit.app Y) =
    CategoryTheory.Limits.prod.lift Y.hom (CategoryTheory.CategoryStruct.id Y.left)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.measurable_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β),
  Measurable f → Measurable fun μ => MeasureTheory.Measure.map f μ
-- Mathlib.Data.Int.GCD
Int.gcd_def : ∀ (i j : ℤ), i.gcd j = i.natAbs.gcd j.natAbs
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_sub_cancel_right : ∀ {m n k : ℤ} (i : ℤ), (m - i).fmod n = (k - i).fmod n ↔ m.fmod n = k.fmod n
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isCycle_map_iff_of_injective`. -/
SimpleGraph.Walk.IsCycle.map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u},
  Function.Injective ⇑f → p.IsCycle → (SimpleGraph.Walk.map f p).IsCycle
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- A recurrence relation that expresses the `(n+1)`th term of the stream of `IntFractPair`s
of `v` for non-integer `v` in terms of the `n`th term of the stream associated to
the inverse of the fractional part of `v`.
 -/
GenContFract.IntFractPair.stream_succ : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K},
  Int.fract v ≠ 0 →
    ∀ (n : ℕ), GenContFract.IntFractPair.stream v (n + 1) = GenContFract.IntFractPair.stream (Int.fract v)⁻¹ n
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.one_def : Real.one✝ = { cauchy := 1 }
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.prev_eq_self : ∀ {ι : Type u_1} (c : ComplexShape ι) (j : ι), ¬c.Rel (c.prev j) j → c.prev j = j
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.toMonoidHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β],
  Function.Injective MonoidWithZeroHom.toMonoidHom
-- Mathlib.Order.OrderDual
OrderDual.instIsTransLt : ∀ {α : Type u_1} [inst : LT α] [T : IsTrans α LT.lt], IsTrans αᵒᵈ LT.lt
-- Mathlib.Analysis.Normed.Group.Pointwise
neg_cthickening : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E),
  -Metric.cthickening δ s = Metric.cthickening δ (-s)
-- Mathlib.Algebra.Group.End
MulAut.one_apply : ∀ (M : Type u_2) [inst : Mul M] (m : M), 1 m = m
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse, version subtracting vectors.  -/
Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_singleton : ∀ {α : Type u_1} (a : α), {a}.card = 1
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.div_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Div γ] [inst_4 : ContinuousDiv γ] (f g : C(β, γ)) (h : C(α, β)),
  (f / g).comp h = f.comp h / g.comp h
-- Mathlib.Topology.Algebra.Group.Basic
AddUnits.instCompactSpaceOfT1SpaceOfContinuousAdd : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousAdd α] [CompactSpace α],
  CompactSpace (AddUnits α)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o] [LawfulMonad m] [LawfulMonad n]
  [LawfulMonad o] [inst_8 : Std.IteratorLoop α m n] [inst_9 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n]
  [Std.LawfulIteratorLoop α m o] [inst_12 : MonadLiftT m n] [inst_13 : MonadLiftT n o] [LawfulMonadLiftT m n]
  [LawfulMonadLiftT n o] {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ}
  {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.filterMapWithPostcondition f it) =
    Std.IterM.foldM
      (fun d b => do
        let __x ← liftM (f b).run
        match __x with
          | some c => g d c
          | x => pure d)
      init it
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.C_transpose : ∀ (n : ℕ), (CartanMatrix.C n).transpose = CartanMatrix.B n
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.comul_apply : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B] (r : A × B),
  CoalgebraStruct.comul r =
    (TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B)) (CoalgebraStruct.comul r.1) +
      (TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B)) (CoalgebraStruct.comul r.2)
-- Mathlib.Algebra.Group.Prod
SemiconjBy.prod : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] {x y z : M × N},
  SemiconjBy x.1 y.1 z.1 → SemiconjBy x.2 y.2 z.2 → SemiconjBy x y z
-- Init.Data.String.Lemmas.Basic
String.getUTF8Byte_toSlice : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.toSlice.rawEndPos}, s.toSlice.getUTF8Byte p h = s.getUTF8Byte p h
-- Mathlib.Data.Sum.Order
/-- The linear/lexicographical `<` on a sum.  -/
Sum.Lex.LT : {α : Type u_1} → {β : Type u_2} → [LT α] → [LT β] → LT (α ⊕ₗ β)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk : {V : Type u} →
  (Adj : V → V → Prop) →
    autoParam (Std.Symm Adj) SimpleGraph.symm._autoParam →
      autoParam (Std.Irrefl Adj) SimpleGraph.loopless._autoParam → SimpleGraph V
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instCommMonoid : {A : Type u_2} →
  {E : Type u_6} →
    [inst : Monoid A] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : CommMonoid E] → [inst_3 : TopologicalSpace E] → [ContinuousMul E] → CommMonoid (A →ₜ* E)
-- Lean.Meta.Basic
Lean.Meta.ConfigWithKey.config : Lean.Meta.ConfigWithKey → Lean.Meta.Config
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {f g : (i : ι) → α i},
  (Set.univ.pi fun i => Set.Ico (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Icc f g
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.presieve₀_sigma : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsZariskiLocalAtSource P]
  [inst_1 : UnivLE.{v, u}] {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S),
  𝒰.sigma.presieve₀ = CategoryTheory.Presieve.singleton (CategoryTheory.Limits.Sigma.desc 𝒰.f)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
range_cfc_eq_range_cfcHom : ∀ (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] [inst_9 : StarModule R A]
  {a : A} (ha : p a), (Set.range fun x => cfc x a) = ↑(cfcHom ha).range
-- Mathlib.GroupTheory.Complement
/-- A left transversal is in bijection with left cosets.  -/
AddSubgroup.IsComplement.leftQuotientEquiv : {G : Type u_1} → [inst : AddGroup G] → {H : AddSubgroup G} → {S : Set G} → AddSubgroup.IsComplement S ↑H → G ⧸ H ≃ ↑S
-- Std.Data.DHashMap.Iterator
/-- Returns a finite iterator over the values of a hash map.
The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DHashMap.Raw.valuesIter : {α β : Type u} → (Std.DHashMap.Raw α fun x => β) → Std.Iter β
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comapₗ.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (f : α → β),
  MeasureTheory.Measure.comapₗ f =
    if hf : Function.Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s) then
      MeasureTheory.Measure.liftLinear (MeasureTheory.OuterMeasure.comap f) ⋯
    else 0
-- Mathlib.Tactic.Linarith.Verification
/-- A type-safe analogue of `addExprs`.  -/
Mathlib.Tactic.Linarith.addExprs' : {u : Lean.Level} →
  {α :
      have u := u;
      Q(Type u)} →
    Q(AddMonoid «$α») → List Q(«$α») → Q(«$α»)
-- Mathlib.Order.WithBot
WithTop.coe_eq_coe : ∀ {α : Type u_1} {a b : α}, ↑a = ↑b ↔ a = b
-- Mathlib.Topology.Algebra.Module.LocallyConvex
Pi.locallyConvexSpace : ∀ {𝕜 : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] {ι : Type u_5} {X : ι → Type u_6}
  [inst_2 : (i : ι) → AddCommMonoid (X i)] [inst_3 : (i : ι) → TopologicalSpace (X i)]
  [inst_4 : (i : ι) → Module 𝕜 (X i)] [∀ (i : ι), LocallyConvexSpace 𝕜 (X i)], LocallyConvexSpace 𝕜 ((i : ι) → X i)
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.mem_centralizer_iff : ∀ {M : Type u_1} {S : Set M} [inst : Semigroup M] {z : M}, z ∈ Subsemigroup.centralizer S ↔ ∀ g ∈ S, g * z = z * g
-- Mathlib.Data.List.PeriodicityLemma
/-- An equivalent definition of `HasPeriod w p` by modular equivalence on indices.  -/
List.hasPeriod_iff_forall_getElem?_mod : ∀ {α : Type u_1} {p : ℕ} {w : List α}, w.HasPeriod p ↔ ∀ i < w.length, w[i]? = w[i % p]?
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.val_map_eq_iff : ∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : LinearOrderedCommMonoidWithZero ΓR] [inst_3 : LinearOrderedCommMonoidWithZero ΓA] [inst_4 : Algebra R A]
  (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x y : R),
  vA ((algebraMap R A) x) = vA ((algebraMap R A) y) ↔ vR x = vR y
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.coe_ratCast : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] (s : S) (x : ℚ),
  ↑↑x = ↑x
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.prod_le_tprod : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] [L.NeBot] [L.LeAtTop] {f : ι → α} (s : Finset ι),
  (∀ i ∉ s, 1 ≤ f i) → Multipliable f L → ∏ i ∈ s, f i ≤ ∏'[L] (i : ι), f i
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometry.adjoint_comp_self : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_5} {E' : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] [inst_4 : NormedAddCommGroup E']
  [inst_5 : InnerProductSpace 𝕜 E'] [inst_6 : CompleteSpace E'] (f : E →ₗᵢ[𝕜] E'),
  ContinuousLinearMap.adjoint f.toContinuousLinearMap ∘SL f.toContinuousLinearMap = 1
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- The restriction of the norm on `L/K` restricted onto `B/A` in an AKLB setup.
See `Algebra.intNorm` instead.  -/
Algebra.intNormAux : (A : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      (B : Type u_6) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : Algebra A B] →
              [inst_3 : Field K] →
                [inst_4 : Field L] →
                  [inst_5 : Algebra A K] →
                    [IsFractionRing A K] →
                      [inst_7 : Algebra K L] →
                        [inst_8 : Algebra A L] →
                          [IsScalarTower A K L] →
                            [inst_10 : Algebra B L] →
                              [IsScalarTower A B L] → [IsIntegralClosure B A L] → [IsIntegrallyClosed A] → B →* A
-- Mathlib.Order.Defs.Unbundled
/-- In a trichotomous irreflexive order, every element is determined by the set of predecessors.  -/
extensional_of_trichotomous_of_irrefl : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Trichotomous r] [Std.Irrefl r] {a b : α}, (∀ (x : α), r x a ↔ r x b) → a = b
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_star : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : StarAddMonoid β] [inst_4 : ContinuousStar β] (f : ZeroAtInftyContinuousMap α β), ⇑(star f) = star ⇑f
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) (n : ℕ),
  groupHomology.map (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) n =
    CategoryTheory.CategoryStruct.comp (groupHomology.map f φ n) (groupHomology.map g ψ n)
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
exteriorPower.ιMultiDual.eq_1 : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)),
  exteriorPower.ιMultiDual R n b s = (exteriorPower.pairingDual R M n) (exteriorPower.ιMulti_family R n b.coord s)
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_lt_descFactorial : ∀ {n k : ℕ}, 2 ≤ k → k ≤ n → n.choose k < n.descFactorial k
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- An equality `a = 0` coming from the core.  -/
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0 : Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.toEquiv : {α : Type u} → {β : Type v} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → α ≃ᵢ β → α ≃ β
-- Init.Control.Reader
instMonadAttachReaderTOfMonad : {m : Type u_1 → Type u_2} → {ρ : Type u_1} → [Monad m] → [MonadAttach m] → MonadAttach (ReaderT ρ m)
-- Mathlib.RingTheory.WittVector.Identities
/-- This is a slightly specialized form of [Hazewinkel, *Witt Vectors*][Haze09] 6.2 equation 5.  -/
WittVector.iterate_verschiebung_mul_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x y : WittVector p R) (i j : ℕ),
  ((⇑WittVector.verschiebung)^[i] x * (⇑WittVector.verschiebung)^[j] y).coeff (i + j) =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
-- Init.Control.Lawful.Instances
ReaderT.ext : ∀ {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : ReaderT ρ m α},
  (∀ (ctx : ρ), x.run ctx = y.run ctx) → x = y
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.mk.inj : ∀ {K : Type u_1} {b : ℤ} {fr : K} {b_1 : ℤ} {fr_1 : K},
  { b := b, fr := fr } = { b := b_1, fr := fr_1 } → b = b_1 ∧ fr = fr_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
algebraMap_le_iff_le_spectrum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  {r : R} {a : A},
  autoParam (p a) algebraMap_le_iff_le_spectrum._auto_1 → ((algebraMap R A) r ≤ a ↔ ∀ x ∈ spectrum R a, r ≤ x)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If a category has images, equalizers and pullbacks, then images are automatically strong epi
images.  -/
CategoryTheory.Limits.hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasImages C]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasEqualizers C],
  CategoryTheory.Limits.HasStrongEpiImages C