mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftMap.congr_simp : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y : C} {n : M}
  (f f_1 : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y),
  f = f_1 → ∀ (a a' : M) (ha' : n + a = a'), F.shiftMap f a a' ha' = F.shiftMap f_1 a a' ha'
-- Mathlib.Topology.Algebra.Semigroup
/-- Any nonempty compact Hausdorff additive semigroup where right-addition is continuous
contains an idempotent, i.e. an `m` such that `m + m = m`  -/
exists_idempotent_of_compact_t2_of_continuous_add_left : ∀ {M : Type u_1} [Nonempty M] [inst : AddSemigroup M] [inst_1 : TopologicalSpace M] [CompactSpace M] [T2Space M],
  (∀ (r : M), Continuous fun x => x + r) → ∃ m, m + m = m
-- Init.Data.BitVec.Lemmas
/-- This normalized a bitvec using `ofFin` to `ofNat`.
 -/
BitVec.ofFin_eq_ofNat : ∀ {w x : ℕ} {lt : x < 2 ^ w}, { toFin := ⟨x, lt⟩ } = BitVec.ofNat w x
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Linear isometry between continuous linear maps from `G` to `G'`
and continuous `1`-multilinear maps from `G` to `G'`.  -/
ContinuousMultilinearMap.ofSubsingletonₗᵢ : (𝕜 : Type u) →
  {ι : Type v} →
    (G : Type wG) →
      {G' : Type wG'} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup G] →
            [inst_2 : NormedSpace 𝕜 G] →
              [inst_3 : SeminormedAddCommGroup G'] →
                [inst_4 : NormedSpace 𝕜 G'] →
                  [inst_5 : Fintype ι] →
                    [Subsingleton ι] → ι → (G →L[𝕜] G') ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun x => G) G'
-- Mathlib.NumberTheory.Divisors
Nat.reverse_divisorsAntidiagonalList : ∀ (n : ℕ), n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList
-- Mathlib.CategoryTheory.Equivalence
/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
functor.  -/
CategoryTheory.Equivalence.invFunIdAssoc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (e : C ≌ D) → (F : CategoryTheory.Functor D E) → e.inverse.comp (e.functor.comp F) ≅ F
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Hom.ext' : ∀ {a b : SimplexCategory} (f g : a.Hom b), f.toOrderHom = g.toOrderHom → f = g
-- Mathlib.Tactic.Widget.StringDiagram
/-- Nodes in a string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.Node : Type
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit_zero : ∀ {M : Type u_1} [inst : AddMonoid M] (h : IsAddUnit 0), h.addUnit = 0
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.exactAt_of_isLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n i : ℤ),
  autoParam (n < i) CochainComplex.exactAt_of_isLE._auto_1 → ∀ [K.IsLE n], HomologicalComplex.ExactAt K i
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_eq_zero_of_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E) {y : E}, ‖y‖ = 0 → inner 𝕜 x y = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.Elements.fromFreeYoneda_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (m : M.Elements),
  (CategoryTheory.ConcreteCategory.hom (m.fromFreeYoneda.app m.fst))
      (ModuleCat.freeMk (CategoryTheory.CategoryStruct.id (Opposite.unop m.fst))) =
    m.snd
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toRingEquiv_eq_coe : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), e.toRingEquiv = e.toRingEquiv
-- Std.Data.TreeMap.Raw.Basic
/-- Checks whether a key is present in a map and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.TreeMap.Raw.containsThenInsert : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → β → Bool × Std.TreeMap.Raw α β cmp
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.instExceptT : {m : Type u_1 → Type u_2} →
  {ε : Type u_1} → [inst : Monad m] → [inst_1 : LawfulMonad m] → [MonadSatisfying m] → MonadSatisfying (ExceptT ε m)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rcc_eq_zero_iff : ∀ {m n i : ℕ}, (m...=n).toArray[i]! = 0 ↔ n + 1 ≤ i + m ∨ m = 0 ∧ i = 0
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.pos_eq : ∀ {s : String.Slice} {p q : s.Pos} {s_1 t t' : String}, p.Splits s_1 t → q.Splits s_1 t' → p = q
-- Lean.Meta.Tactic.Grind.Types
/-- `withEmatchDiagSource s x` executes `x` and uses `s` as the E-matching diagnostics source for any
term created.
 -/
Lean.Meta.Grind.withEmatchDiagSource : {m : Type → Type u_1} →
  {α : Type} → [MonadControlT Lean.Meta.Grind.GrindM m] → [Monad m] → Lean.Meta.Grind.EMatchDiagSource → m α → m α
-- Init.Prelude
/-- Returns the sequence of bytes in a character's UTF-8 encoding.
 -/
String.utf8EncodeChar : Char → List UInt8
-- Init.Prelude
Nat.pred_le_pred : ∀ {n m : ℕ}, n ≤ m → n.pred ≤ m.pred
-- Init.Data.String.Basic
String.Slice.Pos.str_inj : ∀ {s : String.Slice} (p₁ p₂ : s.Pos), p₁.str = p₂.str ↔ p₁ = p₂
-- Mathlib.Algebra.Star.Basic
/-- `star` as an equivalence when it is involutive.  -/
Equiv.Perm.star : {R : Type u} → [InvolutiveStar R] → Equiv.Perm R
-- Mathlib.Data.QPF.Univariate.Basic
QPF.suppPreservation_iff_uniform : ∀ {F : Type u → Type u} [q : QPF F], QPF.SuppPreservation ↔ QPF.IsUniform
-- Mathlib.RingTheory.Multiplicity
multiplicity_eq_of_associated_right : ∀ {α : Type u_1} [inst : Monoid α] {a b c : α}, Associated b c → multiplicity a b = multiplicity a c
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_add : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {a b : R},
  min ((IsDiscreteValuationRing.addVal R) a) ((IsDiscreteValuationRing.addVal R) b) ≤
    (IsDiscreteValuationRing.addVal R) (a + b)
-- Mathlib.Algebra.Lie.Prod
LieHom.inr_injective : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], Function.Injective ⇑(LieHom.inr R L₁ L₂)
-- Init.Data.Order.ClassesExtra
Std.LawfulOrderOrd.isGE_compare : ∀ {α : Type u} {inst : Ord α} {inst_1 : LE α} [self : Std.LawfulOrderOrd α] (a b : α), (compare a b).isGE = true ↔ b ≤ a
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsTopCompl.continuous_projectionOnto : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), Continuous ⇑(p.projectionOnto q ⋯)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.spectrum_one_eq : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [Nontrivial A],
  spectrum R 1 = {1}
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.of_surjective : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSemisimpleModule R M] (f : M →ₗ[R] N),
  Function.Surjective ⇑f → IsSemisimpleModule R N
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.instNontrivial : ∀ {n : ℕ}, Nontrivial (DihedralGroup n)
-- Mathlib.Algebra.Algebra.Basic
Algebra.algebraMap_ofSubring : ∀ {R : Type u_5} [inst : CommRing R] (S : Subring R), algebraMap (↥S) R = S.subtype
-- Lean.Util.FindMVar
Lean.FindMVar.main : (Lean.MVarId → Bool) → Lean.Expr → Lean.FindMVar.Visitor
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.coe_mrange : ∀ {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), ↑(MonoidHom.mrange f) = Set.range ⇑f
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.mulDistribMulAction : {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {m : Monoid α} →
        {n : (i : I) → Monoid (f i)} → [(i : I) → MulDistribMulAction α (f i)] → MulDistribMulAction α ((i : I) → f i)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Multiset.Nat.antidiagonalTuple_one : ∀ (n : ℕ), Multiset.Nat.antidiagonalTuple 1 n = {![n]}
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0IsoOfIsTrivial_inv_eq_π : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  (groupHomology.H0IsoOfIsTrivial A).inv = groupHomology.H0π A
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_pi : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] {s : Set δ} {t : (i : δ) → Set (X i)},
  s.Countable → (MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.eq_empty_iff_forall_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t = ∅ ↔ ∀ (a : α), a ∉ t
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation_trans_rightAngleRotation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)), o.rightAngleRotation.trans o.rightAngleRotation = LinearIsometryEquiv.neg ℝ
-- Mathlib.Data.List.Basic
List.append_left_injective : ∀ {α : Type u} (t : List α), Function.Injective fun s => s ++ t
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_dist : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) {n k : ℕ},
  n ≤ k →
    ‖newton_seq_gen✝ hnorm k - newton_seq_gen✝ hnorm n‖ ≤
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen✝ p F a ^ 2 ^ n
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_self_mul_star : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E}, ‖x * star x‖ = ‖x‖ * ‖x‖
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- If `η` is a lax transformation between `F` and `G`, we have a 1-morphism
`η.app a : F.obj a ⟶ G.obj a` for each object `a : B`. We also have a 2-morphism
`η.naturality f : app a ≫ G.map f ⟶ F.map f ≫ app b` for each 1-morphism `f : a ⟶ b`.
These 2-morphisms satisfy the naturality condition, and preserve the identities and
the compositions modulo some adjustments of domains and codomains of 2-morphisms.
 -/
