mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x : β) (i : ℕ), ↑(CauSeq.const abv x) i = x
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.pre_comp_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {F : CategoryTheory.Functor C CategoryTheory.Cat} (G : CategoryTheory.Functor D C)
  {H : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ H) {E : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (K : CategoryTheory.Functor (CategoryTheory.Grothendieck H) E),
  (CategoryTheory.Grothendieck.pre F G).comp ((CategoryTheory.Grothendieck.map α).comp K) =
    (CategoryTheory.Grothendieck.map (G.whiskerLeft α)).comp ((CategoryTheory.Grothendieck.pre H G).comp K)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.val_inv_unitsEquivUnitsType_apply_coe : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : ↥S.units),
  ↑↑(S.unitsEquivUnitsType x)⁻¹ = (Units.coeHom M) (↑x)⁻¹
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] [inst_2 : SizeOf M]
  [inst_3 : SizeOf N] (toMulHom : M →ₙ* N) (isLocalizationMap : S.IsLocalizationMap toMulHom.toFun),
  sizeOf { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap } =
    1 + sizeOf toMulHom + sizeOf isLocalizationMap
-- Mathlib.GroupTheory.OrderOfElement
finEquivMultiples.eq_1 : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} (hx : IsOfFinAddOrder x),
  finEquivMultiples hx = Equiv.ofBijective (fun n => ⟨↑n • x, ⋯⟩) ⋯
-- Mathlib.Tactic.GCongr.Core
/-- The state used by `GCongrM`.  -/
Mathlib.Tactic.GCongr.State : Type
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.unit_app_unit_comp_map_η : ∀ {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} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (G.map (CategoryTheory.Functor.OplaxMonoidal.η F)) =
    CategoryTheory.Functor.LaxMonoidal.ε G
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
one_le_thickenedIndicator_apply : ∀ (X : Type u_2) [inst : PseudoEMetricSpace X] {δ : ℝ} (δ_pos : 0 < δ) {F : Set X} {x : X},
  x ∈ F → 1 ≤ (thickenedIndicator δ_pos F) x
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.inv_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Groupoid.inv f = CategoryTheory.inv f
-- Mathlib.Data.Set.Lattice.Image
Set.sInter_prod_sInter_subset : ∀ {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (T : Set (Set β)), ⋂₀ S ×ˢ ⋂₀ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.mk : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (toGenerators : Algebra.Generators R S ι) →
                (relation : σ → toGenerators.Ring) →
                  Ideal.span (Set.range relation) = toGenerators.ker → Algebra.Presentation R S ι σ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The data of a categorical commutative square over a cospan `F, G` with cone point `X` is
that of a functor `T : X ⥤ A`, a functor `L : X ⥤ C`, and a `CatCommSq T L F G`.
Note that this is *exactly* what an object of
`((whiskeringRight X A B).obj F) ⊡ ((whiskeringRight X C B).obj G)` is,
so `CatCommSqOver F G X` is in equivalent to
`((whiskeringRight X A B).obj F) ⊡ ((whiskeringRight X C B).obj G)`,
though it is defined separately for performance reasons.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            CategoryTheory.Functor A B →
              CategoryTheory.Functor C B →
                (X : Type u₄) →
                  [CategoryTheory.Category.{v₄, u₄} X] → Type (max (max (max (max (max (max u₁ u₃) u₄) v₁) v₂) v₃) v₄)
-- Mathlib.Data.Int.Bitwise
Int.one_shiftLeft : ∀ (n : ℕ), 1 <<< ↑n = ↑(2 ^ n)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x},
  V₁ =ᶠ[nhdsWithin x s] V →
    W₁ =ᶠ[nhdsWithin x s] W →
      x ∈ s → VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x
-- Mathlib.RingTheory.Coalgebra.TensorProduct
TensorProduct.counit_def : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid B] [inst_4 : Algebra R S] [inst_5 : Module R A]
  [inst_6 : Module S A] [inst_7 : Module R B] [inst_8 : IsScalarTower R S A] [inst_9 : CoalgebraStruct R B]
  [inst_10 : CoalgebraStruct S A],
  CoalgebraStruct.counit =
    ↑(TensorProduct.AlgebraTensorModule.rid R S S) ∘ₗ
      TensorProduct.AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit
-- Init.Data.String.Basic
String.Pos.offset_ofSliceFrom : ∀ {s : String} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos},
  (String.Pos.ofSliceFrom pos).offset = pos.offset.offsetBy p₀.offset
