mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.instIsIsoHomInvCocone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cocone F} (f : c ≅ d), CategoryTheory.IsIso f.hom.hom
-- Mathlib.Data.Nat.Factorial.Basic
Nat.one_lt_factorial : ∀ {n : ℕ}, 1 < n.factorial ↔ 1 < n
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roi.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roi α}, r.toList = (Std.Roi.Internal.iter r).toList
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.algHom_ext_of_eq_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Semiring K] [inst_4 : Algebra F K] {S : IntermediateField F E} {s : Set E}
  (hS : S = IntermediateField.adjoin F s) ⦃φ₁ φ₂ : ↥S →ₐ[F] K⦄,
  (∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) → φ₁ = φ₂
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instSMulCommClass : ∀ {α : Type u_1} {𝕜 : Type u_2} {𝕜' : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : NormedRing 𝕜']
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜' E] [inst_5 : IsBoundedSMul 𝕜 E] [inst_6 : IsBoundedSMul 𝕜' E]
  [SMulCommClass 𝕜 𝕜' E], SMulCommClass 𝕜 𝕜' ↥(MeasureTheory.Lp E p μ)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_counit_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : D} (f f' : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (e.counit.app Y) f = CategoryTheory.CategoryStruct.comp (e.counit.app Y) f' ↔
    f = f'
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.skip.eq_1 : ∀ (goal : Lean.Meta.Grind.Goal) (x kp : Lean.Meta.Grind.ActionCont), Lean.Meta.Grind.Action.skip goal x kp = kp goal
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_map_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.map f m) k = Option.map (f k') (Std.DHashMap.Raw.Const.get? m k)
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.coeff_coe_units_zero_ne_zero : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ), (↑u).coeff 0 ≠ 0
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k : α}, k ∈ m → (m.insertMany l).get? k = m.get? k
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.reflexivity₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.ReflexiveRelation p₁ p₂) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.r (CategoryTheory.CategoryStruct.comp p₂ h) = h
-- Lean.PrettyPrinter
/-- Return a `fmt` representing pretty-printed `e` together with a map from tags in `fmt`
to `Elab.Info` nodes produced by the delaborator at various subexpressions of `e`.  -/
Lean.PrettyPrinter.ppExprWithInfos : Lean.Expr →
  optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅ →
    optParam Lean.PrettyPrinter.Delaborator.Delab Lean.PrettyPrinter.Delaborator.delab → Lean.MetaM Lean.FormatWithInfos
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.IsBase.ncard_sdiff_comm`. -/
Matroid.IsBase.ncard_diff_comm : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → (B₁ \ B₂).ncard = (B₂ \ B₁).ncard
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snocCases_snoc : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {motive : ((i : Fin (n + 1)) → α i) → Sort u_2}
  (snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (Fin.last n)) → motive (Fin.snoc x x₀))
  (x : (i : Fin n) → Fin.init α i) (x₀ : α (Fin.last n)), Fin.snocCases snoc (Fin.snoc x x₀) = snoc x x₀
-- Init.Data.Array.Lemmas
Array.foldr_append' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {xs ys : Array α} {start : ℕ},
  start = xs.size + ys.size → Array.foldr f b (xs ++ ys) start = Array.foldr f (Array.foldr f b ys) xs
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive left cancel monoid,if it
admits an injective map that preserves `0` and `+` to an additive left cancel monoid.  -/
Function.Injective.addRightCancelMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : AddRightCancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 0 = 0 →
                  (∀ (x y : M₁), f (x + y) = f x + f y) →
                    (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddRightCancelMonoid M₁
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- `TStructure C` is the type of t-structures on the (pre)triangulated category `C`.  -/
CategoryTheory.Triangulated.TStructure : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → Type u_1
-- Mathlib.Algebra.Group.TypeTags.Basic
toAdd_one : ∀ {α : Type u} [inst : Zero α], Multiplicative.toAdd 1 = 0
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.ppMap : {ρ : Type u_1} →
  {α β : Type} → [ForIn Id ρ (α × β)] → [Lean.ToMessageData α] → [Lean.ToMessageData β] → Bool → ρ → Lean.MessageData
-- Mathlib.Topology.Homeomorph.Lemmas
/-- The natural homeomorphism between `(Fin m → X) × (Fin n → X)` and `Fin (m + n) → X`.
`Fin.appendEquiv` as a homeomorphism  -/
Fin.appendHomeomorph : {X : Type u_1} → [inst : TopologicalSpace X] → (m n : ℕ) → (Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X)
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.uniformContinuous_extend : ∀ {α : Type u} [inst : UniformSpace α] {β : Type v} [inst_1 : UniformSpace β] [CompleteSpace β] {f : α → β},
  UniformContinuous (CauchyFilter.extend f)
-- Mathlib.Analysis.Normed.Order.Hom.Basic
AddGroupNormClass.toNormedAddGroup_norm_eq : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddGroup α] [inst_2 : AddGroupNormClass F α ℝ] (f : F)
  (x : α), ‖x‖ = f x
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_Ico_eq_restrict_Ioc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, μ.restrict (Set.Ico a b) = μ.restrict (Set.Ioc a b)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Decomposes a friendly operation by the head of the input sequence. Returns `none` if the output
is `nil`, or `some (exp, coef, op')` where `(exp, coef)` is the head of the output and
`op'` is a friendly operation mapping the tail of the input to the tail of the output. See
`destruct_apply_eq_unfold` for the correctness statement.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.unfold : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    {op :
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
          Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op →
        Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl) →
          Option
            (ℝ ×
              Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl ×
                Subtype Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_containsKey_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueCast? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = none
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {n : ℤ}
  {X Y : Cᵒᵖ} (f : Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y),
  (CategoryTheory.shiftFunctor C n).map (CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv f).unop =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app Y).unop f.unop
-- Plausible.Testable
/-- Test a universal property by creating a sample of the right type and instantiating the
bound variable with it.  -/
Plausible.Testable.varTestable : {var : String} →
  {α : Type u_1} →
    [Plausible.SampleableExt α] →
      {β : α → Prop} →
        [(x : α) → Plausible.Testable (β x)] → Plausible.Testable (Plausible.NamedBinder var (∀ (x : α), β x))
-- Mathlib.Algebra.CharP.MixedCharZero
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.PNat.isUnit_natCast : ∀ {R : Type u_1} [inst : CommRing R] [h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))] (n : ℕ+), IsUnit ↑↑n
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_pnat : Cardinal.mk ℕ+ = Cardinal.aleph0
-- Mathlib.Algebra.Algebra.Hom
/-- Turn an element of a type `F` satisfying `AlgHomClass F α β` into an actual
`AlgHom`. This is declared as the default coercion from `F` to `α →+* β`.  -/
AlgHomClass.toAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → {F : Type u_5} → [inst_5 : FunLike F A B] → [AlgHomClass F R A B] → F → A →ₐ[R] B
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_eq_decide_div_mod_eq : ∀ {i x : ℕ}, x.testBit i = decide (x / 2 ^ i % 2 = 1)
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g - h) μ μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.forInUncurried_eq_forIn_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : α × β → δ → m (ForInStep δ)} {init : δ},
  Std.ExtDTreeMap.Const.forInUncurried f init t = forIn (Std.ExtDTreeMap.Const.toList t) init f
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_Ico_val : ∀ {n : ℕ} (i j : Fin n), Fin.val ⁻¹' Set.Ico ↑i ↑j = Set.Ico i j
-- Lean.Expr
Lean.Expr.mdata.injEq : ∀ (data : Lean.MData) (expr : Lean.Expr) (data_1 : Lean.MData) (expr_1 : Lean.Expr),
  (Lean.Expr.mdata data expr = Lean.Expr.mdata data_1 expr_1) = (data = data_1 ∧ expr = expr_1)
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- The form of the **fundamental identity** in the case of Galois extension.  -/
Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn : ∀ {A : Type u_1} [inst : CommRing A] [IsDomain A] (p : Ideal A) [p.IsPrime] (B : Type u_2) [inst_3 : CommRing B]
  [IsDomain B] [inst_5 : Algebra A B] [Module.Finite A B] [Module.Flat A B] (G : Type u_3) [inst_8 : Group G] [Finite G]
  [inst_10 : MulSemiringAction G B] [IsGaloisGroup G A B],
  (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Nat.card G
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcomp₁_obj_hom_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L'))
  (X_1 : C),
  ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).hom.app X_1 =
    CategoryTheory.CategoryStruct.comp (X.hom.app X_1) (X.right.map (f.app X_1))
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_opow : ∀ {b : Ordinal.{u_1}}, 1 < b → ∀ (x : Ordinal.{u_1}), Ordinal.log b (b ^ x) = x
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
_private.Mathlib.CategoryTheory.Limits.Shapes.Countable.0.CategoryTheory.Limits.IsCofiltered.hasCountableColimits_of_hasFiniteColimits_and_hasSequentialColimits : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasFiniteColimits C] →
      [CategoryTheory.Limits.HasLimitsOfShape ℕ C] → ProofWanted (CategoryTheory.Limits.HasCountableColimits C)
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.wildcard.sizeOf_spec : sizeOf Mathlib.Linter.Flexible.Stained.wildcard✝ = 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.union_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.union t₂ = t₁ ∪ t₂
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- The typeclass `SecondCountableTopologyEither α β` registers the fact that at least one of
the two spaces has second countable topology. This is the right assumption to ensure that continuous
maps from `α` to `β` are strongly measurable.  -/
SecondCountableTopologyEither : (α : Type u_6) → (β : Type u_7) → [TopologicalSpace α] → [TopologicalSpace β] → Prop
-- Mathlib.Analysis.Analytic.Order
IsOpen.forall_analyticOrderAt_eq_top_iff_eqOn_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set 𝕜}, IsOpen s → ∀ (f : 𝕜 → E), (∀ z ∈ s, analyticOrderAt f z = ⊤) ↔ Set.EqOn f 0 s
-- Mathlib.NumberTheory.MulChar.Basic
/-- The `p`th power of a quadratic character is itself, when `p` is the (prime) characteristic
of the target ring.  -/
MulChar.IsQuadratic.pow_char : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {χ : MulChar R R'},
  χ.IsQuadratic → ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R' p], χ ^ p = χ
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Complex.isTheta_cpow_rpow : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℂ},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |(g x).im|) →
    (∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0) → (fun x => f x ^ g x) =Θ[l] fun x => ‖f x‖ ^ (g x).re
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β]
  [inst_4 : Max γ] [inst_5 : Bot γ] {g : SupBotHom β γ} {f₁ f₂ : SupBotHom α β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.saturate_toPreZeroHypercover : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S),
  E.saturate.toPreZeroHypercover = E
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (α : g ≅ h),
  (CategoryTheory.Bicategory.whiskerLeftIso f α).hom = (CategoryTheory.Bicategory.whiskerLeftIso f α).hom
