mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.next_ne_startPos : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos}, p.next h ≠ s.startPos
-- Lean.Parser.Command
Lean.Parser.Command.declId.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Prod
Prod.instAddRightCancelMonoid : {M : Type u_3} → {N : Type u_4} → [AddRightCancelMonoid M] → [AddRightCancelMonoid N] → AddRightCancelMonoid (M × N)
-- Std.Data.DHashMap.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `get_insertIfNew`.  -/
Std.DHashMap.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'_eq_forIn' : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  [LawfulMonad n] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ} {γ : Type x} {it : Std.IterM m β}
  {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b} {Q : β → Prop}
  {hQ : ∀ (b : β), it.IsPlausibleIndirectOutput b → Q b} (Pl : β → γ → ForInStep γ → Prop)
  {f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))} {g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))},
  Std.IteratorLoop.WellFounded α m Pl →
    (∀ (b : β) (c : γ) (hPb : P b) (hQb : Q b), f b hPb c = g b hQb c) →
      Std.IterM.DefaultConsumers.forIn' lift γ Pl it init P hP f =
        Std.IterM.DefaultConsumers.forIn' lift γ Pl it init Q hQ g
-- Init.Data.Order.Lemmas
Std.not_le : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.Total fun x1 x2 => x1 ≤ x2] [Std.LawfulOrderLT α] {a b : α},
  ¬a ≤ b ↔ b < a
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rii_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α}, Std.Rii.Sliceable.mkSlice xs *...* = Std.Rco.Sliceable.mkSlice xs 0...xs.size
-- Init.Data.Range.Polymorphic.SInt
ISize.instUpwardEnumerable : Std.PRange.UpwardEnumerable ISize
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.keys.toArray = t.keysArray
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_diagonal_right : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : Zero β]
  [inst_1 : Zero γ] [inst_2 : DecidableEq n] (f : α → β → γ),
  (∀ (a : α), f a 0 = 0) →
    ∀ (A : Matrix l m α) (b : n → β),
      Matrix.kroneckerMap f A (Matrix.diagonal b) = Matrix.blockDiagonal fun i => A.map fun a => f a (b i)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The iterated derivative of the composition with a linear map on the right is
obtained by composing the iterated derivative with the linear map.  -/
ContinuousLinearMap.iteratedFDeriv_comp_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} (g : G →L[𝕜] E) {f : E → F},
  ContDiff 𝕜 n f →
    ∀ (x : G) {i : ℕ},
      ↑i ≤ n → iteratedFDeriv 𝕜 i (f ∘ ⇑g) x = (iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap fun x => g
-- Lean.Util.Trace
Lean.TraceState.traces : Lean.TraceState → Lean.PersistentArray Lean.TraceElem
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- An `R`-algebra norm such that `f 1 = 1` extends the norm on `R`.  -/
AlgebraNorm.extends_norm : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  {f : AlgebraNorm R S}, f 1 = 1 → ∀ (a : R), f ((algebraMap R S) a) = ‖a‖
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSymbolKind : Lean.ToJson Lean.Lsp.SymbolKind
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.free_ε_one : ∀ (R : Type u) [inst : CommRing R],
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.ε (ModuleCat.free R))) 1 =
    ModuleCat.freeMk PUnit.unit
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mem_one_iff : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {x : P}, x ∈ 1 ↔ ∃ x', (algebraMap R P) x' = x
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_le_prod_diam : ∀ {ι : Type u_1} [inst : Fintype ι] (s : Set (ι → ℝ)), MeasureTheory.volume s ≤ ∏ i, Metric.ediam (Function.eval i '' s)
-- Mathlib.Algebra.Regular.Pi
Pi.isAddRightRegular_iff : ∀ {ι : Type u_1} {R : ι → Type u_3} [inst : (i : ι) → Add (R i)] {a : (i : ι) → R i},
  IsAddRightRegular a ↔ ∀ (i : ι), IsAddRightRegular (a i)
-- Mathlib.Algebra.Order.Sub.Defs
tsub_le_iff_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ b + c
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Functor.instPreservesLimitsOfSizeOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w')) [F.IsRepresentable],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, w', u, w' + 1} F
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.mem_nonDegenerate_iff_notMem_degenerate : ∀ (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })), x ∈ X.nonDegenerate n ↔ x ∉ X.degenerate n
-- Init.Data.Range.Polymorphic.Iterators
Std.Roo.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : LT α] →
        [inst_2 : DecidableLT α] →
          [Std.PRange.LawfulUpwardEnumerable α] →
            [Std.PRange.LawfulUpwardEnumerableLT α] →
              [Monad m] → [Std.Iterators.Finite (Std.Rxo.Iterator α) Id] → ForIn' m (Std.Roo α) α inferInstance
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_lt_withBotDegree_iff_of_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R}
  (g : MvPolynomial σ R),
  f ≠ 0 →
    (m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
      m.toSyn (m.degree f) < m.toSyn (m.degree g))