-- Mathlib.Order.UpperLower.Closure
lowerBounds_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, lowerBounds ↑(upperClosure s) = lowerBounds s
-- Mathlib.Data.Seq.Computation
/-- `thinkN c n` is the computation that delays for `n` ticks and then performs
computation `c`.  -/
Computation.thinkN : {α : Type u} → Computation α → ℕ → Computation α
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : Option β → Option β},
  (m.alter k f).contains k' = if (k == k') = true then (f m[k]?).isSome else m.contains k'
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instIsIsoHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} {f : M ⟶ N} [CategoryTheory.IsIso f], CategoryTheory.IsIso f.hom
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.homEquiv_symm_apply_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} (f : F X ⟶ F Y), (CategoryTheory.InducedCategory.homEquiv.symm f).hom = f
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.Pivot.length_listTransvecRow : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  (Matrix.Pivot.listTransvecRow M).length = r
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.mk.sizeOf_spec : ∀ {M : Type u_10} {N : Type u_11} [inst : Zero M] [inst_1 : Zero N] [inst_2 : SizeOf M] [inst_3 : SizeOf N]
  (toFun : M → N) (map_zero' : toFun 0 = 0), sizeOf { toFun := toFun, map_zero' := map_zero' } = 1 + sizeOf map_zero'
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.eq_1 : ∀ (α : Type u_1), WithZero α = Option α
-- Mathlib.Data.Set.Monotone
Function.monotoneOn_of_rightInvOn_of_mapsTo : ∀ {α : Type u_4} {β : Type u_5} [inst : PartialOrder α] [inst_1 : LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β}
  {s : Set α}, MonotoneOn φ t → Set.RightInvOn ψ φ s → Set.MapsTo ψ s t → MonotoneOn ψ s
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.sheafedSpaceMap_id : ∀ {R : CommRingCat},
  AlgebraicGeometry.Spec.sheafedSpaceMap (CategoryTheory.CategoryStruct.id R) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.sheafedSpaceObj R)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_add_fdiv_right : ∀ (a c : ℤ) {b : ℤ}, b ≠ 0 → (a * b + c).fdiv b = c.fdiv b + a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_le_of_neg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b c : α},
  b ≤ c → a < 0 → b + a < c
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, then `norm` and `algebraMap` commutes.
 -/
IntermediateField.LinearDisjoint.norm_algebraMap : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [FiniteDimensional F E],
  A.LinearDisjoint ↥B →
    A ⊔ B = ⊤ → ∀ (x : ↥B), (Algebra.norm ↥A) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.norm F) x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.containsThenInsertIfNew k v).1 = t.contains k
-- Mathlib.Order.Filter.ENNReal
NNReal.limsSup_of_not_isBounded : ∀ {f : Filter NNReal}, ¬Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f → f.limsSup = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.mem_degenerate_iff_notMem_nonDegenerate : ∀ (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })), x ∈ X.degenerate n ↔ x ∉ X.nonDegenerate n
-- Mathlib.Topology.Algebra.Group.Basic
continuous_inv_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G]
  [inst_3 : TopologicalSpace α] {f : α → G}, Continuous f⁻¹ ↔ Continuous f
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_monomial : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {d : σ →₀ ℕ} {c : R},
  m.Monic ((MvPolynomial.monomial d) c) ↔ c = 1
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tsnd_eq_snd_id' : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α β β' : Type u} (f : β → β'),
  Bitraversable.tsnd (pure ∘ f) = pure ∘ Bifunctor.snd f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_none : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α}, a ∉ m → Std.DHashMap.Const.get? m a = none
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_restrictScalars : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (R₀ : Type u_11)
  [inst_9 : CommSemiring R₀] [inst_10 : Algebra R₀ R] [inst_11 : Algebra R₀ A] [inst_12 : Algebra R₀ B]
  [inst_13 : IsScalarTower R₀ R A] [inst_14 : IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ), ⇑(↑R₀ f) = ⇑f
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse.success.injEq : ∀ {α : Type} (response response_1 : α),
  (Lean.Server.ServerRequestResponse.success response = Lean.Server.ServerRequestResponse.success response_1) =
    (response = response_1)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.HasWeakLimit.mk' : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C},
  Nonempty (CategoryTheory.Limits.WeakLimitCone F) → CategoryTheory.Limits.HasWeakLimit F
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_le_size_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t.size ≤ (t.insertIfNew k v).size
-- Mathlib.Analysis.RCLike.Basic
RCLike.isCauSeq_norm : ∀ {K : Type u_1} [inst : RCLike K] {f : ℕ → K}, IsCauSeq norm f → IsCauSeq abs (norm ∘ f)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The continuous `ℤ`-algebra isomorphism between `ℤ_[p]` and
`(primesEquiv.symm p).adicCompletionIntegers ℚ`.  -/
PadicInt.adicCompletionIntegersEquiv : (R : Type u_2) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      [inst_2 : Algebra R ℚ] →
        [inst_3 : IsFractionRing R ℚ] →
          [inst_4 : IsIntegralClosure R ℤ ℚ] →
            (p : Nat.Primes) →
              ℤ_[↑p] ≃A[ℤ]
                ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ
                    (Rat.HeightOneSpectrum.primesEquiv.symm p))
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_3.congr_eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) (h_1 : Unit → motive none)
  (h_2 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c))
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  cOpt = some c →
    (match cOpt with
      | none => h_1 ()
      | some c => h_2 c) ≍
      h_2 c
