mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Construct an isomorphism of additive group objects by giving an additive monoid
isomorphism between the underlying objects.  -/
CategoryTheory.AddGrp.mkIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : C} →
        (e : G ≅ H) →
          [inst_2 : CategoryTheory.AddGrpObj G] →
            [inst_3 : CategoryTheory.AddGrpObj H] →
              [CategoryTheory.IsAddMonHom e.hom] → { X := G, addGrp := inst_2 } ≅ { X := H, addGrp := inst_3 }
-- Mathlib.Data.Set.Opposite
Set.opEquiv_self_apply_coe : ∀ {α : Type u_1} (s : Set α) (x : ↑s.op), ↑(s.opEquiv_self x) = Opposite.unop ↑x
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] [inst_1 : TopologicalSpace α] {s : Set α} [Topology.IsScott α D],
  IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvalue_add'_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ ρ : R}, (ρ • LinearMap.id + f).HasEigenvalue μ ↔ f.HasEigenvalue (μ - ρ)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (h.iso m).inv.hom) (h.π m) =
    CategoryTheory.Subobject.pullbackπ (h.χ m) h.Ω₀
-- Mathlib.Data.Set.MemPartition
_private.Mathlib.Data.Set.MemPartition.0.memPartition.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Lean.Level
Lean.mkLevelIMax : Lean.Level → Lean.Level → Lean.Level
-- Mathlib.Logic.Equiv.Basic
Function.Injective.swap_apply : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β},
  Function.Injective f → ∀ (x y z : α), (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Array.map_unattach.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} → (motive : Subtype P → Sort u_2) → (x : Subtype P) → ((x : α) → (h : P x) → motive ⟨x, h⟩) → motive x
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- A morphism in the category `HomologyPretheory`.  -/
TopPair.HomologyPretheory.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          TopPair.HomologyPretheory C c → TopPair.HomologyPretheory C c → Type (max (max (u + 1) u_2) v_1)
-- Mathlib.Data.Nat.Init
Nat.pincerRecursion.eq_def : ∀ {P : ℕ → ℕ → Sort u_1} (Ha0 : (m : ℕ) → P m 0) (H0b : (n : ℕ) → P 0 n)
  (H : (x y : ℕ) → P x y.succ → P x.succ y → P x.succ y.succ) (x x_1 : ℕ),
  Nat.pincerRecursion Ha0 H0b H x x_1 =
    match x, x_1 with
    | m, 0 => Ha0 m
    | 0, n => H0b n
    | n.succ, n_1.succ => H n n_1 (Nat.pincerRecursion Ha0 H0b H n n_1.succ) (Nat.pincerRecursion Ha0 H0b H n.succ n_1)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isFractional_span_singleton : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [IsLocalization S P] (x : P), IsFractional S (R ∙ x)
-- Mathlib.RingTheory.Nilpotent.Basic
Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero : ∀ {R : Type u_1} {x y : R} [inst : Semiring R],
  Commute x y → ∀ {m n k : ℕ}, x ^ m = 0 → y ^ n = 0 → m + n ≤ k + 1 → (x + y) ^ k = 0
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt.0.USize.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option USize)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} [inst_1 : Inhabited (β k)] (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.get! k = (Option.filter (f k) (t.get? k)).get!
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.opt : {α : Type u_1} → [Lean.ToJson α] → String → Option α → List (String × Lean.Json)
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.instOneH1 : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} → {I : Type w'} → {U : I → C} → One (CategoryTheory.PresheafOfGroups.H1 G U)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.boundaries₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.boundaries₂ A = (ModuleCat.Hom.hom (groupHomology.d₃₂ A)).range
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_a : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S) (D : F.DescentDataAsCoalgebra fun x => f),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor.obj D).a =
    D.hom default default
-- Mathlib.Data.Fintype.Fin
/-- Given a "downward-closed" predicate `p` on `Fin n` (which could be spelt `Antitone p`),
then `p` holds for more than `j` elements iff it holds for `p` itself.
 -/
