mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.finiteArchimedeanClassOrderHomInvLex.eq_1 : ∀ (Γ : Type u_1) (R : Type u_2) [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R],
  HahnSeries.finiteArchimedeanClassOrderHomInvLex Γ R =
    {
      toFun := fun x =>
        (FiniteArchimedeanClass.liftOrderHom
            (fun a => FiniteArchimedeanClass.mk (toLex ((HahnSeries.single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2,
      monotone' := ⋯ }
-- Mathlib.Data.Real.Basic
Real.instMonoid : Monoid ℝ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.getVert_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} {p : G.Walk u v}, n < p.length → p.dropLast.getVert n = p.getVert n
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent.eq_1 : ∀ (G : Type u) [inst : AddMonoid G], AddMonoid.exponent G = if h : AddMonoid.ExponentExists G then Nat.find h else 0
-- Init.Data.List.Attach
List.attach_eq_nil_iff : ∀ {α : Type u_1} {l : List α}, l.attach = [] ↔ l = []
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.mk' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (e : α → β),
  Continuous e →
    DenseRange e →
      Function.Injective e →
        (∀ (a : α), ∀ s ∈ nhds a, ∃ t ∈ nhds (e a), ∀ (b : α), e b ∈ t → b ∈ s) → IsDenseEmbedding e
-- Mathlib.Data.Matrix.Mul
zero_dotProduct : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] (v : m → α), 0 ⬝ᵥ v = 0
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasFDerivWithinAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {f' : E →L[𝕜] ℂ} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Complex.exp (f x)) (Complex.exp (f x) • f') s x
-- Std.Data.DTreeMap.Internal.Operations
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.modify : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] → (k : α) → (β k → β k) → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_roc_eq_zero : ∀ {m n i : ℕ}, n ≤ i + m → (m<...=n).toArray[i]! = 0
-- Mathlib.Combinatorics.Matroid.Constructions
/-- The matroid on `E` whose unique base is the subset `I` of `E`.
Intended for use when `I ⊆ E`; if this is not the case, then the base is `I ∩ E`.  -/
Matroid.uniqueBaseOn : {α : Type u_1} → Set α → Set α → Matroid α
-- Mathlib.GroupTheory.Congruence.BigOperators
Con.dfinsuppProd : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : CommMonoid M]
  [inst_2 : (i : ι) → Zero (β i)] [inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : Con M)
  (h h' : (i : ι) → β i → M) {f g : Π₀ (i : ι), β i},
  (∀ (i : ι), c (h i 0) 1) →
    (∀ (i : ι), c (h' i 0) 1) → (∀ (i : ι), c (h i (f i)) (h' i (g i))) → c (f.prod h) (g.prod h')
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.mk.injEq : ∀ (name url cmd : String) (query : String → ℕ → Lean.MetaM (Array LeanSearchClient.SearchResult))
  (queryNum : Lean.CoreM ℕ) (name_1 url_1 cmd_1 : String)
  (query_1 : String → ℕ → Lean.MetaM (Array LeanSearchClient.SearchResult)) (queryNum_1 : Lean.CoreM ℕ),
  ({ name := name, url := url, cmd := cmd, query := query, queryNum := queryNum } =
      { name := name_1, url := url_1, cmd := cmd_1, query := query_1, queryNum := queryNum_1 }) =
    (name = name_1 ∧ url = url_1 ∧ cmd = cmd_1 ∧ query = query_1 ∧ queryNum = queryNum_1)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.mk.inj : ∀ {C : Type u₁} {ι : Type} {fintype : Fintype ι} {X : ι → C} {ι_1 : Type} {fintype_1 : Fintype ι_1} {X_1 : ι_1 → C},
  { ι := ι, fintype := fintype, X := X } = { ι := ι_1, fintype := fintype_1, X := X_1 } →
    ι = ι_1 ∧ fintype ≍ fintype_1 ∧ X ≍ X_1
-- Aesop.Search.Queue.Class
Aesop.Queue.addGoals : {Q : Type} → [self : Aesop.Queue Q] → Q → Array Aesop.GoalRef → BaseIO Q
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- The transvection associated with a linear form `f` and a vector `v` such that `f v = 0`.  -/
LinearEquiv.transvection : {R : Type u_1} →
  {V : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → {f : Module.Dual R V} → {v : V} → f v = 0 → V ≃ₗ[R] V
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.coe_smul : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] (f : H) (c : 𝕜), ⇑(c • f) = c • ⇑f
-- Lean.Level
Lean.Level.Data.hash : Lean.Level.Data → UInt64
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_associator_inv_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d : B × C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  (CategoryTheory.Bicategory.associator f g h).inv.2 = (CategoryTheory.Bicategory.associator f.2 g.2 h.2).inv
-- Lean.Widget.InteractiveGoal
Lean.Widget.instRpcEncodableInteractiveGoals : Lean.Server.RpcEncodable Lean.Widget.InteractiveGoals
-- Mathlib.RingTheory.RingHom.Locally
/-- For a property of ring homomorphisms `P`, `Locally P` holds for `f : R →+* S` if
it holds locally on `S`, i.e. if there exists a subset `{ t }` of `S` generating
the unit ideal, such that `P` holds for all compositions `R →+* Sₜ`.

We may require `s` to be finite here, for the equivalence, see `locally_iff_finite`.
 -/
RingHom.Locally : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.IsMinimal.val_Δ_maximal : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.IsMinimal R W],
  MaximalFor (fun C => WeierstrassCurve.IsIntegral R (C • W)) (fun C => WeierstrassCurve.valuation_Δ_aux R (C • W)) 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.keys_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 ⋯).impl.keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯))
        t.keys.attach).unattach
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mk.inj : ∀ {cells : Finset (ℕ × ℕ)} {isLowerSet : IsLowerSet ↑cells} {cells_1 : Finset (ℕ × ℕ)}
  {isLowerSet_1 : IsLowerSet ↑cells_1},
  { cells := cells, isLowerSet := isLowerSet } = { cells := cells_1, isLowerSet := isLowerSet_1 } → cells = cells_1
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- Auxiliary definition for `bifunctorComp₁₂Functor`.  -/
CategoryTheory.bifunctorComp₁₂FunctorObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [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} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂) →
                      CategoryTheory.Functor (CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
                        (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_eq_not_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey?.isSome = !t.isEmpty
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_iff_pairwiseDisjoint_range_smul : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X},
  MulAction.IsBlock G B ↔ (Set.range fun g => g • B).PairwiseDisjoint id
-- Mathlib.Order.Interval.Set.Pi
/-- If `x`, `y`, `z` are functions `Π i : ι, α i`, then
the set difference between the box `[x, z]` and the product of the intervals `(y i, z i]`
is covered by the union of the boxes `[x, update z i (y i)]`.

E.g., if `x = y`, then this lemma states that the difference between a closed box
`[x, y]` and the product of half-open intervals `{z | ∀ i, x i < z i ≤ y i}` is covered by the union
of the faces of `[x, y]` adjacent to `x`.  -/
Set.Icc_sdiff_pi_univ_Ioc_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → LinearOrder (α i)]
  (x y z : (i : ι) → α i),
  (Set.Icc x z \ Set.univ.pi fun i => Set.Ioc (y i) (z i)) ⊆ ⋃ i, Set.Icc x (Function.update z i (y i))
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.isPlausibleSuccessorOf_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] {it' it : Std.Iter α},
  it'.IsPlausibleSuccessorOf it ↔
    ∃ a,
      it.internalState.next = some a ∧
        a ≤ it.internalState.upperBound ∧
          Std.PRange.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound
-- Mathlib.Lean.Elab.InfoTree
/-- Returns the value of `f ctx info children` on the outermost `.node info children` which has
context, having merged and updated contexts appropriately.

If `ctx?` is `some ctx`, `ctx` is used as an initial context. A `ctx?` of `none` should **only** be
used when operating on the first node of the entire infotree. Otherwise, it is likely that no
context will be found.
 -/
Lean.Elab.InfoTree.onHighestNode? : {α : Type} →
  Lean.Elab.InfoTree →
    Option Lean.Elab.ContextInfo →
      (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → α) → Option α
-- Init.Data.String.Lemmas.Basic
_private.Init.Data.String.Lemmas.Basic.0.String.Slice.Pos.nextn.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- The forgetful (strict) pseudofunctor from an induced bicategory to the original bicategory,
forgetting the extra data.
 -/
CategoryTheory.Bicategory.InducedBicategory.forget : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} → CategoryTheory.StrictPseudofunctor (CategoryTheory.Bicategory.InducedBicategory C F) C
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X)
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        h)
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebraStruct.toBialgebra : {R : Type u} →
  {A : Type v} → {inst : CommSemiring R} → {inst_1 : Semiring A} → [self : HopfAlgebraStruct R A] → Bialgebra R A
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.IsOver.restrictTarget : ∀ {X Y S : AlgebraicGeometry.Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {f : X.PartialIso Y},
  AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY f →
    ∀ (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target),
      AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY (f.restrictTarget U hU hU')
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_algebraMap : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (S : Type u_3) [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (I : Ideal R),
  (Ideal.relNorm R) (Ideal.map (algebraMap R S) I) = I ^ Module.finrank R S
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (m.insertMany l).getKey! k = m.getKey! k
-- Mathlib.Algebra.Order.Hom.Basic
MulRingSeminormClass.toAddGroupSeminormClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : NonAssocRing α} {inst_1 : Semiring β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : MulRingSeminormClass F α β], AddGroupSeminormClass F α β
-- Init.Data.Iterators.Consumers.Loop
/-- Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldlM`.

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 `Iter.foldM`.
 -/
Std.Iter.Total.foldM : {m : Type x → Type x'} →
  [Monad m] →
    {α β : Type w} →
      {γ : Type x} →
        [inst : Std.Iterator α Id β] →
          [Std.IteratorLoop α Id m] → [Std.Iterators.Finite α Id] → (γ → β → m γ) → γ → Std.Iter.Total β → m γ
-- Init.Control.ExceptCps
ExceptCpsT.runK_lift : ∀ {m : Type u → Type u_1} {β α ε : Type u} [inst : Monad m] (x : m α) (s : ε) (ok : α → m β) (error : ε → m β),
  (ExceptCpsT.lift x).runK s ok error = x >>= ok
-- Mathlib.RingTheory.AdjoinRoot
/-- **Alias** of `AdjoinRoot.quotMapOfEquivQuotMapCMapMk_symm_mk`. -/
AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R) (x : AdjoinRoot f),
  (AdjoinRoot.quotMapOfEquivQuotMapCMapMk I f).symm
      ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) x
-- Mathlib.Topology.Algebra.Monoid
/-- If a submonoid of an additive topological monoid is commutative, then so is its
topological closure.

See note [reducible non-instances]  -/
AddSubsemigroup.addCommSemigroupTopologicalClosure : {M : Type u_3} →
  [inst : TopologicalSpace M] →
    [inst_1 : AddSemigroup M] →
      [inst_2 : SeparatelyContinuousAdd M] →
        [T2Space M] → (s : AddSubsemigroup M) → (∀ (x y : ↥s), x + y = y + x) → AddCommSemigroup ↥s.topologicalClosure
-- Mathlib.Algebra.Group.Hom.Defs
/-- Given an AddMonoid homomorphism `f : M →+ N` and an element `x : M`, if `x` has
a right inverse, then `f x` has a right inverse too.  -/
AddMonoidHom.map_exists_right_neg : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : FunLike F M N]
  [AddMonoidHomClass F M N] (f : F) {x : M}, (∃ y, x + y = 0) → ∃ y, f x + y = 0
-- Mathlib.SetTheory.Lists
Lists.Equiv.decidable : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : Lists α) → Decidable (l₁.Equiv l₂)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_11 : ∀ (k n : ℕ),
  ((Lean.Grind.CommRing.Expr.natCast n).pow k).toPoly =
    bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else Lean.Grind.CommRing.Poly.num (↑n ^ k)
-- Mathlib.Topology.Compactness.Compact
/-- Given a family of closed sets `t i` in a compact space, if they satisfy the Finite Intersection
Property, then the intersection of all `t i` is nonempty.
 -/
CompactSpace.iInter_nonempty : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type v} [CompactSpace X] {t : ι → Set X},
  (∀ (i : ι), IsClosed (t i)) → (∀ (s : Finset ι), (⋂ i ∈ s, t i).Nonempty) → (⋂ i, t i).Nonempty
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.const_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.SimplicialObject.Augmented.const.map f).right = f
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instPiObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Type v} (c : β → C)
  [inst_1 : CategoryTheory.Limits.HasProduct c] [∀ (b : β), CategoryTheory.Injective (c b)],
  CategoryTheory.Injective (∏ᶜ c)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.iff_eventually_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y),
  IsLocallyConstant f ↔ ∀ (x : X), ∀ᶠ (y : X) in nhds x, f y = f x
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The horn is a multicoequalizer of all `1`-codimensional faces of the
standard simplex but one along suitable `2`-codimensional faces.  -/
SSet.horn.isColimit : {n : ℕ} →
  (i : Fin (n + 1)) →
    CategoryTheory.Limits.IsColimit
      ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).toLinearOrder.map SSet.Subcomplex.toSSetFunctor)
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadAutoImplicits.mk : {m : Type → Type} → m (Array Lean.Expr) → Lean.Elab.MonadAutoImplicits m
-- Init.Data.List.Erase
List.erase_eq_eraseP : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) (l : List α), l.erase a = List.eraseP (fun x => a == x) l
-- Mathlib.GroupTheory.FixedPointFree
/-- A function `φ : G → G` is fixed-point-free if `1 : G` is the only fixed point of `φ`.  -/
MonoidHom.FixedPointFree : {G : Type u_2} → (G → G) → [One G] → Prop
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_dep_iff : ∀ {α : Type u_1} {M : Matroid α} {D X : Set α}, (M.delete D).Dep X ↔ M.Dep X ∧ Disjoint X D
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits.eq_2 : ∀ {α : Type u_1} [inst : Semiring α] (b : α) (h : ℕ) (t : List ℕ), Nat.ofDigits b (h :: t) = ↑h + b * Nat.ofDigits b t
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_coe_nnreal : ∀ {p : NNReal}, ENNReal.ofReal ↑p = ↑p
-- Std.Time.Date.Unit.Year
/-- Determines if a year is a leap year in the proleptic Gregorian calendar.
 -/
Std.Time.Year.Offset.isLeap : Std.Time.Year.Offset → Bool
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.fderivCLM_ofSupportedIn : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) (f : ContDiffMapSupportedIn E F n K),
  (TestFunction.fderivCLM 𝕜 n k) (TestFunction.ofSupportedIn K_sub_Ω f) =
    TestFunction.ofSupportedIn K_sub_Ω ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k) f)
-- Mathlib.RingTheory.EuclideanDomain
EuclideanDomain.gcd_isUnit_iff : ∀ {α : Type u_1} [inst : EuclideanDomain α] [inst_1 : DecidableEq α] {x y : α},
  IsUnit (EuclideanDomain.gcd x y) ↔ IsCoprime x y
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv : ∀ {p q n : ℕ}
  (z :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n })),
  z ∈
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
            (SSet.stdSimplex.obj { len := q })).nonDegenerate
        n ↔
    Function.Injective ⇑(SSet.prodStdSimplex.objEquiv z)
-- Lean.Elab.InfoTree.Main
Lean.Elab.DocInfo.format : Lean.Elab.ContextInfo → Lean.Elab.DocInfo → Std.Format
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k}, (cmp (t.insertIfNew k v).minKey! k).isLE = true
-- Mathlib.RepresentationTheory.Character
FDRep.char_mul_comm : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Monoid G] (V : FDRep k G) (g h : G),
  V.character (h * g) = V.character (g * h)
-- Init.Data.UInt.Lemmas
UInt8.toUInt8_toUInt32 : ∀ (n : UInt8), n.toUInt32.toUInt8 = n
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.coe_codRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂)
  (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p), ⇑(f.codRestrict p h) = Set.codRestrict (⇑f) (↑p) h
-- Init.Meta.Defs
/-- Evaluator for `prio` DSL  -/
Lean.evalPrio : Lean.Syntax → Lean.MacroM ℕ
-- Lean.Structure
/-- The name of the structure.  -/
Lean.StructureInfo.structName : Lean.StructureInfo → Lean.Name
-- Mathlib.Algebra.QuadraticDiscriminant
discrim_lt_zero_of_neg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a b c : K},
  a ≠ 0 → (∀ (x : K), a * (x * x) + b * x + c < 0) → discrim a b c < 0
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- The morphism `(A₁ ×_X A₂) ×_{A₁} (A₁ ×_X A₃) ⟶ A₃`.  -/
CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [inst_2 : F.Full] →
            {A₁ A₂ A₃ : C} →
              {X : D} →
                {f₁ : F.obj A₁ ⟶ X} →
                  (hf₁ : F.relativelyRepresentable f₁) →
                    (f₂ : F.obj A₂ ⟶ X) →
                      (f₃ : F.obj A₃ ⟶ X) →
                        [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] →
                          hf₁.pullback₃ f₂ f₃ ⟶ A₃
-- Mathlib.LinearAlgebra.Determinant
/-- Builds a linear equivalence from a linear map whose determinant in some bases is a unit.  -/
LinearEquiv.ofIsUnitDet : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {M' : Type u_3} →
            [inst_3 : AddCommGroup M'] →
              [inst_4 : Module R M'] →
                {ι : Type u_4} →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : Fintype ι] →
                      {f : M →ₗ[R] M'} →
                        {v : Module.Basis ι R M} →
                          {v' : Module.Basis ι R M'} → IsUnit ((LinearMap.toMatrix v v') f).det → M ≃ₗ[R] M'
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasDerivAt.hasGradientAt : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜}, HasDerivAt g g' u → HasGradientAt g ((starRingEnd 𝕜) g') u
-- Mathlib.Algebra.Free
FreeAddMagma.toFreeAddSemigroup_map : ∀ {α : Type u} {β : Type v} (f : α → β) (x : FreeAddMagma α),
  FreeAddMagma.toFreeAddSemigroup ((FreeAddMagma.map f) x) =
    (FreeAddSemigroup.map f) (FreeAddMagma.toFreeAddSemigroup x)