mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.evaluation_preservesColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.Limits.HasColimits C] (k : K),
  CategoryTheory.Limits.PreservesColimits ((CategoryTheory.evaluation K C).obj k)
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.coe_comapSubgroup : ∀ {G : Type u_1} [inst : Group G] {H : Type u_5} [inst_1 : Group H] (e : G ≃* H),
  ⇑e.comapSubgroup = Subgroup.comap e.toMonoidHom
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), s.IsPWO = s.PartiallyWellOrderedOn fun x1 x2 => x1 ≤ x2
-- Init.Data.List.Lemmas
List.eraseDupsBy.eq_1 : ∀ {α : Type u_1} (r : α → α → Bool) (as : List α), List.eraseDupsBy r as = List.eraseDupsBy.loop r as []
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple.eq_def : ∀ (x x_1 : ℕ),
  List.Nat.antidiagonalTuple x x_1 =
    match x, x_1 with
    | 0, 0 => [![]]
    | 0, n.succ => []
    | k.succ, n =>
      List.flatMap (fun ni => List.map (fun x => Fin.cons ni.1 x) (List.Nat.antidiagonalTuple k ni.2))
        (List.Nat.antidiagonal n)
-- Mathlib.ModelTheory.Syntax
/-- Relabels a bounded formula's free variables along a bijection.  -/
FirstOrder.Language.BoundedFormula.relabelEquiv : {L : FirstOrder.Language} →
  {α : Type u'} → {β : Type v'} → α ≃ β → {k : ℕ} → L.BoundedFormula α k ≃ L.BoundedFormula β k
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.Channel.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (inner : Std.CloseableChannel α), sizeOf { inner := inner } = 1 + sizeOf inner
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt16.size ≤ n → (UInt16.ofNatClamp n).toBitVec = (UInt16.size - 1)#'UInt16.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_tfae : ∀ {α : Type u_1} (M : Matroid α) (e : α),
  [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE
-- Mathlib.Topology.Compactness.Lindelof
/-- For every open cover of a Lindelöf set, there exists a countable subcover.  -/
IsLindelof.elim_countable_subcover_image : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X},
  IsLindelof s → (∀ i ∈ b, IsOpen (c i)) → s ⊆ ⋃ i ∈ b, c i → ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
-- Mathlib.Analysis.Normed.Module.HahnBanach
/-- Corollary of Hahn-Banach. Given an element `x` of a normed space with `‖x‖ ≠ 0`, there
exists an element of the dual space, of norm `1`, whose value on `x` is `‖x‖`.  -/
exists_dual_vector : ∀ (𝕜 : Type v) [inst : RCLike 𝕜] {E : Type u} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (x : E),
  ‖x‖ ≠ 0 → ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖
-- ImportGraph.Tools.RedundantImports
/-- List the imports in this file which can be removed
because they are transitively implied by another import.
 -/
«command#redundant_imports» : Lean.ParserDescr
-- Mathlib.Data.Multiset.ZeroCons
Multiset.eq_zero_of_forall_notMem : ∀ {α : Type u_1} {s : Multiset α}, (∀ (x : α), x ∉ s) → s = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getGT!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.Equiv t₂ → t₁.getGT! k = t₂.getGT! k
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_dvd_card : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), H.relIndex K ∣ Nat.card ↥K
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.contDiff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {n : ℕ∞}, ContDiff ℝ ↑n ↑f
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j)
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j))
      (CategoryTheory.Limits.pullback.snd s.fst (𝒰.f j))
-- Batteries.Data.String.Legacy
String.Pos.Raw.utf8GetAux.eq_1 : ∀ (x x_1 : String.Pos.Raw), String.Pos.Raw.utf8GetAux [] x x_1 = default
-- Std.Time.Format.Modifier
/-- Extended year format for more than 4 digits (e.g., "002023")
 -/
Std.Time.Year.extended : ℕ → Std.Time.Year
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.zeroLocus_vanishingIdeal_le : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  (V : Set (σ → K)), V ⊆ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal k V)
-- Mathlib.Order.Filter.Defs
/-- `IsCobounded (≺) f` states that the filter `f` does not tend to infinity w.r.t. `≺`. This is
also called frequently bounded. Will be usually instantiated with `≤` or `≥`.

There is a subtlety in this definition: we want `f.IsCobounded` to hold for any `f` in the case of
complete lattices. This will be relevant to deduce theorems on complete lattices from their
versions on conditionally complete lattices with additional assumptions. We have to be careful in
the edge case of the trivial filter containing the empty set: the other natural definition
  `¬ ∀ a, ∀ᶠ n in f, a ≤ n`
would not work as well in this case.
 -/
