mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId b) =
    (F.mapComp f (CategoryTheory.CategoryStruct.id b)).symm ≪≫
      F.map₂Iso (CategoryTheory.Bicategory.rightUnitor f) ≪≫ (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm
-- Mathlib.Analysis.Normed.Field.Lemmas
NormedField.denseRange_nnnorm : ∀ (α : Type u_1) [inst : DenselyNormedField α], DenseRange nnnorm
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.trans_symm_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S') {E'' : Type u_5} [inst_4 : AddGroup E''] {S'' : AddGroupExtension N E'' G}
  (equiv' : S'.Equiv S'') (a : E''), (equiv.trans equiv').symm a = equiv.symm (equiv'.symm a)
-- Mathlib.GroupTheory.Torsion
/-- Quotienting a group by its torsion subgroup yields a torsion-free group.  -/
QuotientGroup.instIsMulTorsionFree : ∀ (G : Type u_1) [inst : CommGroup G], IsMulTorsionFree (G ⧸ CommGroup.torsion G)
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.QuasiIso.isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  [CategoryTheory.ShortComplex.QuasiIso φ], CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Data.Nat.Factorization.Basic
/-- If `p` is a prime factor of `b` then the power of `p` in `b` is the same that in `a * b`,
for any `a` coprime to `b`.  -/
Nat.factorization_eq_of_coprime_right : ∀ {p a b : ℕ}, a.Coprime b → p ∈ b.primeFactorsList → (a * b).factorization p = b.factorization p
-- Mathlib.FieldTheory.KummerExtension
/-- Suppose `L/K` is the splitting field of `Xⁿ - a`, then `Gal(L/K)` is isomorphic to the
roots of unity in `K` if `K` contains all of them.
Note that this does not depend on a choice of `ⁿ√a`.  -/
autEquivRootsOfUnity : {K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      (primitiveRoots n K).Nonempty →
        {a : K} →
          Irreducible (Polynomial.X ^ n - Polynomial.C a) →
            (L : Type u_1) →
              [inst_1 : Field L] →
                [inst_2 : Algebra K L] →
                  [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] →
                    [NeZero n] → Gal(L/K) ≃* ↥(rootsOfUnity n K)
-- Batteries.Lean.EStateM
EStateM.run'_tryFinally' : ∀ {ε σ α β : Type u_1} (x : EStateM ε σ α) (h : Option α → EStateM ε σ β) (s : σ),
  (tryFinally' x h).run' s =
    match x.run s with
    | EStateM.Result.ok a s => Option.map (fun x => (a, x)) ((h (some a)).run' s)
    | EStateM.Result.error a a_1 => none
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey? =
    some (t.maxKey?.elim k fun k' => if compare k' k = Ordering.lt then k else k')
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.innerAnodyneExtensions_pushoutObjObjι' : ∀ {X₁ X₂ Y₁ Y₂ : SSet} {i : X₁ ⟶ Y₁} {j : X₂ ⟶ Y₂}
  (sq₁₂ : (CategoryTheory.MonoidalCategory.curriedTensor SSet).PushoutObjObj i j) [CategoryTheory.Mono j],
  SSet.innerAnodyneExtensions i → SSet.innerAnodyneExtensions sq₁₂.ι
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientMapAddSubgroupOfOfLe_mk : ∀ {G : Type u} [inst : AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal]
  [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) (x : ↥A),
  (QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h) ↑x = ↑((AddSubgroup.inclusion h) x)
-- Mathlib.Topology.Separation.Hausdorff
/-- If `f x = g x` for all `x ∈ s` and `f`, `g` are continuous on `t`, `s ⊆ t ⊆ closure s`, then
`f x = g x` for all `x ∈ t`. See also `Set.EqOn.closure`.  -/
Set.EqOn.of_subset_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {s t : Set X}
  {f g : X → Y}, Set.EqOn f g s → ContinuousOn f t → ContinuousOn g t → s ⊆ t → t ⊆ closure s → Set.EqOn f g t
-- Mathlib.Data.EReal.Inv
EReal.inv_neg : ∀ (a : EReal), (-a)⁻¹ = -a⁻¹
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.mapArrowEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), (CategoryTheory.Functor.mapArrowEquivalence e).inverse = e.inverse.mapArrow
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_top : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  (f : MeasureTheory.SimpleFunc α E) (μ : MeasureTheory.Measure α), MeasureTheory.MemLp ⇑f ⊤ μ
-- Mathlib.Data.PSigma.Order
/-- The lexicographical `<` on a sigma type.  -/
PSigma.Lex.lt : {ι : Type u_1} → {α : ι → Type u_2} → [LT ι] → [(i : ι) → LT (α i)] → LT (Σₗ' (i : ι), α i)
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.totallyBounded_bot : ∀ {α : Type u} [uniformSpace : UniformSpace α], ⊥.TotallyBounded
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.TreeMap.getEntryGTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α × β → α × β
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- If `x₁ x₂ ... xₙ : A` then `R[x₁,x₂,...,xₙ]` is the `Subalgebra R A` generated by these elements.  -/
Algebra.subalgebra_adjoin : Lean.TrailingParserDescr
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for atomic non-structural 2-morphisms.  -/
Mathlib.Tactic.BicategoryLike.Atom : Type
-- Init.Data.SInt.Lemmas
Int64.neg_eq_neg_one_mul : ∀ (a : Int64), -a = -1 * a
-- Init.Data.SInt.Lemmas
ISize.ofInt_int32ToInt : ∀ (x : Int32), ISize.ofInt x.toInt = x.toISize
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- A basis' of an `IsRkFinite` set is finite.  -/
Matroid.IsRkFinite.finite_of_isBasis' : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsRkFinite X → M.IsBasis' I X → I.Finite
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerDone_flatMap : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β} {it₂ : Std.IterM m γ},
  it₂.IsPlausibleStep Std.IterStep.done →
    (Std.IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (Std.IterStep.skip (Std.IterM.flatMapAfter f it₁ none))
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.merge : ∀ {α : Type u_1} {le : α → α → Bool} {s₁ s₂ : Batteries.BinomialHeap.Imp.Heap α} {n : ℕ},
  Batteries.BinomialHeap.Imp.Heap.WF le n s₁ →
    Batteries.BinomialHeap.Imp.Heap.WF le n s₂ →
      Batteries.BinomialHeap.Imp.Heap.WF le n (Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Naturality of the oplax functoriality constraint, on the right.  -/
CategoryTheory.OplaxFunctor.mapComp_naturality_right_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X)
      ((self.mapComp f g').toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X)
      ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X))
-- Mathlib.Data.Finset.NAry
/-- Symmetric statement to `Finset.image_image₂_distrib_left`.  -/
Finset.image₂_image_left_comm : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
  [inst_1 : DecidableEq γ] {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {f : α' → β → γ} {g : α → α'}
  {f' : α → β → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f (g a) b = g' (f' a b)) →
    Finset.image₂ f (Finset.image g s) t = Finset.image g' (Finset.image₂ f' s t)
-- Mathlib.Data.Nat.Init
Nat.rec_one : ∀ {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)), Nat.rec h0 h 1 = h 0 h0
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.le_sub_of_le : ∀ {a b c : Ordinal.{u_4}}, b ≤ a → (c ≤ a - b ↔ b + c ≤ a)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.ext_iff : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {Q Q' : QuadraticMap R M N}, Q = Q' ↔ ∀ (x : M), Q x = Q' x
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorIso_def' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y X' Y' : C}
  (f : X ≅ Y) (g : X' ≅ Y'),
  CategoryTheory.MonoidalCategory.tensorIso f g =
    CategoryTheory.MonoidalCategory.whiskerLeftIso X g ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso f Y'
-- Mathlib.Combinatorics.Matroid.Map
Matroid.Indep.exists_eq_image_of_mapSetEmbedding : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : ↑M.E ↪ β} {I : Set β},
  (M.mapSetEmbedding f).Indep I → ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀
-- Mathlib.Algebra.Group.ForwardDiff
/-- **Gregory-Newton formula** expressing `f (y + n • h)` in terms of the iterated forward differences
of `f` at `y`.
 -/
shift_eq_sum_fwdDiff_iter : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f : M → G) (n : ℕ) (y : M),
  f (y + n • h) = ∑ k ∈ Finset.range (n + 1), n.choose k • (fwdDiff h)^[k] f y
-- Mathlib.Topology.MetricSpace.Isometry
/-- The natural `IsometryEquiv` `(Fin m → ℝ) × (Fin l → ℝ) ≃ᵢ (Fin n → ℝ)` when `m + l = n`.  -/
Fin.appendIsometryOfEq : {α : Type u} → [inst : PseudoEMetricSpace α] → {n m l : ℕ} → m + l = n → (Fin m → α) × (Fin l → α) ≃ᵢ (Fin n → α)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.eq_1 : ∀ {G : Type u_1} [inst : Mul G] (A B : Finset G) (a0 b0 : G),
  UniqueMul A B a0 b0 = ∀ ⦃a b : G⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0
-- Mathlib.Algebra.CubicDiscriminant
/-- The equivalence between cubic polynomials and polynomials of degree at most three.  -/
Cubic.equiv : {R : Type u_1} → [inst : Semiring R] → Cubic R ≃ { p // p.degree ≤ 3 }
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOnFilter.neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f : ι → β → α} {g : β → α},
  TendstoUniformlyOnFilter f g l l' → TendstoUniformlyOnFilter (-f) (-g) l l'
-- Mathlib.RingTheory.Localization.AsSubring
Localization.isFractionRing_range_mapToFractionRing : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] (B : Type u_3) [inst_4 : CommRing B] [inst_5 : Algebra A B]
  [inst_6 : IsLocalization S B] (hS : S ≤ nonZeroDivisors A),
  IsFractionRing (↥(Localization.mapToFractionRing K S B hS).range) K
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.addSubmonoidClass : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  AddSubmonoidClass (Submodule R M) M
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHomClass.toCoalgHomClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Algebra R A} {inst_3 : Semiring B} {inst_4 : Algebra R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : FunLike F A B} [self : BialgHomClass F R A B],
  CoalgHomClass F R A B
-- Mathlib.Order.Fin.Basic
Fin.val_strictMono : ∀ {n : ℕ}, StrictMono Fin.val
-- Init.Grind.AC
Lean.Grind.AC.Seq.endsWithVar_k_cons : ∀ (y x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq), (Lean.Grind.AC.Seq.cons y s).endsWithVar_k x = s.endsWithVar_k x
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- The embedding of a Lie-Rinehart subalgebra into the ambient space as a morphism of
Lie-Rinehart algebras.  -/
LieRinehartSubalgebra.incl : {A : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : LieRing L] →
        [inst_2 : Module A L] →
          (L' : LieRinehartSubalgebra A L) →
            [inst_3 : LieRingModule L A] →
              [inst_4 : LieRinehartRing A L] →
                (R : Type u_3) →
                  [inst_5 : CommRing R] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : LieAlgebra R L] →
                        [inst_8 : LieRinehartAlgebra R A L] → LieRinehartAlgebra.Hom (AlgHom.id R A) (↥L') L
-- Mathlib.NumberTheory.LucasLehmer
mersenne_zero : mersenne 0 = 0
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.brecOn_3.eq : ∀ {motive_1 : Mathlib.Tactic.Translate.ArgReorder → Sort u}
  {motive_2 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u}
  {motive_3 : List (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u}
  {motive_4 : ℕ × Mathlib.Tactic.Translate.ArgReorder → Sort u} (t : ℕ × Mathlib.Tactic.Translate.ArgReorder)
  (F_1 : (t : Mathlib.Tactic.Translate.ArgReorder) → t.below → motive_1 t)
  (F_2 :
    (t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) → Mathlib.Tactic.Translate.ArgReorder.below_1 t → motive_2 t)
  (F_3 :
    (t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) → Mathlib.Tactic.Translate.ArgReorder.below_2 t → motive_3 t)
  (F_4 : (t : ℕ × Mathlib.Tactic.Translate.ArgReorder) → Mathlib.Tactic.Translate.ArgReorder.below_3 t → motive_4 t),
  Mathlib.Tactic.Translate.ArgReorder.brecOn_3 t F_1 F_2 F_3 F_4 =
    F_4 t (Mathlib.Tactic.Translate.ArgReorder.brecOn_3.go t F_1 F_2 F_3 F_4).2
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.order_lt_iff_exists : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : Zero Γ] {x : HahnSeries Γ R} {i : Γ},
  x ≠ 0 → (x.order < i ↔ ∃ j < i, x.coeff j ≠ 0)
-- Mathlib.Data.Nat.Cast.Basic
/-- `Nat.cast : ℕ → α` as a `RingHom`  -/
Nat.castRingHom : (α : Type u_1) → [inst : NonAssocSemiring α] → ℕ →+* α
-- Std.Data.Iterators.Combinators.Drop
/-- Given an iterator `it` and a natural number `n`, `it.drop n` is an iterator that forwards all of
`it`'s output values except for the first `n`.

**Marble diagram:**

```text
it          ---a----b---c--d-e--⊥
it.drop 3   ---------------d-e--⊥

it          ---a--⊥
it.drop 3   ------⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

**Performance:**

Currently, this combinator incurs an additional O(1) cost with each output of `it`, even when the iterator
does not drop any elements anymore.
 -/
Std.Iter.drop : {α β : Type w} → ℕ → Std.Iter β → Std.Iter β
-- Mathlib.Analysis.RCLike.Basic
RCLike.pos_iff : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, 0 < z ↔ 0 < RCLike.re z ∧ RCLike.im z = 0
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- For `f : M →ₗ[R] A`, construct the algebra isomorphism `SymmetricAlgebra R M ≃ₐ[R] A`
from `IsSymmetricAlgebra f`.  -/
IsSymmetricAlgebra.equiv : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_3} →
            [inst_3 : CommSemiring A] →
              [inst_4 : Algebra R A] → {f : M →ₗ[R] A} → IsSymmetricAlgebra f → SymmetricAlgebra R M ≃ₐ[R] A
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_add_left_closedEBall : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ENNReal),
  (fun x => a + x) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (-a + b) r
-- Mathlib.Topology.Compactness.CompactSystem
/-- To prove that a set of sets is a compact system, it suffices to consider directed families of
sets.  -/
isCompactSystem_iff_of_directed : ∀ {α : Type u_1} {S : Set (Set α)},
  IsPiSystem S →
    (IsCompactSystem S ↔
      ∀ (C : ℕ → Set α), Directed (fun x1 x2 => x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.of_nat_of_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {f : ℤ → M},
  (Summable fun n => f ↑n) → (Summable fun n => f (-(↑n + 1))) → Summable f
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNatLT : ∀ {n : ℕ} {h : n < UInt64.size}, (UInt64.ofNatLT n h).toNat = n
-- Lean.Elab.App
Lean.Elab.Term.elabChoice : Lean.Elab.Term.TermElab
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.mergeWith : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ t₃ t₄ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t₁.Equiv t₂ →
    t₃.Equiv t₄ →
      ∀ (h₁ : t₁.WF) (h₂ : t₂.WF),
        t₃.WF →
          t₄.WF →
            ∀ {f : (a : α) → β a → β a → β a},
              (Std.DTreeMap.Internal.Impl.mergeWith f t₁ t₃ ⋯).impl.Equiv
                (Std.DTreeMap.Internal.Impl.mergeWith f t₂ t₄ ⋯).impl
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_eq_zero_iff_of_injective : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (p : MvPolynomial σ R) {f : σ → τ},
  Function.Injective f → ((MvPolynomial.rename f) p = 0 ↔ p = 0)
-- Mathlib.Analysis.Normed.Group.Pointwise
Bornology.IsBounded.div : ∀ {E : Type u_1} [inst : SeminormedGroup E] {s t : Set E},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s / t)
-- Lean.Elab.Term.TermElabM
/-- Save relevant context for term elaboration postponement.
 -/
Lean.Elab.Term.saveContext : Lean.Elab.TermElabM Lean.Elab.Term.SavedContext
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_iff_existsUnique : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G}, AddSubgroup.IsComplement S T ↔ ∀ (g : G), ∃! x, ↑x.1 + ↑x.2 = g
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
_private.Mathlib.RingTheory.WittVector.DiscreteValuationRing.0.WittVector.inverseCoeff.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.map_comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F G : CategoryTheory.Sheaf J AddCommGrpCat}
  (f : F ⟶ G) {n : ℕ} {G' : CategoryTheory.Sheaf J AddCommGrpCat} (g : G ⟶ G') (x : F.H n),
  (CategoryTheory.Sheaf.H.map (CategoryTheory.CategoryStruct.comp f g) n) x =
    (CategoryTheory.Sheaf.H.map g n) ((CategoryTheory.Sheaf.H.map f n) x)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
sInf_iUnion_Ici : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α),
  sInf (⋃ i, Set.Ici (f i)) = ⨅ i, f i
-- Mathlib.CategoryTheory.Sites.Point.Conservative
_private.Mathlib.CategoryTheory.Sites.Point.Conservative.0.CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk'.isLocallySurjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point} [CategoryTheory.LocallySmall.{w, v, u} C],
  (∀ ⦃X : C⦄ (S : CategoryTheory.Sieve X),
      (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
          ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (CategoryTheory.ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
        S ∈ J X) →
    ∀ {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [CategoryTheory.Mono f],
      (∀ (Φ : P.FullSubcategory),
          Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
        CategoryTheory.Presheaf.IsLocallySurjective J f
-- Mathlib.Order.LiminfLimsup
Filter.gt_mem_sets_of_limsInf_gt : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {f : Filter α} {b : α},
  Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f → b < f.limsInf → ∀ᶠ (a : α) in f, b < a
-- Init.PropLemmas
imp_and : ∀ {b c : Prop} {α : Sort u_1}, (∀ (a : α), b ∧ c) ↔ (∀ (a : α), b) ∧ ∀ (a : α), c
-- Init.Meta.Defs
Lean.Name.reprPrec : Lean.Name → ℕ → Std.Format
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to an `Int16`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toInt16 : Float.Model.UnpackedFloat → Int16
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bind_bind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : α → PMF β) (g : β → PMF γ),
  (p.bind f).bind g = p.bind fun a => (f a).bind g
-- Mathlib.Order.Partition.Finpartition
Finpartition.instPartialOrder : {α : Type u_1} → [inst : Lattice α] → [inst_1 : OrderBot α] → {a : α} → PartialOrder (Finpartition a)
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_eq_ofNat_of_nonpos : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (x : ℤ), x.ble' 0 = true → IntCast.intCast x = -OfNat.ofNat x.natAbs
-- Std.Net.Addr
Std.Net.MACAddr.mk.inj : ∀ {octets octets_1 : Vector UInt8 6}, { octets := octets } = { octets := octets_1 } → octets = octets_1
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
/-- The induced uniform structure of MvPolynomial σ R is an additive group uniform structure  -/
_private.Mathlib.RingTheory.MvPowerSeries.Evaluation.0.MvPowerSeries.instIsUniformAddGroupMvPolynomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] [IsUniformAddGroup R],
  IsUniformAddGroup (MvPolynomial σ R)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.find?.match_1.splitter : (s : String.Slice) →
  (motive : String.Slice.Pattern.SearchStep s → Sort u_1) →
    (x : String.Slice.Pattern.SearchStep s) →
      ((startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos)) →
        ((startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.rejected startPos endPos)) → motive x
-- Mathlib.GroupTheory.IsPerfect
/-- **Grün's lemma**  -/
Group.IsPerfect.center_quotient_center_eq_bot : ∀ (G : Type u_1) [inst : Group G] [Group.IsPerfect G], Subgroup.center (G ⧸ Subgroup.center G) = ⊥
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalNormedCommRing.mk : {α : Type u_5} →
  [toNonUnitalNormedRing : NonUnitalNormedRing α] → (∀ (a b : α), a * b = b * a) → NonUnitalNormedCommRing α
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk'.injEq : ∀ {X : SSet} (toS : X.S) (nonDegenerate : toS.simplex ∈ X.nonDegenerate toS.dim) (toS_1 : X.S)
  (nonDegenerate_1 : toS_1.simplex ∈ X.nonDegenerate toS_1.dim),
  ({ toS := toS, nonDegenerate := nonDegenerate } = { toS := toS_1, nonDegenerate := nonDegenerate_1 }) = (toS = toS_1)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffAt_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {x : M} {n : WithTop ℕ∞}
  [inst_11 : One M'], ContMDiffAt I I' n 1 x