mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mkIso_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.AddGrp C} (e : G.X ≅ H.X)
  (zero_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero)
      CategoryTheory.AddGrp.mkIso._auto_1)
  (add_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
          CategoryTheory.AddMonObj.add)
      CategoryTheory.AddGrp.mkIso._auto_3),
  (CategoryTheory.AddGrp.mkIso e zero_f add_f).inv.hom.hom = e.inv
-- Mathlib.Data.Finsupp.Multiset
/-- The `n`th symmetric power of a finite type `α` is naturally equivalent to the subtype of maps
`α → ℕ` with total mass `n`.

See also `Sym.equivNatSum` when `α` is not necessarily finite.  -/
Sym.equivNatSumOfFintype : (α : Type u_1) → [DecidableEq α] → (n : ℕ) → [inst : Fintype α] → Sym α n ≃ { P // ∑ i, P i = n }
-- Mathlib.Data.Fintype.Pi
RelEmbedding.instFintype : {α : Type u_3} → {β : Type u_4} → [Fintype α] → [Fintype β] → {r : α → α → Prop} → {s : β → β → Prop} → Fintype (r ↪r s)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.id_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Functor.id C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
HasCompactSupport.toSchwartzMap.congr_simp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f f_1 : E → F} (e_f : f = f_1) (h₁ : HasCompactSupport f) (h₂ : ContDiff ℝ (↑⊤) f),
  h₁.toSchwartzMap h₂ = ⋯.toSchwartzMap ⋯
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.State.mk : Array Lean.Expr → Mathlib.Tactic.AtomM.State
-- Mathlib.Algebra.Field.Subfield.Defs
/-- `Subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is a
multiplicative submonoid and an additive subgroup. Note in particular that it shares the
same 0 and 1 as R.  -/
Subfield : (K : Type u) → [DivisionRing K] → Type u
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_eq_domRestrict_iff`. -/
Set.restrict_eq_restrict_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, s.domRestrict f₁ = s.domRestrict f₂ ↔ Set.EqOn f₁ f₂ s
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instGetElem?Mem : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → GetElem? (Std.TreeMap.Raw α β cmp) α β fun m a => a ∈ m
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.sub_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x y : K ⋊⁅ψ⁆ L),
  x - y = { left := x.left - y.left, right := x.right - y.right }
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.tensorObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj G H).X = CategoryTheory.MonoidalCategoryStruct.tensorObj G.X H.X
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsLocalMin.lineDeriv_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {f : E → ℝ} {a : E}, IsLocalMin f a → lineDeriv ℝ f a = 0
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.Method.dynamic : Aesop.ScriptGenerated.Method
-- Mathlib.Order.Defs.LinearOrder
instIsLinearOrder_mathlib : ∀ {α : Type u_1} [inst : LinearOrder α], Std.IsLinearOrder α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldr_eq_foldr_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {f : (a : α) → β a → δ → δ} {init : δ},
  Std.DTreeMap.Raw.foldr f init t = List.foldr (fun a b => f a.fst a.snd b) init t.toList
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- A valuation subring of a field `K` is a subring `A` such that for every `x : K`,
either `x ∈ A` or `x⁻¹ ∈ A`.

This is equivalent to being maximal in the domination order
of local subrings (the stacks project definition). See `LocalSubring.isMax_iff`.
 -/
ValuationSubring : (K : Type u) → [Field K] → Type u
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_fun_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F],
  DifferentiableAt 𝕜 f x → ∀ (c : R), fderiv 𝕜 (fun y => c • f y) x = c • fderiv 𝕜 f x
-- Init.Data.SInt.Bitwise
UInt32.toInt32_not : ∀ (a : UInt32), (~~~a).toInt32 = ~~~a.toInt32
-- Mathlib.Order.PiLex
Pi.apply_le_of_toColex : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x y : (i : ι) → β i} {i : ι}
  [inst_1 : (i : ι) → LinearOrder (β i)], toColex x ≤ toColex y → (∀ j > i, x j = y j) → x i ≤ y i