-- Mathlib.Data.Fintype.Sets
Fintype.coe_finsetOrderIsoSet_symm : ∀ {α : Type u_1} [inst : Fintype α], ⇑Fintype.finsetOrderIsoSet.symm = ⇑Fintype.finsetEquivSet.symm
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal.mk : Lean.MVarId → Array Lean.FVarId → Lean.FVarId → ℕ → Lean.Meta.GeneralizeIndicesSubgoal
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
/-- `(x, y) ↦ x ^ y` is strictly differentiable at `p : ℝ × ℝ` such that `0 < p.fst`.  -/
Real.hasStrictFDerivAt_rpow_of_pos : ∀ (p : ℝ × ℝ),
  0 < p.1 →
    HasStrictFDerivAt (fun x => x.1 ^ x.2)
      ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        (p.1 ^ p.2 * Real.log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ)
      p
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_ac.inj : ∀ {lhs : Bool} {s : Lean.Grind.AC.Seq} {c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr} {lhs_1 : Bool} {s_1 : Lean.Grind.AC.Seq}
  {c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.simp_ac lhs s c₁ c₂ = Lean.Meta.Grind.AC.EqCnstrProof.simp_ac lhs_1 s_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.NumberTheory.RamificationInertia.Unramified
/-- In characteristic zero the generic point is unramified: if `S` is a domain that is integral
over a characteristic-zero domain `R` and `R → S` is injective, then `S` is unramified at the zero
ideal.  -/
Algebra.isUnramifiedAt_bot : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [inst_4 : IsDomain S] [Module.IsTorsionFree R S] [CharZero R] [Algebra.IsIntegral R S], Algebra.IsUnramifiedAt R ⊥
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_add : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A) {m n : ℕ}, n ≠ 0 → M ^ (m + n) = M ^ m * M ^ n
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.match_1.splitter : (motive : Lean.Grind.IntInterval → Lean.Grind.IntInterval → Sort u_1) →
  (x x_1 : Lean.Grind.IntInterval) →
    ((a a_1 b b_1 : ℤ) → motive (Lean.Grind.IntInterval.co a a_1) (Lean.Grind.IntInterval.co b b_1)) →
      ((a b : ℤ) → motive (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b)) →
        ((a b : ℤ) → motive (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b)) →
          (Unit → motive Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii) →
            ((x x_2 : Lean.Grind.IntInterval) →
                (∀ (a a_1 b b_1 : ℤ),
                    x = Lean.Grind.IntInterval.co a a_1 → x_2 = Lean.Grind.IntInterval.co b b_1 → False) →
                  (∀ (a b : ℤ), x = Lean.Grind.IntInterval.ci a → x_2 = Lean.Grind.IntInterval.ci b → False) →
                    (∀ (a b : ℤ), x = Lean.Grind.IntInterval.io a → x_2 = Lean.Grind.IntInterval.io b → False) →
                      (x = Lean.Grind.IntInterval.ii → x_2 = Lean.Grind.IntInterval.ii → False) → motive x x_2) →
              motive x x_1
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instBoundedOrder.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instBoundedOrder =
    { toTop := AddGroupTopology.instTop, le_top := ⋯, toBot := AddGroupTopology.instBot, bot_le := ⋯ }