-- Lean.Exception
/-- Exception type used in most Lean monads  -/
Lean.Exception : Type
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.list_prod_comp : ∀ {R : Type u} [inst : CommSemiring R] (l : List (Polynomial R)) (q : Polynomial R),
  l.prod.comp q = (List.map (fun p => p.comp q) l).prod
-- Init.Data.SInt.Lemmas
ISize.succ_mul : ∀ {a b : ISize}, (a + 1) * b = a * b + b
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
selfAdjoint.joined_one_expUnitary : ∀ {A : Type u_1} [inst : CStarAlgebra A] (x : ↥(selfAdjoint A)), Joined 1 (selfAdjoint.expUnitary x)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_eq_self : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_update_sub : ∀ {R : Type u_1} [inst : Semiring R] {M' : Type u_5} [inst_1 : AddCommGroup M'] [inst_2 : Module R M'] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g' : M' [⋀^ι]→ₗ[R] N') (v' : ι → M')
  [inst_5 : DecidableEq ι] (i : ι) (x y : M'),
  g' (Function.update v' i (x - y)) = g' (Function.update v' i x) - g' (Function.update v' i y)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_map_self_eq_one : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [IsDedekindDomain S],
  Ideal.map (algebraMap R S) p ≠ ⊤ →
    Ideal.map (algebraMap R S) p ≠ ⊥ → p.ramificationIdx' (Ideal.map (algebraMap R S) p) = 1
-- Mathlib.Data.WSeq.Basic
/-- Get the nth element of `s`.  -/
Stream'.WSeq.get? : {α : Type u} → Stream'.WSeq α → ℕ → Computation (Option α)
-- Init.Data.Int.Order
Int.natAbs_sign : ∀ (z : ℤ), z.sign.natAbs = if z = 0 then 0 else 1
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : InfSet γ]
  (f : sInfHom β γ) (g : sInfHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_sum_measure : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {t : ℝ} {ι : Type u_3} {μ : ι → MeasureTheory.Measure Ω},
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) (MeasureTheory.Measure.sum μ) →
    ProbabilityTheory.mgf X (MeasureTheory.Measure.sum μ) t = ∑' (i : ι), ProbabilityTheory.mgf X (μ i) t
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_intCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocDiv hp a (b + ↑m * p) = toIocDiv hp a b + m
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.iSup_mk_le_mk_iUnion : ∀ {α : Type u} {ι : Type v} {f : ι → Set α}, ⨆ i, Cardinal.mk ↑(f i) ≤ Cardinal.mk ↑(⋃ i, f i)
-- Mathlib.Order.OrderDual
OrderDual.instLT : (α : Type u_2) → [h : LT α] → LT αᵒᵈ
-- Aesop.Util.UnorderedArraySet
Aesop.instInhabitedUnorderedArraySet : {a : Type u_1} → {a_1 : BEq a} → Inhabited (Aesop.UnorderedArraySet a)
-- Init.Data.String.Lemmas.StringOrder
String.instIsLinearOrder : Std.IsLinearOrder String
-- Mathlib.Order.Hom.Bounded
BotHom.instPartialOrder : {α : Type u_2} → {β : Type u_3} → [inst : Bot α] → [PartialOrder β] → [inst_2 : Bot β] → PartialOrder (BotHom α β)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
/-- A category has finite coproducts if there exists a colimit for every diagram
with shape `Discrete J`, where we have `[Fintype J]`.

We require this condition only for `J = Fin n` in the definition, then deduce a version for any
`J : Type*` as a corollary of this definition.
 -/