-- Lean.Parser.Command
Lean.Parser.Command.quot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
/-- `Complex.inv_cpow_eq_ite` with the `ite` on the other side.  -/
Complex.inv_cpow_eq_ite' : ∀ (x n : ℂ), (x ^ n)⁻¹ = if x.arg = Real.pi then (starRingEnd ℂ) (x⁻¹ ^ (starRingEnd ℂ) n) else x⁻¹ ^ n
-- Mathlib.Order.CompleteLattice.Basic
/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
is larger than all elements of `s`, and that this is not the case of any `w < b`.
See `csSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete
lattices.  -/
sSup_eq_of_forall_le_of_forall_lt_exists_gt : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {b : α},
  (∀ a ∈ s, a ≤ b) → (∀ w < b, ∃ a ∈ s, w < a) → sSup s = b
-- Mathlib.RepresentationTheory.Rep.Iso
/-- An isomorphism of `k`-linear representations of `G` from `k[Gⁿ⁺¹]` to `k[G] ⊗ₖ k[Gⁿ]` (on
which `G` acts by `ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x`) sending `(g₀, ..., gₙ)` to
`g₀ ⊗ (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)`. The inverse sends `g₀ ⊗ (g₁, ..., gₙ)` to
`(g₀, g₀g₁, ..., g₀g₁...gₙ)`.  -/
Rep.diagonalSuccIsoTensorTrivial : (k G : Type u) →
  [inst : Group G] →
    [inst_1 : CommRing k] →
      (n : ℕ) →
        Rep.diagonal k G (n + 1) ≅
          CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.leftRegular k G)
            (Rep.trivial k G (MonoidAlgebra k (Fin n → G)))
-- Init.Data.String.Substring
Substring.next : Substring.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_objs_of_src : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d : C} {f : c ⟶ d},
  f ∈ S.arrows c d → c ∈ S.objs
-- Init.Data.Sum.Basic
Sum.lex_inl_inl : ∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {a₁ a₂ : α},
  Sum.Lex r s (Sum.inl a₁) (Sum.inl a₂) ↔ r a₁ a₂
-- Mathlib.Data.Set.Functor
Set.mem_of_mem_coe : ∀ {α : Type u} {β : Set α} {γ : Set ↑β} {a : α}
  (ha :
    a ∈ do
      let a ← γ
      pure ↑a),
  ⟨a, ⋯⟩ ∈ γ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The **measurable Schröder-Bernstein Theorem**: given measurable embeddings
`α → β` and `β → α`, we can find a measurable equivalence `α ≃ᵐ β`.  -/
MeasurableEmbedding.schroederBernstein : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → {f : α → β} → {g : β → α} → MeasurableEmbedding f → MeasurableEmbedding g → α ≃ᵐ β
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The coproduct is homeomorphic to the disjoint union of the topological spaces.
 -/
TopCat.sigmaIsoSigma : {ι : Type v} → (α : ι → TopCat) → ∐ α ≅ TopCat.of ((i : ι) × ↑(α i))
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_sum : ∀ {ι : Type u_1} (f : ι → ℕ → ℂ) (S : Finset ι) (s : ℂ), LSeries.term (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries.term (f i) s
-- Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
/-- If `f` is `n` times continuously differentiable at `x`, then the `n`th iterated Fréchet derivative
with respect to `𝕜` equals scalar restriction of the `n`th iterated Fréchet derivative with respect
to `𝕜'`.
 -/
