mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- Construct a modification isomorphism between oplax natural transformations
by giving object level isomorphisms, and checking naturality only in the forward direction.
 -/
CategoryTheory.Lax.OplaxTrans.isoMk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ≅ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
                        (θ.naturality f) =
                      CategoryTheory.CategoryStruct.comp (η.naturality f)
                        (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
                  CategoryTheory.Lax.OplaxTrans.isoMk._auto_1 →
                (η ≅ θ)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_top_of_eq_top : ∀ {α : Type u_1} {f : α → ENNReal}, (∃ a, f a = ⊤) → ∑' (a : α), f a = ⊤
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
  Polynomial.eval x (Polynomial.map f p) = Polynomial.eval₂ f x p
-- Mathlib.Algebra.Lie.AdjointAction.Basic
/-- The adjoint of a semisimple element is semisimple.  -/
LieAlgebra.ad_isSemisimple_of_isSemisimple : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [PerfectField K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [FiniteDimensional K V] {a : Module.End K V}, a.IsSemisimple → ((LieAlgebra.ad K (Module.End K V)) a).IsSemisimple
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Triangle diagrams for (right) extensions.
```
  b
  △ \
  |   \ extension  | counit
f |     \          ▽
  |       ◿
  a - - - ▷ c
      g
```
 -/
CategoryTheory.Bicategory.RightExtension : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b c : B} → (a ⟶ b) → (a ⟶ c) → Type (max v w)
-- Std.Data.DTreeMap.Raw.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.get : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → (t : Std.DTreeMap.Raw α β cmp) → (a : α) → a ∈ t → β a
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.getEntryLTD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Sigma β → (a : α) × β a
-- Mathlib.Data.SetLike.Basic
SetLike.le_def : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : LE A] [IsConcreteLE A B] {S T : A},
  S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T
-- Mathlib.Data.TypeVec
TypeVec.toSubtype_of_subtype : ∀ {n : ℕ} {α : TypeVec.{u_1} n} (p : α.Arrow (TypeVec.repeat n Prop)),
  TypeVec.comp (TypeVec.toSubtype p) (TypeVec.ofSubtype p) = TypeVec.id
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
/-- Whiskering right and then taking a limit is the same as taking the limit and applying the
functor.  -/
CategoryTheory.limitCompWhiskeringRightIsoLimitComp : {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] →
        {E : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {J : Type u_4} →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} J] →
                [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D] →
                  (F : CategoryTheory.Functor D E) →
                    [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J F] →
                      (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) →
                        CategoryTheory.Limits.limit (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) ≅
                          (CategoryTheory.Limits.limit G).comp F
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instReprConfig.repr : Mathlib.Tactic.RingNF.Config → ℕ → Std.Format
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k : α} {f : β → β} {hc : k ∈ Std.ExtDTreeMap.Const.modify t k f},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.modify t k f) k hc = f (Std.ExtDTreeMap.Const.get t k ⋯)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instInhabitedStruct : Inhabited Lean.Meta.Grind.Arith.Linear.Struct
-- Mathlib.CategoryTheory.Yoneda
/-- The Yoneda lemma asserts that the Yoneda pairing
`(X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F)`
is naturally isomorphic to the evaluation `(X, F) ↦ F.obj X`.  -/
CategoryTheory.yonedaLemma : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.yonedaPairing C ≅ CategoryTheory.yonedaEvaluation C
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_hom_rel : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] {r : M → N → Prop}
  {f : ι → M} {g : ι → N} {s : Finset ι},
  r 1 1 → (∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)) → r (∏ x ∈ s, f x) (∏ x ∈ s, g x)
-- Mathlib.LinearAlgebra.Matrix.Diagonal
Matrix.diagonal_toLin' : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type v} [inst_2 : CommSemiring R] (w : n → R),
  Matrix.toLin' (Matrix.diagonal w) = LinearMap.pi fun i => w i • LinearMap.proj i
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findSome?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Homology.Homotopy
prevD_nat : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (C D : CochainComplex V ℕ) (i : ℕ) (f : (i j : ℕ) → C.X i ⟶ D.X j),
  (prevD i) f = CategoryTheory.CategoryStruct.comp (f i (i - 1)) (D.d (i - 1) i)