-- Init.Data.List.Sublist
List.Sublist.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length ≤ l₂.length
-- Std.Do.WP.Basic
_private.Std.Do.WP.Basic.0.Std.Do.EStateM.instWP.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → motive (EStateM.Result.ok a s')) →
        ((e : ε) → (s' : σ) → motive (EStateM.Result.error e s')) → motive x
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.realFundSystem.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (i : Fin (NumberField.Units.rank K)),
  NumberField.IsCMField.realFundSystem K i =
    (Units.map
        ↑(algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)) (NumberField.RingOfIntegers K)))
      (NumberField.Units.fundSystem (↥(NumberField.maximalRealSubfield K)) ((finCongr ⋯) i))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokens.mk.inj : ∀ {resultId? : Option String} {data : Array ℕ} {resultId?_1 : Option String} {data_1 : Array ℕ},
  { resultId? := resultId?, data := data } = { resultId? := resultId?_1, data := data_1 } →
    resultId? = resultId?_1 ∧ data = data_1
-- Mathlib.Topology.WithTopology
/-- If `X` is equipped with topology `t`, the map `WithTopology X t → X` is continuous.  -/
WithTopology.continuous_ofTopology : ∀ {X : Type u_1} (t : TopologicalSpace X), Continuous WithTopology.ofTopology
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.repr_apply_coe : ∀ {ι : Type u_1} {G : Type u_3} [inst : Group G] (b : FreeGroupBasis ι G) (i : ι), b.repr (b i) = FreeGroup.of i
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.card_algHom_adjoin_integral : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E} {K : Type u}
  [inst_3 : Field K] [inst_4 : Algebra F K],
  IsIntegral F α →
    IsSeparable F α →
      (Polynomial.map (algebraMap F K) (minpoly F α)).Splits → Nat.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_iff_isCompact_closure_image_ball : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  [T2Space M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) {r : ℝ},
  0 < r → (IsCompactOperator ⇑f ↔ IsCompact (closure (⇑f '' Metric.ball 0 r)))