Fin.lt_card_filter_univ_iff_apply_of_imp : ∀ {n : ℕ} {j : Fin n} (p : Fin n → Prop) [inst : DecidablePred p],
  (∀ (i j : Fin n), j ≤ i → p i → p j) → (↑j < {i | p i}.card ↔ p j)
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.dvd_monomial_one_iff_exists : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {n : σ →₀ ℕ},
  p ∣ (MvPolynomial.monomial n) 1 ↔ ∃ m u, m ≤ n ∧ IsUnit u ∧ p = (MvPolynomial.monomial m) u
-- Mathlib.Algebra.Homology.DerivedCategory.KInjective
CochainComplex.quasiIso_iff_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℕ}
  [∀ (n : ℕ), CategoryTheory.Injective (K.X n)] [∀ (n : ℕ), CategoryTheory.Injective (L.X n)] (f : K ⟶ L),
  QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℕ) f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insert k v).getKey? k = some k
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_inf : ∀ {α : Type u_1} [inst : LE α] (s t : LowerSet α), (s ⊓ t).compl = s.compl ⊓ t.compl
-- Mathlib.FieldTheory.Finite.Basic
/-- The finite field `F` has even cardinality iff it has characteristic `2`.  -/
FiniteField.even_card_iff_char_two : ∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F], ringChar F = 2 ↔ Fintype.card F % 2 = 0
-- Std.Do.WP.SimpLemmas
OptionT.orElse.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type u} (x : OptionT m α) (y : Unit → OptionT m α),
  x.orElse y =
    OptionT.mk do
      let __do_lift ← x
      match __do_lift with
        | some a => pure (some a)
        | x => y ()
-- Aesop.Script.UScriptToSScript
Aesop.Script.instNonemptyStepTree : Nonempty Aesop.Script.StepTree
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.map_comp_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {U V W : Cᵒᵖ} (i : U ⟶ V) (j : V ⟶ W) (x : ↑(M.obj U)),
  (CategoryTheory.ConcreteCategory.hom (M.map (CategoryTheory.CategoryStruct.comp i j))) x =
    (CategoryTheory.ConcreteCategory.hom (M.map j)) ((CategoryTheory.ConcreteCategory.hom (M.map i)) x)