-- Init.Data.Array.MapIdx
Array.mapFinIdxM.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : (i : ℕ) → α → i < as.size → m β),
  as.mapFinIdxM f = Array.mapFinIdxM.map as f as.size 0 ⋯ (Array.emptyWithCapacity as.size)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.const_coeff : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a → ∀ (s : σ), IsNilpotent (MvPowerSeries.constantCoeff (a s))
-- Mathlib.MeasureTheory.Measure.Restrict
volume_image_subtype_coe : ∀ {α : Type u_2} [inst : MeasureTheory.MeasureSpace α] {s : Set α},
  MeasurableSet s → ∀ (t : Set ↑s), MeasureTheory.volume (Subtype.val '' t) = MeasureTheory.volume t
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.insert : {γ : Type} →
  Lean.KeyedDeclsAttribute.ExtensionState γ →
    Lean.KeyedDeclsAttribute.AttributeEntry γ → Lean.KeyedDeclsAttribute.ExtensionState γ
-- Lean.Meta.Basic
Lean.Meta.orElse : {α : Type} → Lean.MetaM α → (Unit → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_surjective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, Function.Surjective ⇑f → Function.Surjective (Submonoid.map f)
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_sum_of_commute : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸]
  [CompleteSpace 𝔸] {ι : Type u_6} (s : Finset ι) (f : ι → Matrix m m 𝔸) (h : (↑s).Pairwise (Function.onFun Commute f)),
  NormedSpace.exp (∑ i ∈ s, f i) = s.noncommProd (fun i => NormedSpace.exp (f i)) ⋯
-- Mathlib.RingTheory.Multiplicity
emultiplicity_lt_top : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, emultiplicity a b < ⊤ ↔ FiniteMultiplicity a b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.keysArray_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).keysArray =
    (Array.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯))
        t.keysArray.attach).unattach
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- `(toSimpleFunc f)` is measurable.  -/
MeasureTheory.Lp.simpleFunc.measurable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasurableSpace E] (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  Measurable ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getOfNotLE? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' fallback : α},
      cmp k k' = Ordering.eq →
        k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).getD k' fallback = k
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_neg_add_self_nhdsGE : ∀ {E : Type u_4} [inst : SeminormedAddGroup E] (x : E),
  Filter.Tendsto (fun a => ‖-a + x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))
-- Mathlib.Util.Export
Lean.Export.instOfStateLevel : Lean.Export.OfState Lean.Level
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor : ∀ (V : SSet.Truncated 2), (SSet.Truncated.HomotopyCategory.quotientFunctor V).Full
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R),
  MonoidAlgebra.single m r = MonoidAlgebra.ofCoeff fun₀ | m => r
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_coe_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithZero α} {b : α}, x ≤ ↑b ↔ ∀ (a : α), x = ↑a → a ≤ b
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- Given an `n`-th primitive root of unity `ζ`, we have that `ζ - 1` is associated to any of its
conjugate.  -/
IsPrimitiveRoot.associated_sub_one_map_sub_one : ∀ {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A] {R : Type u_3} [inst_2 : CommRing R] [inst_3 : Algebra R A]
  {n : ℕ} [NeZero n], IsPrimitiveRoot ζ n → ∀ (σ : A ≃ₐ[R] A), Associated (ζ - 1) (σ (ζ - 1))
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCyclesIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i], (K.iCyclesIso i j hj h).hom = K.iCycles i
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsStableUnderComposition.inverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.MorphismProperty D} [P.IsStableUnderComposition] (F : CategoryTheory.Functor C D),
  (P.inverseImage F).IsStableUnderComposition
-- Mathlib.Algebra.DirectSum.Ring
/-- A direct sum of copies of a `NonUnitalNonAssocSemiring` inherits the multiplication structure.
 -/
NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring : (ι : Type u_1) →
  {R : Type u_2} →
    [inst : AddMonoid ι] → [inst_1 : NonUnitalNonAssocSemiring R] → DirectSum.GNonUnitalNonAssocSemiring fun x => R
