mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_iff_isSome_get? : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, a ∈ t ↔ (Std.DTreeMap.Internal.Impl.Const.get? t a).isSome = true
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.ker_eq_bot_of_mono : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) [CategoryTheory.Mono f], (ModuleCat.Hom.hom f).ker = ⊥
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.lift.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] (ι : Type u_2) [inst_1 : Preorder ι] (G : ι → Type u_3)
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_4 : DecidableEq ι] {P : Type u_4} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  (g g_1 : (i : ι) → G i →ₗ[R] P) (e_g : g = g_1)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x),
  Module.DirectLimit.lift R ι G f g Hg = Module.DirectLimit.lift R ι G f g_1 ⋯
-- Init.Data.String.Modify
/-- Replaces the character at position `p` in the string `s` with the result of applying `f` to that
character. If `p` is an invalid position, the string is returned unchanged.

If both the replacement character and the replaced character are 7-bit ASCII characters and the
string is not shared, then it is updated in-place and not copied.

This is a legacy function. The recommended alternative is `String.Pos.set`, combined with
`String.pos` or another means of obtaining a `String.Pos`.

Examples:
* `"abc".modify ⟨1⟩ Char.toUpper = "aBc"`
* `"abc".modify ⟨3⟩ Char.toUpper = "abc"`
 -/
String.modify : String → String.Pos.Raw → (Char → Char) → String
-- Mathlib.NumberTheory.FLT.Four
/-- To prove Fermat's Last Theorem, it suffices to prove it for odd prime exponents.
 -/
FermatLastTheorem.of_odd_primes : (∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p) → FermatLastTheorem
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.coe_neg_val_add_coe_val : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits ↥S}, ↑↑(-x) + ↑↑x = 0
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Coyoneda.instHasColimitObjOppositeFunctorTypeCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ),
  CategoryTheory.Limits.HasColimit (CategoryTheory.coyoneda.obj X)
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_apply_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Sₚ : Type u_4) [inst_4 : CommRing Sₚ] [inst_5 : Algebra S Sₚ]
  [inst_6 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [hPp : P.LiesOver p]
  [inst_7 : P.IsMaximal] (x : S),
  (IsLocalization.AtPrime.equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) x) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) ((algebraMap S Sₚ) x)