-- Mathlib.Order.InitialSeg
/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≺i s` is an initial
segment embedding whose range is `Set.Iio x` for some element `x`. If `β` is a well order, this is
equivalent to the embedding not being surjective.  -/
PrincipalSeg : {α : Type u_4} → {β : Type u_5} → (α → α → Prop) → (β → β → Prop) → Type (max u_4 u_5)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanQueryModuleResponse : Lean.FromJson Lean.Lsp.LeanQueryModuleResponse
-- Mathlib.Analysis.Analytic.Basic
/-- If a function `f` has a power series `p` around `x`, then the function `z ↦ f (z - y)` has the
same power series around `x + y`.  -/
HasFPowerSeriesOnBall.comp_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → ∀ (y : E), HasFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) r
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- Determinant of transvections, over a field.

See `LinearMap.Transvection.det` for the general result.  -/
_private.Mathlib.LinearAlgebra.Transvection.Basic.0.LinearMap.transvection.det_ofField : ∀ {K : Type u_3} {V : Type u_4} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (f : Module.Dual K V) (v : V), LinearMap.det (LinearMap.transvection f v) = 1 + f v
-- Batteries.Data.Nat.Lemmas
Nat.recAuxOn_succ : ∀ {motive : ℕ → Sort u_1} (zero : motive 0) (succ : (n : ℕ) → motive n → motive (n + 1)) (n : ℕ),
  Nat.recAuxOn (n + 1) zero succ = succ n (Nat.recAuxOn n zero succ)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- The head of a multiseries, i.e. the first two entries of the tuple returned by `destruct`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.head : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)
-- Mathlib.Tactic.ENatToNat
Mathlib.Tactic.ENatToNat.not_lt_top : ∀ (x : ℕ∞), ¬⊤ < x
-- Lean.Util.SCC
Lean.SCC.Data.lowlink? : Lean.SCC.Data → Option ℕ
-- Init.Data.List.Perm
List.Perm.insert : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) {l₁ l₂ : List α},
  l₁.Perm l₂ → (List.insert a l₁).Perm (List.insert a l₂)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.RightAdjointCommShift.iso_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [inst_5 : F.CommShift A] (X : D),
  (CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorCompIsoId C b a h).inv.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C a).map
          (adj.unit.app ((CategoryTheory.shiftFunctor C b).obj (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor C a).map
            (G.map
              ((CategoryTheory.Functor.commShiftIso F b).hom.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor C a).map
              (G.map
                ((CategoryTheory.shiftFunctor D b).map (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj X)))))
            ((CategoryTheory.shiftFunctor C a).map
              (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app X))))))
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.mk.inj : ∀ {G : Type u_6} {inst : Group G} {toFun : G → ℝ} {map_one' : toFun 1 = 0}
  {mul_le' : ∀ (x y : G), toFun (x * y) ≤ toFun x + toFun y} {inv' : ∀ (x : G), toFun x⁻¹ = toFun x} {toFun_1 : G → ℝ}
  {map_one'_1 : toFun_1 1 = 0} {mul_le'_1 : ∀ (x y : G), toFun_1 (x * y) ≤ toFun_1 x + toFun_1 y}
  {inv'_1 : ∀ (x : G), toFun_1 x⁻¹ = toFun_1 x},
  { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' } =
      { toFun := toFun_1, map_one' := map_one'_1, mul_le' := mul_le'_1, inv' := inv'_1 } →
    toFun = toFun_1
-- Batteries.Util.Cache
/-- Once-per-file cache.  -/
Batteries.Tactic.Cache : Type → Type
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.map_range : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] [inst_2 : NonAssocRing T]
  (g : S →+* T) (f : R →+* S), Subring.map g f.range = (g.comp f).range
-- Init.Data.Array.Basic
/-- Returns the index of the first element for which `p` returns `true`, or the size of the array if
there is no such element.

Examples:
* `#[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = 4`
* `#[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = 7`
 -/
Array.findIdx : {α : Type u} → (α → Bool) → Array α → ℕ
-- Mathlib.Topology.Defs.Induced
/-- We say that restrictions of the topology on `X` to sets from a family `S`
generates the original topology,
if either of the following equivalent conditions hold:

- a set which is relatively open in each `s ∈ S` is open;
- a set which is relatively closed in each `s ∈ S` is closed;
- for any topological space `Y`, a function `f : X → Y` is continuous
  provided that it is continuous on each `s ∈ S`.
 -/
Topology.IsCoherentWith : {X : Type u_1} → [tX : TopologicalSpace X] → Set (Set X) → Prop
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.edgeDensity_le_one : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s t : Finset α), G.edgeDensity s t ≤ 1
-- Mathlib.Algebra.Regular.Basic
/-- In an additive semigroup, the sum of add-right-regular elements is add-right-regular.  -/
IsAddRightRegular.add : ∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R},
  IsAddRightRegular a → IsAddRightRegular b → IsAddRightRegular (a + b)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.equivalence_counitIso : AddCommMonCat.equivalence.counitIso =
  CategoryTheory.Iso.refl
    ({ obj := fun X => AddCommMonCat.of (Additive ↑X),
          map := fun {X Y} f => AddCommMonCat.ofHom (MonoidHom.toAdditive (CommMonCat.Hom.hom f)),
          map_id := AddCommMonCat.equivalence._proof_3, map_comp := @AddCommMonCat.equivalence._proof_4 }.comp
      { obj := fun X => CommMonCat.of (Multiplicative ↑X),
        map := fun {X Y} f => CommMonCat.ofHom (AddMonoidHom.toMultiplicative (AddCommMonCat.Hom.hom f)),
        map_id := AddCommMonCat.equivalence._proof_1, map_comp := @AddCommMonCat.equivalence._proof_2 })
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The natural map from a nonsingular Jacobian point on a Weierstrass curve `W` to its
corresponding nonsingular point in affine coordinates.