-- Lean.Parser.Term
Lean.Parser.Term.matchExprAlts.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.numeratorHom_inj : ∀ {R : Type u_1} [inst : Ring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  S ≤ nonZeroDivisorsLeft R → Function.Injective ⇑OreLocalization.numeratorHom
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_3),
  (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₃ =
    CategoryTheory.CategoryStruct.id (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Data.ENNReal.Basic
ENNReal.zero_lt_top : 0 < ⊤
-- Init.NotationExtra
unexpandMkArray4 : Lean.PrettyPrinter.Unexpander
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Weight (exponent in the functional equation)  -/
WeakFEPair.k : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℝ
-- Mathlib.Topology.Connected.Basic
instConnectedSpaceForall : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), ConnectedSpace (X i)],
  ConnectedSpace ((i : ι) → X i)
-- Init.Data.Vector.Basic
/-- Custom eliminator for `Vector α n` through `List α`  -/
Vector.elimAsList : {α : Type u_1} →
  {n : ℕ} →
    {motive : Vector α n → Sort u} →
      ((l : List α) → (ha : l.length = n) → motive (Vector.mk { toList := l } ha)) → (xs : Vector α n) → motive xs
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm_apply_eq : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) {x : N} {y : M}, e.symm x = y ↔ x = e y
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.refl_trans : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), (ContinuousAffineEquiv.refl k P₁).trans e = e
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLT.toPosSMulMono : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β] [inst_3 : Zero α]
  [PosSMulReflectLT α β], PosSMulMono α β
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.associator_inv_iso_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b)
  (y : b ⟶ c) (z : c ⟶ d),
  (CategoryTheory.Bicategory.associator x y z).inv.iso.hom = (CategoryTheory.Bicategory.associator x.of y.of z.of).inv
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- The colimit of `F ⋙ forget₂ (ModuleCat R) AddCommGrpCat` in the category `AddCommGrpCat`.
In the following, we will show that this has the structure of an `R`-module.
 -/
ModuleCat.FilteredColimits.M : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J (ModuleCat R) → AddCommGrpCat
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.inhabitedCone.eq_1 : ∀ {C : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C),
  CategoryTheory.Limits.inhabitedCone F =
    {
      default :=
        { pt := F.obj { as := PUnit.unit },
          π :=
            {
              app := fun x =>
                match x with
                | { as := PUnit.unit } =>
                  CategoryTheory.CategoryStruct.id
                    (((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{u_1 + 1})).obj
                          (F.obj { as := PUnit.unit })).obj
                      { as := PUnit.unit }),
              naturality := ⋯ } } }
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensorHom_tmul : ∀ {R : Type u} [inst : CommSemiring R] {K L M N : SemimoduleCat R} (f : K ⟶ L) (g : M ⟶ N) (k : ↑K) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (k ⊗ₜ[R] m) =
    (CategoryTheory.ConcreteCategory.hom f) k ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) m
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
prodIsoPullback_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv CategoryTheory.Limits.prod.snd =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The second modified cyclotomic polynomial is `X + 1` if the characteristic of `R` is not `2`.  -/
Polynomial.cyclotomic'_two : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R] (p : ℕ) [CharP R p],
  p ≠ 2 → Polynomial.cyclotomic' 2 R = Polynomial.X + 1