-- Mathlib.Algebra.Homology.Bifunctor
/-- The inclusion of a summand of `(mapBifunctor K₁ K₂ F c).X j`, or zero.  -/
HomologicalComplex.ιMapBifunctorOrZero : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            (K₁ : HomologicalComplex C₁ c₁) →
                              (K₂ : HomologicalComplex C₂ c₂) →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [inst_9 : K₁.HasMapBifunctor K₂ F c] →
                                            [inst_10 : DecidableEq J] →
                                              (i₁ : I₁) →
                                                (i₂ : I₂) →
                                                  (j : J) →
                                                    (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X j
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotientTensorEquiv_apply_tmul_mk : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (m : Submodule R M) (x : M) (y : N),
  (TensorProduct.quotientTensorEquiv N m) (Submodule.Quotient.mk x ⊗ₜ[R] y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
-- Init.Data.List.Lemmas
/-- This differs from `getElem?_set` by monadically mapping `Function.const _ a`
over the `Option` returned by `l[j]`?  -/
List.getElem?_set' : ∀ {α : Type u_1} {l : List α} {i j : ℕ} {a : α}, (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.IsDiscrete.eq_of_hom : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.IsDiscrete C] {X Y : C}
  (f : X ⟶ Y), X = Y
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.subset_of_forall_subset : ∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s t_1 : Set α},
  TopologicalSpace.IsTopologicalBasis B → IsOpen s → (∀ U ∈ B, U ⊆ s → U ⊆ t_1) → s ⊆ t_1
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.liftTruncLT_ι : ∀ {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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
  [inst_6 : t.IsLE X n₀], CategoryTheory.CategoryStruct.comp (t.liftTruncLT f n₀ n₁ h) ((t.truncLTι n₁).app Y) = f
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.of_coe : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [LindelofSpace ↑s], IsLindelof s
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rio α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Rio α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Lean.Server.InfoUtils
/-- For every branch of the `InfoTree`, find the deepest node in that branch for which `p` returns
`some _`  and return the union of all such nodes. The visitor `p` is given a node together with
its innermost surrounding `ContextInfo`.  -/
Lean.Elab.InfoTree.deepestNodesM : {m : Type → Type u_1} →
  {α : Type} →
    [Monad m] →
      (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m (Option α)) →
        Lean.Elab.InfoTree → m (List α)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  ↑I.support ∩ ↑↑U = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁ : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCompIso G).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₁))
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.isOpen_ball`.

---

For any valuation `v` compatible with the valuative relation on `R`, the open `r`-ball
around zero `{x | v.restrict x < r}` is open in the valuative topology.  -/
IsValuativeTopology.isOpen_ball : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  (r : (MonoidWithZeroHom.ofClass v).ValueGroup₀), IsOpen {x | v.restrict x < r}
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instModule : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [inst_13 : VectorBundle 𝕜 F V] → Module 𝕜 (ContMDiffSection I F n V)
-- Init.Data.Int.Lemmas
Int.add_sub_assoc : ∀ (a b c : ℤ), a + b - c = a + (b - c)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity []) =
    Std.DHashMap.Internal.Raw₀.emptyWithCapacity
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.rowLen_transpose : ∀ (μ : YoungDiagram) (i : ℕ), μ.transpose.rowLen i = μ.colLen i
-- Mathlib.RingTheory.WittVector.Teichmuller
/-- The underlying function of the monoid hom `WittVector.teichmuller`.
The `0`-th coefficient of `teichmullerFun p r` is `r`, and all others are `0`.
 -/
WittVector.teichmullerFun : (p : ℕ) → {R : Type u_1} → [CommRing R] → R → WittVector p R
-- Std.Time.Duration
Std.Time.Duration.instCoeOffset_5 : Coe Std.Time.Day.Offset Std.Time.Duration
-- Batteries.Data.Array.Basic
/-- Find the first maximal element of an array. If the array is empty, `none` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.rangeMax? : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → optParam ℕ 0 → optParam ℕ xs.size → Option α
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instSetLike : {α : Type u_2} → [inst : TopologicalSpace α] → SetLike (TopologicalSpace.Opens α) α
-- Mathlib.Tactic.Translate.Reorder
_private.Mathlib.Tactic.Translate.Reorder.0.List.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.RingTheory.Polynomial.UniqueFactorization
/-- If `D` is a unique factorization domain, `f` is a non-zero polynomial in `D[X]`, then `f` has
only finitely many monic factors.
(Note that its factors up to unit may be more than monic factors.)
See also `UniqueFactorizationMonoid.fintypeSubtypeDvd`.  -/
Polynomial.fintypeSubtypeMonicDvd : {D : Type u} →
  [inst : CommRing D] → [UniqueFactorizationMonoid D] → (f : Polynomial D) → f ≠ 0 → Fintype { g // g.Monic ∧ g ∣ f }
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- Together `Matrix.detInvertibleOfInvertible` and `Matrix.invertibleOfDetInvertible` form an
equivalence, although both sides of the equiv are subsingleton anyway.  -/
Matrix.invertibleEquivDetInvertible : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A : Matrix n n α) → Invertible A ≃ Invertible A.det
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `map f p` maps a polynomial `p` across a ring hom `f`  -/
Polynomial.map : {R : Type u} → {S : Type v} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → Polynomial R → Polynomial S
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
CategoryTheory.LocalizerMorphism.Derives.isIso_of_isRightDerivedFunctor : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₂ : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  {F : CategoryTheory.Functor C₂ H},
  Φ.Derives F →
    ∀ [Φ.IsRightDerivabilityStructure] {L₂ : CategoryTheory.Functor C₂ D₂} [inst_5 : L₂.IsLocalization W₂]
      {RF : CategoryTheory.Functor D₂ H} (α : F ⟶ L₂.comp RF) (X₁ : C₁) [RF.IsRightDerivedFunctor α W₂],
      CategoryTheory.IsIso (α.app (Φ.functor.obj X₁))
-- Mathlib.Data.Set.NAry
Set.image2_nonempty_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
  (Set.image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces_of_odd_card_aut : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K],
  Odd (Nat.card Gal(K/k)) → IsUnramifiedAtInfinitePlaces k K
-- ImportGraph.Imports.RequiredModules
/-- Return the names of the modules in which constants used in the specified declaration were defined.

Note that this will *not* account for tactics and syntax used in the declaration,
so the results may not suffice as imports.
 -/
Lean.Name.requiredModules : Lean.Name → Lean.CoreM Lean.NameSet
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.toEquiv_mulLeft₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MeasurableSpace G₀] [inst_2 : MeasurableMul G₀] {g : G₀}
  (hg : g ≠ 0), (MeasurableEquiv.mulLeft₀ g hg).toEquiv = Equiv.mulLeft₀ g hg
-- ProofWidgets.Data.Html
ProofWidgets.Html.text.injEq : ∀ (a a_1 : String), (ProofWidgets.Html.text a = ProofWidgets.Html.text a_1) = (a = a_1)
-- Init.Try
/-- Helper internal tactic for implementing the tactic `try?` with parallel execution.  -/
Lean.Parser.Tactic.attemptAllPar : Lean.ParserDescr
-- Init.Data.String.Decode
ByteArray.exists_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {c : Char}, b.utf8DecodeChar? 0 = some c → ∃ l, b = (String.utf8EncodeChar c).toByteArray ++ l
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_forall_constGet?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], (∀ (k : α), t₁[k]? = t₂[k]?) → t₁.Equiv t₂
-- Mathlib.Data.Finset.Lattice.Fold
Finset.isLUB_sup' : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Finset α} (hs : s.Nonempty), IsLUB (↑s) (s.sup' hs id)
-- Mathlib.Topology.Closure
frontier_inter_subset : ∀ {X : Type u} [inst : TopologicalSpace X] (s t : Set X),
  frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.symm_trans_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : γ), (h₁.trans h₂).symm x = h₁.symm (h₂.symm x)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective : ∀ {X : AlgebraicGeometry.Scheme} {U : X.AffineZariskiSite}, Function.Surjective U.presieveOfSections
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic.0.Std.Tactic.BVDecide.Gate.toString.match_1.splitter : (motive : Std.Tactic.BVDecide.Gate → Sort u_1) →
  (x : Std.Tactic.BVDecide.Gate) →
    (Unit → motive Std.Tactic.BVDecide.Gate.and) →
      (Unit → motive Std.Tactic.BVDecide.Gate.xor) →
        (Unit → motive Std.Tactic.BVDecide.Gate.beq) → (Unit → motive Std.Tactic.BVDecide.Gate.or) → motive x
-- Lean.Language.Basic
/-- Helper class for projecting a heterogeneous hierarchy of snapshot classes to a homogeneous
representation.  -/
Lean.Language.ToSnapshotTree : Type → Type
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.instAdd : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              (x : Submonoid A) →
                [inst_3 : AddCommMonoid ι] →
                  [inst_4 : DecidableEq ι] → [GradedRing 𝒜] → Add (HomogeneousLocalization.NumDenSameDeg 𝒜 x)
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.rank_le_natTrailingDegree_charpoly_ad : ∀ (R : Type u_1) {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] (x : L) [Nontrivial R],
  LieAlgebra.rank R L ≤ (LinearMap.charpoly ((LieAlgebra.ad R L) x)).natTrailingDegree
-- Init.Data.List.Lemmas
List.set_set : ∀ {α : Type u_1} (a : α) {b : α} {l : List α} {i : ℕ}, (l.set i a).set i b = l.set i b
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsIsLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W.isLocal.IsClosedUnderIsomorphisms