If `hP` is the nonsingular condition underlying a nonsingular Jacobian point `P` on `W`, then
`toAffineLift ⟨hP⟩` is definitionally equivalent to `toAffine W P`.  -/
WeierstrassCurve.Jacobian.Point.toAffineLift : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Jacobian F} → W.Point → W.toAffine.Point
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonClientInfo : Lean.ToJson Lean.Lsp.ClientInfo
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply : ∀ (R S : CommRingCat) (p : PrimeSpectrum ↑R) [inst : Algebra ↑R ↑S] (x : ↑(CommRingCat.of ↑S)),
  (AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p) x =
    (((TopCat.Presheaf.pushforward CommRingCat
                  (AlgebraicGeometry.Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((AlgebraicGeometry.structureSheafInType ↑S ↑S).obj.obj
                (Opposite.op
                  ((TopologicalSpace.Opens.map
                        (AlgebraicGeometry.Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                    ⊤))))).hom'
        x)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries_isAscendingCentralSeries`.

---

The upper central series of a group is an ascending central series.  -/
upperCentralSeries_isAscendingCentralSeries : ∀ (G : Type u_1) [inst : Group G], Subgroup.IsAscendingCentralSeries (Subgroup.upperCentralSeries G)
-- Mathlib.Data.FunLike.Equiv
EquivLike.inv_injective : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β], Function.Injective EquivLike.inv
-- Init.Data.String.Basic
/-- Creates a `String` from a `String.Slice` by copying the bytes.  -/
String.Slice.copy : String.Slice → String
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- If the image of a morphism under a fully faithful functor in an isomorphism,
then the original morphisms is also an isomorphism.
 -/
CategoryTheory.isIso_of_fully_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (F.map f)],
  CategoryTheory.IsIso f
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.comp_apply : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [inst : SMul M X]
  {Y : Type u_6} [inst_1 : SMul N Y] {Z : Type u_7} [inst_2 : SMul P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y)
  [inst_3 : CompTriple φ ψ χ] (x : X), (g.comp f) x = g (f x)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubringClass.toNonUnitalSubsemiringClass : ∀ {S : Type u_1} {R : Type u} {inst : NonUnitalNonAssocRing R} {inst_1 : SetLike S R}
  [self : NonUnitalSubringClass S R], NonUnitalSubsemiringClass S R
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- Coroots written as functionals on the weight space.  -/
RootPairing.coroot' : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι → Module.Dual R M
-- Aesop.Tree.Data
Aesop.RappData.scriptSteps? : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Option (Array Aesop.Script.LazyStep)
-- Mathlib.Data.Set.Image
Set.preimage_inl_image_inr : ∀ {α : Type u_1} {β : Type u_2} (s : Set β), Sum.inl ⁻¹' Sum.inr '' s = ∅
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  (as : Std.DHashMap.Internal.AssocList α β) (init : δ) (f : (a : α) → β a → δ → m (ForInStep δ)),
  as.forInStep init f = Std.DHashMap.Internal.AssocList.forInStep.go✝ f as init
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Returns the smallest element in the heap, or `default` if the heap is empty.  -/
Batteries.BinomialHeap.headI : {α : Type u} → {le : α → α → Bool} → [Inhabited α] → Batteries.BinomialHeap α le → α
-- Mathlib.Data.Quot
Quotient.lift_surjective : ∀ {α : Sort u_3} {β : Sort u_4} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b),
  Function.Surjective f → Function.Surjective (Quotient.lift f h)
-- Lean.Elab.Command
Lean.Elab.Command.Context.mk.inj : ∀ {fileName : String} {fileMap : Lean.FileMap} {currRecDepth : ℕ} {cmdPos : String.Pos.Raw}
  {macroStack : Lean.Elab.MacroStack} {quotContext? : Option Lean.Name} {currMacroScope : Lean.MacroScope}
  {ref : Lean.Syntax} {snap? : Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot)}
  {cancelTk? : Option IO.CancelToken} {suppressElabErrors : Bool} {fileName_1 : String} {fileMap_1 : Lean.FileMap}
  {currRecDepth_1 : ℕ} {cmdPos_1 : String.Pos.Raw} {macroStack_1 : Lean.Elab.MacroStack}
  {quotContext?_1 : Option Lean.Name} {currMacroScope_1 : Lean.MacroScope} {ref_1 : Lean.Syntax}
  {snap?_1 : Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot)} {cancelTk?_1 : Option IO.CancelToken}
  {suppressElabErrors_1 : Bool},
  { fileName := fileName, fileMap := fileMap, currRecDepth := currRecDepth, cmdPos := cmdPos, macroStack := macroStack,
        quotContext? := quotContext?, currMacroScope := currMacroScope, ref := ref, snap? := snap?,
        cancelTk? := cancelTk?, suppressElabErrors := suppressElabErrors } =
      { fileName := fileName_1, fileMap := fileMap_1, currRecDepth := currRecDepth_1, cmdPos := cmdPos_1,
        macroStack := macroStack_1, quotContext? := quotContext?_1, currMacroScope := currMacroScope_1, ref := ref_1,
        snap? := snap?_1, cancelTk? := cancelTk?_1, suppressElabErrors := suppressElabErrors_1 } →
    fileName = fileName_1 ∧
      fileMap = fileMap_1 ∧
        currRecDepth = currRecDepth_1 ∧
          cmdPos = cmdPos_1 ∧
            macroStack = macroStack_1 ∧
              quotContext? = quotContext?_1 ∧
                currMacroScope = currMacroScope_1 ∧
                  ref = ref_1 ∧ snap? = snap?_1 ∧ cancelTk? = cancelTk?_1 ∧ suppressElabErrors = suppressElabErrors_1
-- Lean.Parser.Basic
Lean.Parser.identEq : Lean.Name → Lean.Parser.Parser
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coprod_inl_inr : ∀ {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},
  (Representation.IntertwiningMap.inl A ρ σ).comp (Representation.IntertwiningMap.fst A ρ σ) +
      (Representation.IntertwiningMap.inr A ρ σ).comp (Representation.IntertwiningMap.snd A ρ σ) =
    Representation.IntertwiningMap.id (ρ.prod σ)
-- Init.Data.List.Lemmas
/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result.  -/
List.flatten_reverse : ∀ {α : Type u_1} {L : List (List α)}, L.reverse.flatten = (List.map List.reverse L).flatten.reverse
-- Mathlib.Data.Finsupp.Order
Finsupp.support_monotone : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α],
  Monotone Finsupp.support
-- Lean.Data.Lsp.TextSync
Lean.Lsp.SaveOptions.mk : Bool → Lean.Lsp.SaveOptions
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.centerCongr_symm_apply_coe : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (e : G ≃* H) (s : ↥(Subsemigroup.center H)),
  ↑((Subgroup.centerCongr e).symm s) = e.symm ↑s
-- Init.Data.List.Impl
/-- Auxiliary for `intercalateTR`:
`intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)`  -/
_private.Init.Data.List.Impl.0.List.intercalateTR.go : {α : Type u_1} → Array α → List α → List (List α) → Array α → List α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey! k = t₁.getKey! k
-- Mathlib.LinearAlgebra.Dimension.Free
Module.Free.ChooseBasisIndex.congr_simp : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M], Module.Free.ChooseBasisIndex R M = Module.Free.ChooseBasisIndex R M