CategoryTheory.Lax.LaxTrans : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.LaxFunctor B C → CategoryTheory.LaxFunctor B C → Type (max (max (max u₁ v₁) v₂) w₂)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {fallback : β} (h : t.WF),
  (Std.TreeMap.Raw.filter f t).getD k fallback = (t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.instLinear : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] → CategoryTheory.Linear R (CategoryTheory.ShortComplex C)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCompletionItemTag : Hashable Lean.Lsp.CompletionItemTag
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_of_splits' : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {L : Type u_4} [inst_5 : Field L] [inst_6 : Algebra F L]
  [inst_7 : Algebra L E] [inst_8 : IsScalarTower F L E] (f : L →ₐ[F] K),
  (∀ (s : E), IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits) → ∃ φ, AlgHom.domRestrict L φ = f
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote_mul : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly)
  (k : ℤ), Lean.Grind.Linarith.Poly.denote ctx (p.mul k) = k • Lean.Grind.Linarith.Poly.denote ctx p
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- Preimages of codiscrete sets: if `f` is analytic on a neighbourhood of `U` and not locally constant,
then the preimage of any subset codiscrete within `f '' U` is codiscrete within `U`.

See `AnalyticOnNhd.preimage_zero_mem_codiscreteWithin` for the special case that `s` is the
complement of zero. Applications might want to use the theorem `Filter.codiscreteWithin_mono`.
 -/