Filter.IsCobounded : {α : Type u_1} → (α → α → Prop) → Filter α → Prop
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.CancelParams.mk.injEq : ∀ (id id_1 : Lean.JsonRpc.RequestID), ({ id := id } = { id := id_1 }) = (id = id_1)
-- Init.Data.UInt.Lemmas
UInt8.neg_ne_zero : ∀ {a : UInt8}, -a ≠ 0 ↔ a ≠ 0
-- Std.Http.Data.URI.Basic
/-- Finds the first value of a query parameter by raw key string. The key is percent-encoded before
matching. This avoids aliasing between raw and pre-encoded spellings.
 -/
Std.Http.URI.Query.find? : Std.Http.URI.Query → String → Option (Option Std.Http.URI.EncodedQueryParam)
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given an element `x : A`, there is a natural morphism of representations `k[G] ⟶ A` sending
`g ↦ A.ρ(g)(x).`  -/
Rep.leftRegularHom : {k : Type u} →
  {G : Type v} → [inst : Ring k] → [inst_1 : Monoid G] → (A : Rep.{max u v, u, v} k G) → ↑A → (Rep.leftRegular k G ⟶ A)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_comp_addEquiv : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {P : Type u_8} [inst_2 : AddZeroClass P]
  (g : N →+ P) (iso : G ≃+ N), (g.comp ↑iso).ker = AddSubgroup.map (↑iso.symm) g.ker
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.ofIso_toColimitPresentation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) {Y : C} (e : X ≅ Y),
  (h.ofIso e).toColimitPresentation = h.ofIso e
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.not_vlt_of_veq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → ¬x <ᵥ y
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.snd_hom_hom : ∀ {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.SemiCartesianMonoidalCategory.snd G H).hom.hom =
    CategoryTheory.SemiCartesianMonoidalCategory.snd G.X H.X
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
NonUnitalClosedEmbeddingContinuousFunctionalCalculus.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (p p_1 : A → Prop),
  p = p_1 →
    ∀ [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R] [inst_3 : MetricSpace R]
      [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A] [inst_7 : StarRing A]
      [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
      [inst_11 : SMulCommClass R A A],
      NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p =
        NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.all_prop_eq : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String}, s.all P = s.toList.all fun x => decide (P x)
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.mk.injEq : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (val : A) (isGroupLikeElem_val : IsGroupLikeElem R val) (val_1 : A)
  (isGroupLikeElem_val_1 : IsGroupLikeElem R val_1),
  ({ val := val, isGroupLikeElem_val := isGroupLikeElem_val } =
      { val := val_1, isGroupLikeElem_val := isGroupLikeElem_val_1 }) =
    (val = val_1)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ElabHeaderResult.mk.sizeOf_spec : ∀ (toPreElabHeaderResult : Lean.Elab.Command.PreElabHeaderResult) (indFVar : Lean.Expr),
  sizeOf { toPreElabHeaderResult := toPreElabHeaderResult, indFVar := indFVar } =
    1 + sizeOf toPreElabHeaderResult + sizeOf indFVar
-- Mathlib.ModelTheory.Basic
/-- A first-order equivalence is also a first-order homomorphism.  -/
FirstOrder.Language.Equiv.toHom : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Equiv M N → L.Hom M N
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_dvd_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c : α}, lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
-- Batteries.Classes.Order
/-- Class for types where the ordering function is compatible with the `LT`.  -/
Std.LawfulLTOrd : (α : Type u_1) → [LT α] → [Ord α] → Prop
-- Lean.Meta.Constructions.SparseCasesOnEq
/-- Given a sparseCasesOn, creates an equational theorem for the else-case.
 -/
Lean.Meta.getSparseCasesOnEq : Lean.Name → Lean.MetaM Lean.Name
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_leftUnitor_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  Bicategory.Opposite.op2 (CategoryTheory.Bicategory.leftUnitor f).hom =
    (CategoryTheory.Bicategory.rightUnitor f.op).hom
-- Mathlib.Logic.Encodable.Basic
/-- Explicit decoding function for `Sigma γ`  -/
Encodable.decodeSigma : {α : Type u_1} → {γ : α → Type u_3} → [Encodable α] → [(a : α) → Encodable (γ a)] → ℕ → Option (Sigma γ)
-- Mathlib.Algebra.Order.AddTorsor
SMul.smul_lt_smul_of_le_of_lt : ∀ {G : Type u_1} {P : Type u_2} [inst : LE G] [inst_1 : Preorder P] [inst_2 : SMul G P] [IsOrderedCancelSMul G P]
  {a b : G} {c d : P}, a ≤ b → c < d → a • c < b • d
-- Mathlib.Topology.Covering.Basic
/-- If `f : E → X` is a continuous map between Hausdorff spaces with `E` compact, `s` is a subset
of `X` such that `f` restricts to a homeomorphism on a neighborhood of every point of `f ⁻¹' s`,
then `f` is a covering map on `s`.