ContDiffAt.restrictScalars_iteratedFDeriv_eventuallyEq : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {x : E} {f : E → F} {n : ℕ},
  ContDiffAt 𝕜' (↑n) f x →
    ContinuousMultilinearMap.restrictScalars 𝕜 ∘ iteratedFDeriv 𝕜' n f =ᶠ[nhds x] iteratedFDeriv 𝕜 n f
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- If `f ≫ g = 0` implies `g = 0` for all `g`, then `g` is a monomorphism.  -/
CategoryTheory.NormalMonoCategory.epi_of_zero_cancel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C]
  [CategoryTheory.IsNormalMonoCategory C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y),
  (∀ (Z : C) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) → CategoryTheory.Epi f
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.mk : (toGrp : GrpCat) → [isFinite : Finite ↑toGrp] → FiniteGrp.{u}
-- Init.Data.List.Lemmas
List.cons_beq_cons : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l₁ l₂ : List α}, (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_sub_iff_add_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b c : α}, a ≤ c - b ↔ a + b ≤ c
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.Functor.instFaithfulSkeletonMapSkeleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Faithful], F.mapSkeleton.Faithful
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionCyclesIso_inv_iCycles_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (j k : ι) (hk : c.next j = k) {j' k' : ι'}
  (hj' : e.f j = j') (hk' : e.f k = k') (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j] {Z : C} (h : (K.restriction e).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv
      (CategoryTheory.CategoryStruct.comp ((K.restriction e).iCycles j) h) =
    CategoryTheory.CategoryStruct.comp (K.iCycles j')
      (CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').inv h)
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalGroup.mulInvClosureNhd.inv : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : Group G],
  IsTopologicalGroup.mulInvClosureNhd T W → T⁻¹ = T
-- Mathlib.CategoryTheory.Localization.Predicate
/-- Localization of a category with respect to all morphisms results in a groupoid.  -/
CategoryTheory.Localization.groupoid : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Groupoid ⊤.Localization
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- associativity of the tensorator  -/
CategoryTheory.Functor.CoreMonoidal.associativity_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) (X Y Z : C) {Z_1 : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.μIso X Y).hom (F.obj Z))
      (CategoryTheory.CategoryStruct.comp (self.μIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (self.μIso Y Z).hom)
        (CategoryTheory.CategoryStruct.comp (self.μIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom h))
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Star α] (M : Matrix m n α), M.conjTranspose = M.transpose.map star
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mul_mem_cancel_left : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → (x * y ∈ H ↔ y ∈ H)
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.of_pow : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : A} {n : ℕ},
  0 < n → IsAlgebraic R (r ^ n) → IsAlgebraic R r
-- Mathlib.Order.Max
/-- **Alias** of the reverse direction of `isBot_toDual_iff`. -/
IsTop.toDual : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsBot (OrderDual.toDual a)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.app_localPreimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : Cᵒᵖ}
  (s : CategoryTheory.ToType (G.obj U)) {V : C} (g : V ⟶ Opposite.unop U)
  (hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g),
  (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op V))) (CategoryTheory.Presheaf.localPreimage f s g hg) =
    (CategoryTheory.ConcreteCategory.hom (G.map g.op)) s
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.setIntegral_tilted_mul_eq_mgf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (g : Ω → E) (s : Set Ω),
  (∫ (x : Ω) in s, g x ∂μ.tilted fun x => t * X x) =
    ∫ (x : Ω) in s, (Real.exp (t * X x) / ProbabilityTheory.mgf X μ t) • g x ∂μ
-- Mathlib.Data.Num.Prime
PosNum.minFac_to_nat : ∀ (n : PosNum), ↑n.minFac = (↑n).minFac
-- Mathlib.Data.Int.SuccPred
Int.instSuccOrder : SuccOrder ℤ
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_refl : ∀ {M : Type u_4} [inst : Add M], ⇑(AddEquiv.refl M) = id
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.MinIndexableMode.no.sizeOf_spec : sizeOf Lean.Meta.Grind.MinIndexableMode.no = 1
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.mk : {E : Type u_8} →
  [toNorm : Norm E] →
    [toGroup : Group E] →
      [toMetricSpace : MetricSpace E] →
        autoParam (∀ (x y : E), dist x y = ‖x⁻¹ * y‖) NormedGroup.dist_eq._autoParam → NormedGroup E
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_ofNat : ∀ (n : ℕ), Int32.ofBitVec (BitVec.ofNat 32 n) = Int32.ofNat n
-- Mathlib.Topology.Order.LeftRightNhds
nhds_basis_Icc_one_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α]
  [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] (a : α),
  (nhds a).HasBasis (fun x => 1 < x) fun ε => Set.Icc (a / ε) (a * ε)