-- Mathlib.Data.EReal.Operations
EReal.toENNReal_sub : ∀ {x y : EReal}, 0 ≤ y → (x - y).toENNReal = x.toENNReal - y.toENNReal
-- Init.System.IO
IO.FS.FileType.file.sizeOf_spec : sizeOf IO.FS.FileType.file = 1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
_private.Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing.0.AlgebraicGeometry.PresheafedSpace.GlueData.«term𝖣» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Gluing
/-- The open cover of the glued space given by the glue data.  -/
AlgebraicGeometry.Scheme.GlueData.openCover : (D : AlgebraicGeometry.Scheme.GlueData) → D.glued.OpenCover
-- Lean.Data.KVMap
Lean.KVMap.isEmpty : Lean.KVMap → Bool
-- Mathlib.Algebra.Group.TransferInstance
Equiv.mulEquiv_symm_apply : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Mul β] (b : β), (MulEquiv.symm e.mulEquiv) b = e.symm b
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeight.eq_def : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_3} [inst_1 : AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) (x x_1 : V)
  (x_2 : Quiver.Path x x_1),
  Quiver.Path.addWeight w x_2 =
    match x, x_1, x_2 with
    | a, .(a), Quiver.Path.nil => 0
    | a, x, p.cons e => Quiver.Path.addWeight (fun {i j} => w) p + w e
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Typeclass for monotonicity of multiplication by nonnegative elements on the right,
namely `a₁ ≤ a₂ → a₁ * b ≤ a₂ * b` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedRing`.  -/
MulPosMono : (α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
-- Lean.Environment
_private.Lean.Environment.0.Lean.RealizationContext.mk.sizeOf_spec : ∀ (env : NonScalar) (opts : Lean.Options) (realizeMapRef : IO.Ref (Lean.NameMap NonScalar)),
  sizeOf { env := env, opts := opts, realizeMapRef := realizeMapRef } =
    1 + sizeOf env + sizeOf opts + sizeOf realizeMapRef
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
/-- `f +ᵣ g` is the composite `X ⟶ X ⊞ X ⟶ Y`, where the first map is `(𝟙, 𝟙)` and the second map
is `(f g)`.  -/
CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] → (X Y : C) → (X ⟶ Y) → (X ⟶ Y) → (X ⟶ Y)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Y Y' Z : C}
  [inst_2 : CategoryTheory.ExactPairing Y Y'] (f : Y' ⟶ Z),
  (CategoryTheory.tensorLeftHomEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y Y' Z).symm
      (CategoryTheory.CategoryStruct.comp (η_ Y Y') (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y').hom f
-- Mathlib.Data.Set.Sups
Set.empty_infs : ∀ {α : Type u_2} [inst : SemilatticeInf α] {t : Set α}, ∅ ⊼ t = ∅
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balancedAtRoot_one_one : Std.DTreeMap.Internal.Impl.BalancedAtRoot 1 1
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IicExtend_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β) (x : α),
  Set.IicExtend f x = f ⟨min b x, ⋯⟩
-- Mathlib.Order.Filter.Finite
Filter.sInter_mem : ∀ {α : Type u} {f : Filter α} {s : Set (Set α)}, s.Finite → (⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f)
-- Batteries.Data.Char.AsciiCasing
Char.not_isUpper_of_isLower : ∀ {c : Char}, c.isLower = true → ¬c.isUpper = true
-- Mathlib.Order.Hom.Lattice
/-- `Subtype.val` as a `LatticeHom`.  -/
LatticeHom.subtypeVal : {β : Type u_3} →
  [inst : Lattice β] →
    {P : β → Prop} →
      (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) →
        (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) → LatticeHom { x // P x } β
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.alter.eq_1 : ∀ {α : Type u_1} (cut : α → Ordering) (f : Option α → Option α) (t : RBTree.RBNode α),
  RBTree.RBNode.alter cut f t =
    match RBTree.RBNode.zoom cut t with
    | (RBTree.RBNode.nil, path) =>
      match f none with
      | none => t
      | some y => path.insertNew y
    | (RBTree.RBNode.node c a x b, path) =>
      match f (some x) with
      | none => path.del (a.append b) c
      | some y => path.fill (RBTree.RBNode.node c a y b)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_ciInf_set : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set γ} {f : γ → α},
  BddBelow (f '' s) → s.Nonempty → e (⨅ i, f ↑i) = ⨅ i, e (f ↑i)
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
/-- **Alias** of the reverse direction of `associated_abs_right_iff`. -/
Associated.abs_right : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] {x y : R}, Associated x y → Associated x |y|
-- Mathlib.Analysis.Normed.Group.Real
enorm_eq_self : ∀ (x : ENNReal), ‖x‖ₑ = x
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.lt_rank_root : ∀ {self : Batteries.UnionFind} {x : ℕ}, self.rank x < self.rank (self.rootD x) ↔ self.parent x ≠ x
-- Mathlib.Algebra.Ring.Prod
/-- Swapping components as an equivalence of (semi)rings.  -/
RingEquiv.prodComm : {R : Type u_1} → {S : Type u_3} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R × S ≃+* S × R
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.eval₂_derivative_ne_zero : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] [Nontrivial S] (f : R →+* S)
  {p : Polynomial R},
  p.Separable → ∀ {x : S}, Polynomial.eval₂ f x p = 0 → Polynomial.eval₂ f x (Polynomial.derivative p) ≠ 0
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.fromCommLeftInv.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M),
  S.fromCommLeftInv = { toFun := S.fromLeftInv, map_one' := ⋯, map_mul' := ⋯ }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_eq_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {he : t ≠ ∅}, t.maxKey he = t.maxKey!
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.inter : ∀ {α : Type u_1} {s t : Set α} {P : α → Prop} [inst : LE α],
  IsRelLowerSet s P → IsRelLowerSet t P → IsRelLowerSet (s ∩ t) P
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_le_size_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, m.size ≤ (m.insert k v).size
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.eq_empty_of_insertManyIfNewUnit_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ}, m.insertManyIfNewUnit l = ∅ → m = ∅
-- Init.Data.Nat.Div.Basic
Nat.div_one : ∀ (n : ℕ), n / 1 = n
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.algEquiv_commutes : ∀ {A : Type u_4} [inst : CommRing A] {B : Type u_6} [inst_1 : CommRing B] [inst_2 : Algebra A B] {K₁ : Type u_8}
  {K₂ : Type u_9} [inst_3 : Field K₁] [inst_4 : Field K₂] [inst_5 : Algebra A K₁] [inst_6 : Algebra A K₂]
  [IsFractionRing A K₁] {L₁ : Type u_10} {L₂ : Type u_11} [inst_8 : Field L₁] [inst_9 : Field L₂]
  [inst_10 : Algebra B L₁] [inst_11 : Algebra B L₂] [inst_12 : Algebra K₁ L₁] [inst_13 : Algebra K₂ L₂]
  [inst_14 : Algebra A L₁] [inst_15 : Algebra A L₂] [IsScalarTower A K₁ L₁] [IsScalarTower A K₂ L₂]
  [IsScalarTower A B L₁] [IsScalarTower A B L₂] (e : K₁ ≃ₐ[A] K₂) (f : L₁ ≃ₐ[B] L₂) (x : K₁),
  (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.finsetSum : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : AddCommMonoid β]
  [ContinuousAdd β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) →
    MeasureTheory.IsStronglyProgressive f fun i a => ∑ c ∈ s, U c i a
-- Init.Data.List.Lemmas
List.mem_cons_of_mem : ∀ {α : Type u_1} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: l
-- Mathlib.Analysis.Distribution.Distribution
/-- Note: we cannot express the full generality of `lineDerivCLM` purely in terms of this typeclass,
because (by design) the target type `𝓓^{k}_{K}(E, F)` is not determined by the input type
`𝓓^{n}_{K}(E, F)`.  -/
Distribution.instLineDerivTopENat : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_2} →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module ℝ F] →
              [inst_4 : TopologicalSpace F] →
                [IsTopologicalAddGroup F] → [ContinuousSMul ℝ F] → LineDeriv E (Distribution Ω F ⊤) (Distribution Ω F ⊤)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.irreducible_of_monic : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] {p : Polynomial R},
  p.Monic → p ≠ 1 → (Irreducible p ↔ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1)
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.coconesIsoComponentInv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J C} (Y : D)
  (t : (G.comp ((CategoryTheory.cocones J C).obj (Opposite.op K))).obj Y),
  adj.coconesIsoComponentInv Y t = { app := fun j => (adj.homEquiv (K.obj j) Y).symm (t.app j), naturality := ⋯ }
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- The canonical ring equivalence between `WithVal v` and `R`.  -/
WithVal.equiv : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → WithVal v ≃+* R
-- Mathlib.LinearAlgebra.Ray
SameRay.exists_pos_right : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, SameRay R x y → x ≠ 0 → y ≠ 0 → ∃ r, 0 < r ∧ x = r • y
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sup' : ∀ {C : Type u_2} [inst : AddCommGroup C] {s t : AddSubgroup C} {x : C}, x ∈ s ⊔ t ↔ ∃ y z, ↑y + ↑z = x
-- Mathlib.Data.Set.CoeSort
/-- Coercion from a set to the corresponding subtype.  -/
Set.instCoeSortType : {α : Type u} → CoeSort (Set α) (Type u)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_zsmul : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → AddGroup (G i)] [inst_7 : AddGroup C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), AddMonoidHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x : DirectLimit G f)
  (z : ℤ), DirectLimit.lift f (fun x => ⇑(g x)) h (z • x) = z • DirectLimit.lift f (fun x => ⇑(g x)) h x
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf : ∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α],
  f.IsCycle → ∀ {n : ℕ}, 0 < n → n < orderOf f → (f ^ n).support = f.support
-- Init.Data.List.Lemmas
List.getLastD_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {a : α}, (List.map f l).getLastD (f a) = f (l.getLastD a)
-- Lean.Data.LOption
Lean.instInhabitedLOption.default : {α : Type u} → Lean.LOption α
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_3.eq_2 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → Sort u_1) (b' : ONote) (h_1 : (f : ℕ → ONote) → motive (Sum.inr f))
  (h_2 : (b' : ONote) → motive (Sum.inl (some b'))) (h_3 : Unit → motive (Sum.inl none)),
  (match Sum.inl (some b') with
    | Sum.inr f => h_1 f
    | Sum.inl (some b') => h_2 b'
    | Sum.inl none => h_3 ()) =
    h_2 b'
-- Mathlib.Algebra.GCDMonoid.Basic
GCDMonoid.mk.congr_simp : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [toIsCancelMulZero : IsCancelMulZero α] (gcd gcd_1 : α → α → α)
  (e_gcd : gcd = gcd_1) (lcm lcm_1 : α → α → α) (e_lcm : lcm = lcm_1) (gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a)
  (gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b) (dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b)
  (gcd_mul_lcm : ∀ (a b : α), Associated (gcd a b * lcm a b) (a * b)) (lcm_zero_left : ∀ (a : α), lcm 0 a = 0)
  (lcm_zero_right : ∀ (a : α), lcm a 0 = 0),
  { toIsCancelMulZero := toIsCancelMulZero, gcd := gcd, lcm := lcm, gcd_dvd_left := gcd_dvd_left,
      gcd_dvd_right := gcd_dvd_right, dvd_gcd := dvd_gcd, gcd_mul_lcm := gcd_mul_lcm, lcm_zero_left := lcm_zero_left,
      lcm_zero_right := lcm_zero_right } =
    { toIsCancelMulZero := toIsCancelMulZero, gcd := gcd_1, lcm := lcm_1, gcd_dvd_left := ⋯, gcd_dvd_right := ⋯,
      dvd_gcd := ⋯, gcd_mul_lcm := ⋯, lcm_zero_left := ⋯, lcm_zero_right := ⋯ }
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.inv_head : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Group (G i)] {i j : ι} (w : Monoid.CoprodI.NeWord G i j),
  w.inv.head = w.last⁻¹
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- Given proofs
- that `a` is a natural number `m`
- that `b` is a nonnegative rational number `n / d`
- that `r ^ d = m ^ n` (written as `r ^ d = k`, `m ^ n = l`, `k = l`)

prove that `a ^ b = r`.
 -/
Mathlib.Meta.NormNum.IsNat.rpow_isNNRat : ∀ {a b : ℝ} {m n d r : ℕ},
  Mathlib.Meta.NormNum.IsNat a m →
    Mathlib.Meta.NormNum.IsNNRat b n d →
      ∀ (k : ℕ), r ^ d = k → ∀ (l : ℕ), m ^ n = l → k = l → Mathlib.Meta.NormNum.IsNat (a ^ b) r
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The constant morphism from ⦋0⦌.  -/
SimplexCategory.const : (x y : SimplexCategory) → Fin (y.len + 1) → (x ⟶ y)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.ext : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f g : ↑(GenLoop N X x)),
  (∀ (y : N → ↑unitInterval), f y = g y) → f = g
-- Mathlib.RingTheory.OreLocalization.Basic
/-- Negation on the Ore localization is defined via negation on the numerator.  -/
OreLocalization.neg : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddGroup X] → [inst_3 : DistribMulAction R X] → OreLocalization S X → OreLocalization S X
-- Mathlib.Geometry.Manifold.Riemannian.Basic
eventually_norm_mfderivWithin_symm_extChartAt_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] (x : M),
  ∃ C > 0,
    ∀ᶠ (y : E) in nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I), ‖mfderiv[Set.range ↑I] ↑(extChartAt I x).symm y‖ < C
-- Mathlib.NumberTheory.NumberField.Units.Basic
/-- If `k` does not divide `torsionOrder` then there are no nontrivial roots of unity of
order dividing `k`.  -/
NumberField.Units.rootsOfUnity_eq_one : ∀ (K : Type u_1) [inst : Field K] {k : ℕ+},
  (↑k).Coprime (NumberField.Units.torsionOrder K) →
    ∀ {ζ : (NumberField.RingOfIntegers K)ˣ}, ζ ∈ rootsOfUnity (↑k) (NumberField.RingOfIntegers K) ↔ ζ = 1
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM_loop : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} {i : ℕ} [inst : Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α)
  (x : α) (h : i + 1 ≤ n + 1),
  Fin.foldrM.loop✝ (n + 1) f ⟨i + 1, h⟩ x = Fin.foldrM.loop✝ n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.swap_map_inr : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : D} {f : Sum.inr X ⟶ Sum.inr Y}, (CategoryTheory.Sum.swap C D).map f = f
-- Init.Data.UInt.Lemmas
UInt32.mul_succ : ∀ {a b : UInt32}, a * (b + 1) = a * b + a
-- Mathlib.Data.List.Sym
List.Subperm.sym2 : ∀ {α : Type u_1} {xs ys : List α}, xs.Subperm ys → xs.sym2.Subperm ys.sym2
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- A left distributive symmetric monoidal category is distributive.  -/
CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.SymmetricCategory C]
  [CategoryTheory.IsMonoidalLeftDistrib C], CategoryTheory.IsMonoidalDistrib C
-- Init.Data.SInt.Basic
/-- The smallest number that `ISize` can represent: `-2^(System.Platform.numBits - 1)`.  -/
ISize.minValue : ISize
-- Mathlib.Topology.Irreducible
IrreducibleSpace.mk : ∀ {X : Type u_3} [inst : TopologicalSpace X] [toPreirreducibleSpace : PreirreducibleSpace X],
  Nonempty X → IrreducibleSpace X
-- Mathlib.Computability.AkraBazzi.AkraBazzi
/-- The **Akra-Bazzi theorem**: `T ∈ Ω(n^p (1 + ∑_u^n g(u) / u^{p+1}))`  -/
AkraBazziRecurrence.isBigO_symm_asympBound : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), AkraBazziRecurrence.asympBound g a b =O[Filter.atTop] T
-- Batteries.Classes.Order
/-- `LawfulBCmp cmp` asserts that the `LE`, `LT`, `BEq` are all coherent with each other
and with `cmp`, describing a strict weak order (a linear order except for antisymmetry).  -/
Std.LawfulBCmp : {α : Type u_1} → [LE α] → [LT α] → [BEq α] → (α → α → Ordering) → Prop
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Lean.Loop.forIn.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b' : β) (h_1 : (b' : β) → motive (ForInStep.done b'))
  (h_2 : (b' : β) → motive (ForInStep.yield b')),
  (match ForInStep.yield b' with
    | ForInStep.done b' => h_1 b'
    | ForInStep.yield b' => h_2 b') =
    h_2 b'
-- Lean.Meta.Sym.SymM
/-- Issues found during symbolic computation. Accumulated across operations
within a `sym =>` block and reported when a tactic fails.
 -/
Lean.Meta.Sym.State.issues : Lean.Meta.Sym.State → List Lean.MessageData
-- Lean.Elab.Tactic.RCases
/-- Convert a list of patterns to a tuple pattern, but mapping `[p]` to `p` instead of `⟨p⟩`.  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.typed? : Lean.Syntax → Lean.Elab.Tactic.RCases.RCasesPatt → Option Lean.Term → Lean.Elab.Tactic.RCases.RCasesPatt
-- Std.Data.DHashMap.RawLemmas
/-- Simpler variant of `get!_filter` when `LawfulBEq` is available.  -/
Std.DHashMap.Raw.Const.get!_filter' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  [inst_3 : Inhabited β] {f : α → β → Bool} {k : α},
  m.WF →
    Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.filter f m) k =
      (Option.filter (f k) (Std.DHashMap.Raw.Const.get? m k)).get!
-- Std.Data.TreeSet.Basic
/-- Two tree sets are equivalent in the sense of Equiv iff all the values are equal.  -/
Std.TreeSet.Equiv : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Std.TreeSet α cmp → Prop
-- Mathlib.Algebra.Group.Semiconj.Units
AddSemiconjBy.addUnits_of_val : ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy ↑a ↑x ↑y → AddSemiconjBy a x y
-- Std.Internal.Do.Triple.Gadget
/-- Specification for `assertGadget`: the precondition requires both the assertion `as` and
the Heyting implication `as ⇨ post ⟨⟩`, ensuring the assertion holds and the postcondition
follows from it.  -/
Std.Internal.Do.Spec.assertGadget : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  {post : PUnit.{u + 1} → Pred} {epost : EPred} (name : Lean.Name) (as : Pred)
  [∀ (a : Pred), Lean.Order.PreservesSup (Lean.Order.meet a)],
  ⦃ Lean.Order.meet as (Lean.Order.himp as (post PUnit.unit)) ⦄ Std.Internal.Do.assertGadget name as ⦃ post; epost ⦄
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toTopologicalSpace_inf : ∀ {α : Type u} [inst : Group α] (x y : GroupTopology α),
  (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.kernelIsoKer_inv_comp_ι : ∀ {G H : AddCommGrpCat} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (AddCommGrpCat.kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) =
    AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).ker.subtype