-- Init.Data.List.Lemmas
List.concat_inj : ∀ {α : Type u_1} {a b : α} {l l' : List α}, l.concat a = l'.concat b ↔ l = l' ∧ a = b
-- Mathlib.Algebra.Group.Action.Basic
MulDistribMulAction.toMonoidHom_apply : ∀ {M : Type u_2} (A : Type u_3) [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A] (r : M)
  (x : A), (MulDistribMulAction.toMonoidHom A r) x = r • x
-- Init.Data.Array.Lemmas
Array.flatten_ne_empty_iff : ∀ {α : Type u_1} {xss : Array (Array α)}, xss.flatten ≠ #[] ↔ ∃ xs ∈ xss, xs ≠ #[]
-- Init.Data.Array.Monadic
/-- This lemma identifies monadic maps over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Array.mapM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Prop}
  {xs : Array { x // p x }} {f : { x // p x } → m β} {g : α → m β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Array.mapM f xs = Array.mapM g xs.unattach
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.mapsTo_Ico : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictMonoOn f (Set.Icc a b) → Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instPosMulReflectLT : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : Preorder α] [PosMulReflectLT α],
  PosMulReflectLT (WithBot α)
-- Lean.Data.AssocList
Lean.AssocList.mapVal : {α : Type u} → {β : Type v} → {δ : Type w} → (β → δ) → Lean.AssocList α β → Lean.AssocList α δ
-- Init.Data.UInt.Bitwise
instAssociativeUInt16HXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Given tactic syntax `tac` that we want to paste into the editor, return it as a string.
This function respects the 100 character limit for long lines.  -/
Mathlib.Tactic.ClickSuggestions.tacticPasteString : Lean.TSyntax `tactic → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM String
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_add_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionSemiring α] {q r : ℚ≥0}, ↑q.den ≠ 0 → ↑r.den ≠ 0 → ↑(q + r) = ↑q + ↑r
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`.  -/
Equiv.Perm.cycleFactors : {α : Type u_2} →
  [Fintype α] →
    [LinearOrder α] →
      (f : Equiv.Perm α) → { l // l.prod = f ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Equiv.Perm.Disjoint l }
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instBot : {α : Type u_1} → Bot (MeasureTheory.OuterMeasure α)
-- Lean.Meta.Tactic.Simp.Simproc
/-- Builtin simprocs.  -/
Lean.Meta.Simp.builtinSimprocsRef : IO.Ref Lean.Meta.Simprocs
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [inst_21 : IsScalarTower R₁ B L] [IsScalarTower R₂ B L]
  [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂]
  [Module.IsTorsionFree R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [inst_28 : IsScalarTower A R₂ ↥F₂]
  [inst_29 : IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂]
  [Algebra.IsSeparable (↥F₁) L] [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B] [inst_35 : IsDedekindDomain R₁]
  [inst_36 : IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂]
  [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [Module.IsTorsionFree R₁ B] [Module.IsTorsionFree R₂ B], ⋯
-- Mathlib.Order.WellFounded
WellFounded.mono : ∀ {α : Type u_1} {r r' : α → α → Prop}, WellFounded r → (∀ (a b : α), r' a b → r a b) → WellFounded r'
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.mono_nonneg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [inst_1 : Lattice β] [HasSolidNorm β] [AddLeftMono β] {f g : α → β},
  MeasureTheory.HasFiniteIntegral g μ →
    (∀ᵐ (a : α) ∂μ, 0 ≤ f a) → (∀ᵐ (a : α) ∂μ, f a ≤ g a) → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.IsStandardOpenImmersion.holdsForLocalizationAway : RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardOpenImmersion
-- Init.Classical
/-- Extract an element from an existential statement, using `Classical.choose`.  -/
Exists.choose : {α : Sort u_1} → {p : α → Prop} → (∃ a, p a) → α
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.closure_nsmul : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {n : ℕ},
  0 ∈ s → n ≠ 0 → AddSubgroup.closure (n • s) = AddSubgroup.closure s
-- Lean.Meta.DecLevel
Lean.Meta.DecLevelContext.mk.injEq : ∀ (canAssignMVars canAssignMVars_1 : Bool),
  ({ canAssignMVars := canAssignMVars } = { canAssignMVars := canAssignMVars_1 }) = (canAssignMVars = canAssignMVars_1)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.addConst_k_eq_addConst : ∀ (p : Int.Internal.Linear.Poly) (k : ℤ), p.addConst_k k = p.addConst k
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun_pure : ∀ {m : Type w → Type w'} {α : Type u} {β : Type w} [inst : Monad m] [LawfulMonad m] {x : α}
  {f : (a : α) → (Std.Iterators.HetT.pure x).Property a → m β}, (Std.Iterators.HetT.pure x).prun f = f x ⋯
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_self : ∀ {p : ℕ}, 1 < p → p.maxPowDvdDiv p = (1, 1)
-- Mathlib.RingTheory.Valuation.Quotient
AddValuation.onQuot_comap_eq : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : AddValuation R Γ₀) {J : Ideal R} (hJ : J ≤ v.supp), AddValuation.comap (Ideal.Quotient.mk J) (v.onQuot hJ) = v
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueProds.instForall : ∀ {ι : Type u_2} (G : ι → Type u_1) [inst : (i : ι) → Mul (G i)] [∀ (i : ι), UniqueProds (G i)],
  UniqueProds ((i : ι) → G i)