-- Aesop.Stats.Report
Aesop.StatsReport.scripts : Aesop.StatsReport
-- Batteries.Data.AssocList
Batteries.AssocList.toListTR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (as : Batteries.AssocList α β),
  as.toListTR = (Batteries.AssocList.foldl (fun r a b => r.push (a, b)) #[] as).toList
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_eq_half_of_head : ∀ {α : Type u_1} {s t : Stream'.Seq α}, s.head = t.head → dist s t = 2⁻¹ * dist s.tail t.tail
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restriction.sc'Iso_hom_τ₁ : ∀ {ι : 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] (i j k : ι) {i' j' k' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k'),
  (HomologicalComplex.restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom.τ₁ = (K.restrictionXIso e hi').hom
-- Init.Data.List.Erase
List.Nodup.eraseP : ∀ {α : Type u_1} {l : List α} (p : α → Bool), l.Nodup → (List.eraseP p l).Nodup
-- Mathlib.Condensed.Light.Functors
lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_hom_apply_apply : ∀ (X : LightProfinite) (X_1 : LightProfiniteᵒᵖ) (f : (lightProfiniteToLightCondSet.obj X).obj.obj X_1)
  (a : ↑(Opposite.unop X_1).toTop),
  ((CategoryTheory.ConcreteCategory.hom ((lightProfiniteToLightCondSetIsoTopCatToLightCondSet.hom.app X).hom.app X_1))
        f)
      a =
    (CategoryTheory.ConcreteCategory.hom f.hom) a
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.instFullRingObjCatForget₂RingObjCat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommRingObjCat.forget₂RingObjCat C).Full
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  (p.copy hu hv).IsPath ↔ p.IsPath
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_lemma : ∀ (n k : ℕ), ¬n < k * k → n.sqrt - k < n.sqrt + 2 - k
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.of_fixedPoints_eq : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L)
  [hGKL : IsGaloisGroup G K L], FixedPoints.intermediateField ↥H = F → IsGaloisGroup (↥H) (↥F) L
-- Init.Data.Vector.Lemmas
Vector.foldl_congr : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs ys : Vector α n},
  xs = ys → ∀ {f g : β → α → β}, f = g → ∀ {a b : β}, a = b → Vector.foldl f a xs = Vector.foldl g b ys
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.exists_Finpartition_sum_ge' : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : Set X} (hs : MeasurableSet s) {ε : ENNReal},
  0 < ε → MeasureTheory.preVariationFun f s ≠ ⊤ → ∃ P, MeasureTheory.preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ε
-- Mathlib.Data.Fintype.Sort
/-- Given a linearly ordered fintype `α` of cardinal `k`, the order isomorphism
`monoEquivOfFin α h` is the increasing bijection between `Fin k` and `α`. Here, `h` is a proof
that the cardinality of `α` is `k`. We use this instead of an isomorphism `Fin (card α) ≃o α` to
avoid casting issues in further uses of this function.  -/
monoEquivOfFin : (α : Type u_1) → [inst : Fintype α] → [inst_1 : LinearOrder α] → {k : ℕ} → Fintype.card α = k → Fin k ≃o α
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkLhsPrec.formatter : Lean.PrettyPrinter.Formatter