For example, `s` can be taken to be the set of regular values of a C¹ map `f : E → X`
where `E` and `X` are manifolds of the same dimension with `E` compact, according to
the inverse function theorem (see `ContDiffAt.toOpenPartialHomeomorph`).  -/
IsCoveringMapOn.of_isLocalHomeomorphOn : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X}
  [T2Space E] [T2Space X] [CompactSpace E], Continuous f → IsLocalHomeomorphOn f (f ⁻¹' s) → IsCoveringMapOn f s
-- Lean.Expr
Lean.Int.mkInstNatCast : Lean.Expr
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.lift_comp_mk' : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M)
  (HN : N ≤ φ.ker), (QuotientGroup.lift N φ HN).comp (QuotientGroup.mk' N) = φ
-- Mathlib.Analysis.Complex.Norm
Complex.abs_re_le_norm : ∀ (z : ℂ), |z.re| ≤ ‖z‖
-- Init.Data.List.Lemmas
List.any_flatMap : ∀ {α : Type u_1} {β : Type u_2} {p : β → Bool} {l : List α} {f : α → List β},
  (List.flatMap f l).any p = l.any fun a => (f a).any p
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ofNatIsoRight_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : H ⊣ F) (iso : F ≅ G),
  (adj.ofNatIsoRight iso).counit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight iso.inv H) adj.counit
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- When `F ⊣ G`,
the functor associating to each `X` the cones over `K` with cone point `F.op.obj X`
is naturally isomorphic to
the functor associating to each `X` the cones over `K ⋙ G` with cone point `X`.
 -/
CategoryTheory.Adjunction.conesIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₀, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₀, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  {K : CategoryTheory.Functor J D} →
                    F.op.comp ((CategoryTheory.cones J D).obj K) ≅ (CategoryTheory.cones J C).obj (K.comp G)
-- Mathlib.Tactic.ExtractGoal
/-- Have `extract_goal` extract the full local context.  -/
Mathlib.Tactic.ExtractGoal.star : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (t.insertMany l).contains k = (t.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.cellsOfRowLens.eq_2 : ∀ (w : ℕ) (ws : List ℕ),
  YoungDiagram.cellsOfRowLens (w :: ws) =
    {0} ×ˢ Finset.range w ∪
      Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ))
        (YoungDiagram.cellsOfRowLens ws)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_filter_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : (a : α) → β a → Bool}, (Std.ExtDHashMap.filter f m).size ≤ m.size
-- Mathlib.RingTheory.Etale.Descent
_private.Mathlib.RingTheory.Etale.Descent.0.Algebra.FormallySmooth.of_formallySmooth_tensorProduct_of_faithfullyFlat : {R : Type u_4} →
  {S : Type u_5} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_6) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [Module.FaithfullyFlat R T] →
                  [Algebra.FormallySmooth T (TensorProduct R T S)] → ProofWanted (Algebra.FormallySmooth R S)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.rfind.eq_1 : ∀ (f : Turing.ToPartrec.Code),
  f.rfind =
    Turing.ToPartrec.Code.pred.comp
      ((f.cons (Turing.ToPartrec.Code.succ.cons Turing.ToPartrec.Code.tail)).fix.comp Turing.ToPartrec.Code.zero')
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.Nondegenerate.eq_1 : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M), B.Nondegenerate = (B.SeparatingLeft ∧ B.SeparatingRight)
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.bijective_algebraMap_quotient : ∀ (k : Type u_1) {R : Type u_2} [inst : Field k] [inst_1 : CommRing R] [inst_2 : Algebra k R]
  [Algebra.IsFiniteSplit k R] (p : Ideal R) [p.IsPrime], Function.Bijective ⇑(algebraMap k (R ⧸ p))
-- Mathlib.Algebra.Group.Center
IsMulCentral.mid_assoc : ∀ {M : Type u_1} [inst : Mul M] {z : M}, IsMulCentral z → ∀ (a c : M), a * z * c = a * (z * c)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.injective_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (self : c.Embedding c'),
  Function.Injective self.f
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.ιMulti_family.eq_1 : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Type u_4}
  [inst_3 : LinearOrder I] (v : I → M) (s : ↑(Set.powersetCard I n)),
  exteriorPower.ιMulti_family R n v s = (exteriorPower.ιMulti R n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))
-- Mathlib.Data.Finset.Insert
Finset.insert_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ t → s ⊆ t → insert a s ⊆ t
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.automorphismGroup.toLinearMapMonoidHom_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (e : M ≃ₗ[R] M),
  LinearEquiv.automorphismGroup.toLinearMapMonoidHom e = ↑e
-- Init.Prelude
/-- Version of `Array.getInternal` that does not increment the reference count of its result.

This is only intended for direct use by the compiler.
 -/