-- Mathlib.GroupTheory.Nilpotent
AddGroup.IsNilpotent.nilpotencyClass_nonpos_iff : ∀ {G : Type u_1} [inst : AddGroup G] [AddGroup.IsNilpotent G], AddGroup.nilpotencyClass G ≤ 1 ↔ IsAddCommutative G
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- Isomorphic algebras induce isomorphic `H¹(L_{S/R})`.  -/
Algebra.H1Cotangent.mapEquiv : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (S' : Type u_2) →
            [inst_3 : CommRing S'] →
              [inst_4 : Algebra R S'] → (S ≃ₐ[R] S') → Algebra.H1Cotangent R S ≃ₗ[R] Algebra.H1Cotangent R S'
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isArrayLitTransition : Lean.Meta.Match.Problem → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_insertIfNew_le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ →
    ∀ {k : α} {v : β} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.SetTheory.Ordinal.Basic
/-- `Quotient.inductionOn` specialized to ordinals.

Not to be confused with well-founded induction `WellFoundedLT.induction`.  -/
Ordinal.inductionOn : ∀ {motive : Ordinal.{u_1} → Prop} (o : Ordinal.{u_1}),
  (∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r], motive (Ordinal.type r)) → motive o
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A coercion from an arrow with codomain `P` to its associated pseudoelement.  -/
CategoryTheory.Abelian.Pseudoelement.overToSort : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → {P : C} → Coe (CategoryTheory.Over P) (CategoryTheory.Abelian.Pseudoelement P)
-- Mathlib.Algebra.CharP.Defs
ringChar.spec : ∀ (R : Type u_1) [inst : NonAssocSemiring R] (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.mk.injEq : ∀ {Γ : Type u_8} {R : Type u_9} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {α : Type u_7}
  (toFun : α → HahnSeries Γ R) (isPWO_iUnion_support' : (⋃ a, (toFun a).support).IsPWO)
  (finite_co_support' : ∀ (g : Γ), {a | (toFun a).coeff g ≠ 0}.Finite) (toFun_1 : α → HahnSeries Γ R)
  (isPWO_iUnion_support'_1 : (⋃ a, (toFun_1 a).support).IsPWO)
  (finite_co_support'_1 : ∀ (g : Γ), {a | (toFun_1 a).coeff g ≠ 0}.Finite),
  ({ toFun := toFun, isPWO_iUnion_support' := isPWO_iUnion_support', finite_co_support' := finite_co_support' } =
      { toFun := toFun_1, isPWO_iUnion_support' := isPWO_iUnion_support'_1,
        finite_co_support' := finite_co_support'_1 }) =
    (toFun = toFun_1)
-- Lean.Widget.TaggedText
Lean.Widget.instBEqTaggedText : {α : Type u_1} → [BEq α] → BEq (Lean.Widget.TaggedText α)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.baseChange_addPolynomial : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Affine R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (x y ℓ : A),
  (W'.baseChange B).addPolynomial (f x) (f y) (f ℓ) = Polynomial.map (↑f) ((W'.baseChange A).addPolynomial x y ℓ)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.self_mem_adjoin_singleton : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (x : A), x ∈ NonUnitalAlgebra.adjoin R {x}
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt64.beq_eq_decide_eq : ∀ {a b : UInt64}, (a == b) = decide (a = b)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.contains a = false → t.getD a fallback = fallback
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
/-- The functor `SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory`
is a covariant involution.  -/
SimplexCategory.revCompRevIso : SimplexCategory.rev.comp SimplexCategory.rev ≅ CategoryTheory.Functor.id SimplexCategory
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The map sending `f : P ⟶ Q` to `f.f : P.X ⟶ Q.X` is additive.  -/
CategoryTheory.Idempotents.Karoubi.inclusionHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (P Q : CategoryTheory.Idempotents.Karoubi C) → (P ⟶ Q) →+ (P.X ⟶ Q.X)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.toUliftFunctor_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X)
  (hf : S.arrows f) (Z : Cᵒᵖ),
  (S.toUliftFunctor f hf).app Z = TypeCat.ofHom fun g => { down := ⟨CategoryTheory.CategoryStruct.comp g.down f, ⋯⟩ }
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.CancelParams : Type
-- Lean.Meta.TryThis
/-- Optional style specification for the suggestion. If `none` (the default), the suggestion is
styled as a text link. Otherwise, the suggestion can be styled as:
* a status: `.error`, `.warning`, `.success`
* a hypothesis name: `.asHypothesis`, `.asInaccessible`
* a variable color: `.value (t : Float)`, which draws from a red-yellow-green gradient, with red
at `0.0` and green at `1.0`.

See `SuggestionStyle` for details.

Note that this property is used only by the "try this" widget; it is ignored by the inline hint
widget.  -/
Lean.Meta.Tactic.TryThis.Suggestion.style? : Lean.Meta.Tactic.TryThis.Suggestion → Option Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.algHom_bijective : ∀ {K : Type u_1} {L : Type u_2} [inst : CommRing K] [IsDomain K] [inst_2 : Field L] [inst_3 : Algebra K L]
  [Module.IsTorsionFree K L] [Algebra.IsAlgebraic K L] (f : L →ₐ[K] L), Function.Bijective ⇑f
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerLeft_twice : ∀ {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] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D)
  {H K : CategoryTheory.Functor D E} (α : H ⟶ K),
  F.whiskerLeft (G.whiskerLeft α) =
    CategoryTheory.CategoryStruct.comp (F.associator G H).inv
      (CategoryTheory.CategoryStruct.comp ((F.comp G).whiskerLeft α) (F.associator G K).hom)