CategoryTheory.Limits.HasFiniteCoproducts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.SetTheory.ZFC.Class
/-- Convert a class into a conglomerate (a collection of classes)  -/
Class.classToCong : Class.{u} → Set Class.{u}
-- Lean.Elab.Do.Control
/-- Continuation of the surrounding `do` block; restored after the body.  -/
Lean.Elab.Do.EffectForwarder.origCont : Lean.Elab.Do.EffectForwarder → Lean.Elab.Do.DoElemCont
-- Std.Data.HashMap.Lemmas
Std.HashMap.all_eq_false_iff_exists_mem_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {p : α → β → Bool},
  m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p a m[a] = false
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.NonemptyCompacts.lipschitz_sup : ∀ {α : Type u_1} [inst : EMetricSpace α], LipschitzWith 1 fun p => p.1 ⊔ p.2
-- Batteries.Tactic.PrintDependents
/-- The cached results on visited constants.  -/
Batteries.Tactic.CollectDependents.State.result : Batteries.Tactic.CollectDependents.State → Lean.NameMap Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited β] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Const.get! (Std.DTreeMap.Const.insertMany t l) k = Std.DTreeMap.Const.get! t k
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The 1st face of a 2-simplex, as a morphism in the 2-truncated simplex category.  -/
SSet.Truncated.δ1₂ : { obj := { len := 1 }, property := SSet.Truncated.ι0₂._proof_5 } ⟶
  { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.instPreservesMonomorphismsSimplicialObjectChainComplexNatAlternatingFaceMapComplexOfHasPullbacks : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasPullbacks C], (AlgebraicTopology.alternatingFaceMapComplex C).PreservesMonomorphisms
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.self_le_maxKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (cmp k ((t.insertIfNew k v).maxKey ⋯)).isLE = true
-- Init.Data.Range.Polymorphic.Instances
/-- Creates a `HasSize α` from a `HasSize α` instance. If the latter is lawful
and certain other conditions hold, then the former is also lawful by
`Rxo.LawfulHasSize.of_closed`.
 -/
Std.Rxo.HasSize.ofClosed : {α : Type u_1} → [Std.Rxc.HasSize α] → Std.Rxo.HasSize α
-- Mathlib.Algebra.Group.Action.Hom
MulAction.compHom_smul_def : ∀ {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : Monoid E] [inst_1 : Monoid F] [inst_2 : MulAction F G]
  (f : E →* F) (a : E) (x : G), a • x = f a • x
-- Aesop.Util.Unfold
Aesop.unfoldManyStar : (Lean.Name → Option (Option Lean.Name)) → Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.NumberTheory.Dioph
Poly.instNeg : {α : Type u_1} → Neg (Poly α)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- A configuration in the TM2 model is a label (or `none` for the halt state), the state of
local variables, and the stacks. (Note that the stacks are not `ListBlank`s, they have a definite
size.)  -/
Turing.TM2.Cfg : {K : Type u_1} → (K → Type u_2) → Type u_3 → Type u_4 → Type (max (max (max u_1 u_2) u_3) u_4)
-- Lean.Parser.Attr
Lean.Parser.Attr.tactic_tag.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_set_ne_zero_iff : ∀ {α : Type u} {s : Set α}, Cardinal.mk ↑s ≠ 0 ↔ s.Nonempty
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.matrix_top : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n], RingCon.matrix n ⊤ = ⊤
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
derivWithin_const_rpow : ∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ} {a : ℝ},
  0 < a → DifferentiableWithinAt ℝ f s x → derivWithin (fun x => a ^ f x) s x = Real.log a * derivWithin f s x * a ^ f x
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : M → M')
  (V : (x : M') → TangentSpace I' x) (x : M), VectorField.mpullback I I' f V x = (mfderiv% f x).inverse (V (f x))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.inter_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∩ t₂).Equiv (t₃ ∩ t₄)
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.le_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : GroupWithZero G₀] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G₀ A]
  {S T : AddSubgroup A} {a : G₀}, a ≠ 0 → (S ≤ a • T ↔ a⁻¹ • S ≤ T)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_eq_one_of_map_localization`.

---

The converse is true when `S` is a Dedekind domain.
See `Ideal.ramificationIdx'_eq_one_iff_of_isDedekindDomain`.  -/
Ideal.ramificationIdx_eq_one_of_map_localization : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [inst_3 : P.IsPrime] [IsNoetherianRing S],
  Ideal.map (algebraMap R S) p ≤ P →
    P ≠ ⊥ →
      P.primeCompl ≤ nonZeroDivisors S →
        Ideal.map (algebraMap R (Localization.AtPrime P)) p = IsLocalRing.maximalIdeal (Localization.AtPrime P) →
          p.ramificationIdx' P = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasDerivWithinAt.csinh : ∀ {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) * f') s x
-- Init.Tactics
/-- * `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`,
  or else fails.
* `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses
  with inaccessible names to the given names.
* `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`.
 -/
Lean.Parser.Tactic.case : Lean.ParserDescr
-- Mathlib.Analysis.Convex.Between
Sbtw.eq_1 : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y z : P), Sbtw R x y z = (Wbtw R x y z ∧ y ≠ x ∧ y ≠ z)