Array.getInternalBorrowed : {α : Type u} → (a : Array α) → (i : ℕ) → i < a.size → α
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The top submodule is continuous linearly equivalent to the module.
This is the continuous version of `Submodule.topEquiv`.  -/
Submodule.topContEquiv : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : TopologicalSpace M] → ↥⊤ ≃L[R] M
-- Mathlib.Algebra.Homology.EulerCharacteristic
GradedObject.finrankSupport.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} (X : CategoryTheory.GradedObject ι (ModuleCat R)),
  GradedObject.finrankSupport X = Function.support fun i => Module.finrank R ↑(X i)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_eq_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k fallback : α}, k ∈ t → t.getD k fallback = k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  [hi : Inhabited (β k')] {f : β k → β k},
  (m.modify k f).get! k' =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).get! else m.get! k'
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle `c ↦ d ⊙ᵣ c` as a functor.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionLeft : (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] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory.MonoidalRightAction C D] → D → CategoryTheory.Functor C D
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.compLpL₂_apply_apply : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {𝕜 : Type u_6} [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 E]
  {F : Type u_8} {G : Type u_9} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fact (1 ≤ p)] (B : G →L[𝕜] E →L[𝕜] F) (g : G)
  (f : ↥(MeasureTheory.Lp E p μ)), ((ContinuousLinearMap.compLpL₂ p μ B) g) f = (B g).compLp f
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_le_map_iff_of_injective : ∀ {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.Injective ⇑f → ∀ {S T : Submonoid M}, Submonoid.map f S ≤ Submonoid.map f T ↔ S ≤ T
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.mk'.eq_1 : ∀ {M : Type u_4} {G : Type u_7} [inst : Group G] [inst_1 : MulOneClass M] (f : M → G)
  (map_mul : ∀ (a b : M), f (a * b) = f a * f b),
  MonoidHom.mk' f map_mul = { toFun := f, map_one' := ⋯, map_mul' := map_mul }
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.coe_lcs_range_toEnd_eq : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (k : ℕ),
  ↑(LieModule.lowerCentralSeries R (↥(LieModule.toEnd R L M).range) M k) = ↑(LieModule.lowerCentralSeries R L M k)
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The "additive circle": `𝕜 ⧸ ℤ ∙ p`. See also `Circle` and `Real.Angle`.  -/
AddCircle : {𝕜 : Type u_1} → [AddCommGroup 𝕜] → 𝕜 → Type u_1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x - a) '' Set.Iic b = Set.Iic (b - a)
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ico_Ici_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Ici a)) (Filter.principal (Set.Ici a))
-- Std.Data.DHashMap.RawDef
/-- Support for the `for` loop construct in `do` blocks.  -/
Std.DHashMap.Raw.forIn : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type w'} → [Monad m] → ((a : α) → β a → δ → m (ForInStep δ)) → δ → Std.DHashMap.Raw α β → m δ
-- Mathlib.Topology.Algebra.Ring.Basic
Subring.topologicalClosure_minimal : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [inst_2 : IsSemitopologicalRing R] (s : Subring R)
  {t : Subring R}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.Order.SuccPred.Basic
/-- `SuccOrder` transfers across equivalences between orders.  -/
SuccOrder.ofOrderIso : {X : Type u_3} → {Y : Type u_4} → [inst : Preorder X] → [inst_1 : Preorder Y] → [SuccOrder X] → X ≃o Y → SuccOrder Y
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.GridLines.T.congr_simp : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)]
  (μ μ_1 : (i : ι) → MeasureTheory.Measure (A i)),
  μ = μ_1 →
    ∀ {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι] (p p_1 : ℝ),
      p = p_1 →
        ∀ (f f_1 : ((i : ι) → A i) → ENNReal),
          f = f_1 →
            ∀ (s s_1 : Finset ι),
              s = s_1 →
                ∀ (a a_1 : (i : ι) → A i),
                  a = a_1 → MeasureTheory.GridLines.T μ p f s a = MeasureTheory.GridLines.T μ_1 p_1 f_1 s_1 a_1
-- Mathlib.Order.UpperLower.Closure
UpperSet.coe_erase : ∀ {α : Type u_1} [inst : Preorder α] (s : UpperSet α) (a : α), ↑(s.erase a) = ↑s \ ↑(LowerSet.Iic a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.head?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : Min α]
  [inst_1 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.WF → t.keys.head? = t.minKey?
-- Mathlib.Tactic.Translate.GuessName
/-- Replaces characters in `s` by lower-casing the first characters until a non-upper-case character
is found.  -/
Mathlib.Tactic.GuessName.String.decapitalizeSeq : String → optParam String.Pos.Raw 0 → String
-- Init.Classical
/-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`.  -/
Exists.choose_spec : ∀ {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a), p P.choose