AnalyticOnNhd.preimage_mem_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {s : Set E} {f : 𝕜 → E},
  AnalyticOnNhd 𝕜 f U →
    (∀ x ∈ U, ¬Filter.EventuallyConst f (nhds x)) →
      s ∈ Filter.codiscreteWithin (f '' U) → f ⁻¹' s ∈ Filter.codiscreteWithin U
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isTop.inj : ∀ {idx idx_1 : ℕ}, Mathlib.Tactic.Order.AtomicFact.isTop idx = Mathlib.Tactic.Order.AtomicFact.isTop idx_1 → idx = idx_1
-- Init.Data.SInt.Lemmas
Int64.mod_self : ∀ {a : Int64}, a % a = 0
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- Prop-valued mixin for an ordered topological space to be
The upper set topology is the topology where the open sets are the upper sets. In general the upper
set topology does not coincide with the upper topology.
 -/
Topology.IsUpperSet : (α : Type u_4) → [t : TopologicalSpace α] → [Preorder α] → Prop
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.alter m k f) k = f (Std.ExtDHashMap.Const.get? m k)
-- Mathlib.Topology.Category.Stonean.Limits
Stonean.extremallyDisconnected_preimage : ∀ {X Y Z : Stonean} {f : X ⟶ Z} (i : Y ⟶ Z),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    ExtremallyDisconnected
      ↑(⇑(CategoryTheory.ConcreteCategory.hom i) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.factorₐ_comp : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (hIJ : I ≤ J) {K : Ideal A} [inst_5 : K.IsTwoSided] (hJK : J ≤ K),
  (Ideal.Quotient.factorₐ R₁ hJK).comp (Ideal.Quotient.factorₐ R₁ hIJ) = Ideal.Quotient.factorₐ R₁ ⋯
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- The **Plünnecke-Ruzsa inequality**. Division version.  -/
Finset.pluennecke_ruzsa_inequality_pow_div_pow_div : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] {A : Finset G},
  A.Nonempty → ∀ (B : Finset G) (m n : ℕ), ↑(B ^ m / B ^ n).card ≤ (↑(A / B).card / ↑A.card) ^ (m + n) * ↑A.card
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C),
  CategoryTheory.Abelian.coimageImageComparison (α.app X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Abelian.coimageImageComparison α).app X)
        (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).hom)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.mul_one.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] (a : Rack.PreEnvelGroup R),
  sizeOf (Rack.PreEnvelGroupRel'.mul_one a) = 1 + sizeOf a
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_insertEntry_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = true → Std.Internal.List.minKey (Std.Internal.List.insertEntry k v l) ⋯ = k
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ofGroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G),
  HNNExtension.NormalWord.ofGroup g = { head := g, toList := [], chain := ⋯, mem_set := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : m → α} [inst : DecidableEq n],
  M.transpose.updateRow j c = (M.updateCol j c).transpose
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRoc.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Roc α) → Decidable (x = x_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.expDegree.eq_1 : ∀ (n : ℕ), WeierstrassCurve.expDegree✝ n = (n ^ 2 - if Even n then 4 else 1) / 2
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorph.image_coe : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N}
  (hf : IsLocalDiffeomorph I J n f), hf.image.carrier = Set.range f
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.instInitiallySmallProd : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {J' : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J'] [CategoryTheory.InitiallySmall J] [CategoryTheory.InitiallySmall J'],
  CategoryTheory.InitiallySmall (J × J')
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
GaloisConnection.u_ciInf_of_directed : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α]
  [inst_1 : ConditionallyCompletePartialOrderInf β] [Nonempty ι] {l : α → β} {u : β → α},
  GaloisConnection u l →
    ∀ {f : ι → α}, Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → l (⨅ i, f i) = ⨅ i, l (f i)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc_ι_assoc : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (c : f.Cell j) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp c.mapToSucc
      (CategoryTheory.CategoryStruct.comp (f.filtration (Order.succ j)).ι h) =
    CategoryTheory.CategoryStruct.comp c.map h
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.self_mul_conjTranspose_eq_zero : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {m : Type u_5} {A : Matrix m n R},
  A * A.conjTranspose = 0 ↔ A = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeParams : Type
-- Init.Data.ByteArray.Basic
/-- Retrieves the byte at the indicated index. Panics if the index is out of bounds.
 -/
ByteArray.get! : ByteArray → ℕ → UInt8
-- Batteries.Classes.Order
Std.instOrientedCmpCompareLex_batteries : ∀ {α : Type u_1} {cmp₁ cmp₂ : α → α → Ordering} [inst₁ : Std.OrientedCmp cmp₁] [inst₂ : Std.OrientedCmp cmp₂],
  Std.OrientedCmp (compareLex cmp₁ cmp₂)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `mdifferentiableAt_localFrameCoeff`.

---

If `s` is differentiable at `x`, so is its coefficient `b.localFrameCoeff e i` in the local
frame near `x` induced by `e` and `b`  -/
mdifferentiableAt_localFrame_coeff : ∀ {𝕜 : 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] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {x : M}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜],
  x ∈ e.baseSet →
    MDiffAt (T% s) x → ∀ (i : ι), MDiffAt ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) x
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
/-- The `SubMulAction` generated by a set `s`.  -/
SubMulAction.closure : (R : Type u_1) → {M : Type u_2} → [inst : SMul R M] → Set M → SubMulAction R M
-- Mathlib.Algebra.Algebra.Pi
Pi.coe_evalAlgHom : ∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] (i : ι), ↑(Pi.evalAlgHom R A i) = Pi.evalRingHom A i
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_iUnion_le : ∀ {α ι : Type u} (f : ι → Set α), Cardinal.mk ↑(⋃ i, f i) ≤ Cardinal.mk ι * ⨆ i, Cardinal.mk ↑(f i)
-- Mathlib.Order.Category.OmegaCompletePartialOrder
/-- The category of types with an omega complete partial order.  -/
ωCPO : Type (u + 1)
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- If `b` mod `p` spans `S/p` as `R/p`-space, then `b` itself spans `Frac(S)` as `K`-space.

Here,
* `p` is an ideal of `R` such that `R / p` is nontrivial
* `K` is a field that has an embedding of `R` (in particular we can take `K = Frac(R)`)
* `L` is a field extension of `K`
* `S` is the integral closure of `R` in `L`

More precisely, we avoid quotients in this statement and instead require that `b ∪ pS` spans `S`.
 -/
Ideal.FinrankQuotientMap.span_eq_top : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {K : Type u_1} [inst_3 : Field K] [inst_4 : Algebra R K] {L : Type u_2} [inst_5 : Field L] [inst_6 : Algebra S L]
  [IsFractionRing S L] [IsDomain R] [IsDomain S] [inst_10 : Algebra K L] [Module.Finite R S] [inst_12 : Algebra R L]
  [IsScalarTower R S L] [IsScalarTower R K L] [Algebra.IsAlgebraic R S] [Module.IsTorsionFree R K],
  p ≠ ⊤ →
    ∀ (b : Set S),
      Submodule.span R b ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p) = ⊤ →
        Submodule.span K (⇑(algebraMap S L) '' b) = ⊤