mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.liftToTerminalUnique_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z)
  (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F)
  (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).inv.app X =
    (match X with
      | CategoryTheory.WithTerminal.of x => h.app x
      | CategoryTheory.WithTerminal.star => hG).inv
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {a : α} {c : ℕ},
  Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.emptyWithCapacity c) a = none
-- Mathlib.LinearAlgebra.RootSystem.Chain
/-- If `α = P.root i` and `β = P.root j` are linearly independent, this is the index of the root
`β - q • α` where `β - q • α, ..., β - α, β, β + α, ..., β + p • α` is the `α`-chain through `β`.

In the absence of linear independence, it takes a junk value.  -/
RootPairing.chainBotIdx : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [Finite ι] →
          [inst : CommRing R] →
            [CharZero R] →
              [IsDomain R] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : AddCommGroup N] →
                      [inst_6 : Module R N] → {P : RootPairing ι R M N} → [P.IsCrystallographic] → ι → ι → ι
-- Init.System.Platform
/-- Checks whether the current platform is Windows.
 -/
System.Platform.getIsWindows : Unit → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.add.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinOp.add = 1
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A simpler inductive constructor for `ℕ`-indexed cochain complexes.

You provide explicitly the first differential,
then a function which takes a differential,
and returns the next object, its differential, and the fact it composes appropriately to zero.
 -/
CochainComplex.mk' : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ : V) →
        (X₀ ⟶ X₁) →
          ({X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0) →
            CochainComplex V ℕ
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.getTacSeqElems? : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → Option (Array (Lean.TSyntax `tactic))
-- Mathlib.Data.Fintype.BigOperators
/-- If a sum of a `Finset` of a subsingleton type has a given
value, so do the terms in that sum.  -/
Fintype.eq_of_subsingleton_of_sum_eq : ∀ {M : Type u_4} [inst : AddCommMonoid M] {ι : Type u_5} [Subsingleton ι] {s : Finset ι} {f : ι → M} {b : M},
  ∑ i ∈ s, f i = b → ∀ i ∈ s, f i = b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonCompIso.eq_1 : ∀ {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] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal],
  CategoryTheory.Functor.mapAddMonCompIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.AddMon.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapAddMon.obj X).X) ⋯ ⋯) ⋯
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_join_of_le_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.PartialOrder.rel P R → Lean.Order.PartialOrder.rel P (Lean.Order.join Q R)
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.id_mem : ∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H), OpenPartialHomeomorph.refl H ∈ G
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanModuleHierarchyImportedByParams.toJson : Lean.Lsp.LeanModuleHierarchyImportedByParams → Lean.Json
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α} {v : β k}, (m.insert k v).getKeyD k fallback = k
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, (t.erase k).getKeyD k fallback = fallback
-- Mathlib.Computability.TuringMachine.Tape
/-- Construct a tape from a list, with the head of the list at the TM head and the rest going
to the right.  -/
Turing.Tape.mk₁ : {Γ : Type u_1} → [inst : Inhabited Γ] → List Γ → Turing.Tape Γ
-- Init.Data.String.Defs
String.utf8ByteSize.eq_1 : ∀ (s : String), s.utf8ByteSize = s.toByteArray.size
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_two_nsmul_eq_sign_iff : ∀ {θ : Real.Angle}, (2 • θ).sign = θ.sign ↔ θ = ↑Real.pi ∨ |θ.toReal| < Real.pi / 2
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {y : P}, FractionalIdeal.spanSingleton S y = 0 ↔ y = 0
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.fix.injEq : ∀ (a a_1 : Turing.ToPartrec.Code), (a.fix = a_1.fix) = (a = a_1)
-- Init.Data.Vector.Lemmas
Vector.contains_toList : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {x : α}, xs.toList.contains x = xs.contains x
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.abel1 : Lean.ParserDescr
-- Init.Data.List.Lemmas
List.contains_map : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {l : List α} {x : β} {f : α → β},
  (List.map f l).contains x = l.any fun a => x == f a
-- Std.Http.Data.Body.Full
_private.Std.Http.Data.Body.Full.0.Std.Http.Body.Full.state : Std.Http.Body.Full → Std.Mutex (Option ByteArray)
-- Init.Data.Order.Ord
Std.LawfulBEqOrd.not_compare_eq_iff_beq_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Ord α} [Std.LawfulBEqOrd α] {a b : α}, ¬compare a b = Ordering.eq ↔ (a == b) = false
-- Mathlib.Data.Set.Image
Function.Surjective.range_comp : ∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} {f : ι → ι'},
  Function.Surjective f → ∀ (g : ι' → α), Set.range (g ∘ f) = Set.range g
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.φ_zero : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.φ 0 = 1
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_norm_expr : ∀ (ctx : Int.Internal.Linear.Context) (d : ℤ) (e : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  (p == e.norm) = true → d ∣ Int.Internal.Linear.Expr.denote ctx e → d ∣ Int.Internal.Linear.Poly.denote' ctx p
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_update_ne : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) {n i : ℕ} (a : R),
  i ≠ n → (p.update n a).coeff i = p.coeff i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂)[k]? = m₂[k]?.or m₁[k]?
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- The counit for the adjunction for `Cone.functoriality K G : Cone K ⥤ Cone (K ⋙ G)`.

Auxiliary definition for `functorialityAdjunction'`.
 -/
CategoryTheory.Adjunction.functorialityCounit' : {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 D) →
                    (CategoryTheory.Limits.Cone.functoriality K G).comp (adj.functorialityLeftAdjoint K) ⟶
                      CategoryTheory.Functor.id (CategoryTheory.Limits.Cone K)
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo : Type
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- Given an iterator `it` and a predicate `P`, `it.dropWhile P` is an iterator that
emits the values emitted by `it` starting from the first value that is rejected by `P`.
The elements before are dropped.

In situations where `P` is monadic, use `dropWhileM` instead.

**Marble diagram (ignoring monadic effects):**

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

```text
it               ---a----b---c--d-e--⊥
it.dropWhile P   ------------c--d-e--⊥

it               ---a----⊥
it.dropWhile P   --------⊥
```

**Termination properties:**

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

**Performance:**

This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.
 -/
Std.IterM.dropWhile : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → [inst : Monad m] → (P : β → Bool) → Std.IterM m β → Std.IterM m β
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- `AbsoluteValue R S` is the type of absolute values on `R` mapping to `S`:
the maps that preserve `*`, are nonnegative, positive definite and satisfy
the triangle inequality.  -/
AbsoluteValue : (R : Type u_5) → (S : Type u_6) → [Semiring R] → [Semiring S] → [PartialOrder S] → Type (max u_5 u_6)
-- Mathlib.Tactic.Widget.CommDiag
/-- If the expression is a function application of `fName` with 7 arguments, return those arguments.
Otherwise return `none`.  -/
Lean.Expr.app7? : Lean.Expr → Lean.Name → Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
mem_extChartAt_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), x ∈ (extChartAt I x).source
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.toReal_rnDeriv_tilted_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  MeasureTheory.Integrable (fun x => Real.exp (f x)) ν →
    (fun x => (μ.rnDeriv (ν.tilted f) x).toReal) =ᵐ[ν] fun x =>
      (Real.exp (-f x) * ∫ (x : α), Real.exp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_pred_self : ∀ {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ 0), (p.pred hp).predAbove p = p.pred hp
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.loop : (n : ℕ) →
  {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u} →
    ((i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯) → (j : ℕ) → j ≤ n → α (n - j) ⋯ → α n ⋯
-- Mathlib.GroupTheory.GroupAction.CardCommute
/-- **Class formula** for a finite group acting on a finite type. See
`MulAction.card_eq_sum_card_group_div_card_stabilizer` for a specialized version using
`Quotient.out`.  -/
MulAction.card_eq_sum_card_group_div_card_stabilizer' : ∀ (α : Type u_1) (β : Type u_2) [inst : Group α] [inst_1 : MulAction α β] [inst_2 : Fintype α] [inst_3 : Fintype β]
  [inst_4 : Fintype (Quotient (MulAction.orbitRel α β))] [inst_5 : (b : β) → Fintype ↥(MulAction.stabilizer α b)]
  {φ : Quotient (MulAction.orbitRel α β) → β},
  Function.LeftInverse Quotient.mk'' φ →
    Fintype.card β = ∑ ω, Fintype.card α / Fintype.card ↥(MulAction.stabilizer α (φ ω))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).getKey? k = if (f t[k]?).isSome = true then some k else none
-- Mathlib.Analysis.Seminorm
Seminorm.ball.eq_1 : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) (x : E) (r : ℝ), p.ball x r = {y | p (y - x) < r}
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.nonempty_of_neZero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [NeZero μ], Nonempty α
-- Mathlib.Algebra.Group.Pi.Basic
Pi.subtractionMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → SubtractionMonoid (f i)] → SubtractionMonoid ((i : I) → f i)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.unopUnop_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.unopUnop C).map f = f.unop.unop
-- Mathlib.NumberTheory.Height.Basic
/-- The nonarchimedean absolute values are indeed nonarchimedean.  -/
Height.AdmissibleAbsValues.isNonarchimedean : ∀ {K : Type u_1} {inst : Field K} [self : Height.AdmissibleAbsValues K],
  ∀ v ∈ Height.AdmissibleAbsValues.nonarchAbsVal, IsNonarchimedean ⇑v
-- Mathlib.Topology.Algebra.Order.Archimedean
AddSubgroup.dense_iff_ne_zmultiples : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] {s : AddSubgroup G},
  Dense ↑s ↔ ∀ (a : G), s ≠ AddSubgroup.zmultiples a
-- Mathlib.Algebra.WithConv
WithConv.ofConv_neg : ∀ {A : Type u_2} [inst : AddGroup A] (x : WithConv A), (-x).ofConv = -x.ofConv
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Any free group is isomorphic to "the" free group.  -/
IsFreeGroup.toFreeGroup : (G : Type u_1) → [inst : Group G] → [inst_1 : IsFreeGroup G] → G ≃* FreeGroup (IsFreeGroup.Generators G)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.coe_copy : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = ↑P), ↑(P.copy S hS) = S
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.VersionedTextDocumentIdentifier)
  (processing : Array Lean.Lsp.LeanFileProgressProcessingInfo),
  sizeOf { textDocument := textDocument, processing := processing } = 1 + sizeOf textDocument + sizeOf processing
-- Batteries.Data.MLList.Basic
/-- Constructs an `MLList` recursively, with state in `α`, recording terms from `β`.
If `f` returns `none` the list will terminate.

Variant of `MLList.fix?` that allows returning values of a different type.
 -/
MLList.fix?' : {m : Type (max u_1 u_2) → Type (max u_1 u_2)} →
  {α : Type u_2} → {β : Type (max u_1 u_2)} → [Monad m] → (α → m (Option (β × α))) → α → MLList m β
-- Mathlib.CategoryTheory.Galois.Basic
/-- `F.obj X` is connected if `X` is connected.  -/
CategoryTheory.PreGaloisCategory.PreservesIsConnected.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {D : Type v₁} {inst_1 : CategoryTheory.Category.{v₂, v₁} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.PreGaloisCategory.PreservesIsConnected F] {X : C}
  [CategoryTheory.PreGaloisCategory.IsConnected X], CategoryTheory.PreGaloisCategory.IsConnected (F.obj X)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.symm.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] {a b : Rack.PreEnvelGroup R} (hab : Rack.PreEnvelGroupRel' R a b),
  sizeOf hab.symm = 1 + sizeOf a + sizeOf b + sizeOf hab
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.pow_subset_pow_mul_of_sq_subset_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s t : Finset α} {n : ℕ},
  s ^ 2 ⊆ t * s → n ≠ 0 → s ^ n ⊆ t ^ (n - 1) * s
-- Mathlib.Topology.Connected.PathConnected
/-- If `f` is continuous and `F` is path-connected, so is `f(F)`.  -/
IsPathConnected.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Set X},
  IsPathConnected F → ∀ {f : X → Y}, Continuous f → IsPathConnected (f '' F)
-- Init.Data.Nat.Div.Lemmas
Nat.div_add_div_le_add_div : ∀ {x y z : ℕ}, x / z + y / z ≤ (x + y) / z
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_congr : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} {f g : G →* H} {φ : A ⟶ Rep.res f B} {ψ : A ⟶ Rep.res g B},
  f = g →
    (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap →
      groupHomology.chainsMap f φ = groupHomology.chainsMap g ψ
-- Mathlib.Algebra.Group.Int.Even
Int.two_mul_ediv_two_of_even : ∀ {n : ℤ}, Even n → 2 * (n / 2) = n
-- Mathlib.Data.Finset.Sym
Finset.sym_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (n : ℕ), ∅.sym (n + 1) = ∅
-- Mathlib.Topology.Algebra.GroupWithZero
Filter.Tendsto.div : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} {l : Filter α} {a b : G₀},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → b ≠ 0 → Filter.Tendsto (f / g) l (nhds (a / b))
-- Std.Time.DateTime
/-- Add `Minute.Offset` to a `DateTime`.
 -/
Std.Time.DateTime.addMinutes : Std.Time.DateTime → Std.Time.Minute.Offset → Std.Time.DateTime
-- Std.Http.Data.URI.Basic
Std.Http.URI.instToStringPath : ToString Std.Http.URI.Path
-- Mathlib.Data.Stream.Init
Stream'.mem_map : ∀ {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Stream' α}, a ∈ s → f a ∈ Stream'.map f s
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.toZeroHom_injective : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N], Function.Injective AddMonoidHom.toZeroHom
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is uniformly equicontinuous, then the limit is uniformly continuous.  -/
Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {l : Filter ι} [l.NeBot]
  {F : ι → β → α} {f : β → α}, Filter.Tendsto F l (nhds f) → UniformEquicontinuous F → UniformContinuous f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_le_size_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, (↑m).size - 1 ≤ (↑(m.alter k f)).size
-- Init.Data.Nat.Sqrt.Lemmas
Nat.lt_succ_sqrt : ∀ (n : ℕ), n < n.sqrt.succ * n.sqrt.succ
-- Mathlib.RingTheory.Extension.Generators
/-- The identity hom.  -/
Algebra.Generators.Hom.id : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Generators R S ι) → P.Hom P
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_le_mk_of_subset : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → Cardinal.mk ↑s ≤ Cardinal.mk ↑t
-- Mathlib.Data.Nat.Cast.Defs
/-- The canonical map `ℕ → R` sends `0 : ℕ` to `0 : R`.  -/
AddMonoidWithOne.natCast_zero : ∀ {R : Type u_2} [self : AddMonoidWithOne R], ↑0 = 0
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelUnopOp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.kernelUnopOp g).hom =
    (CategoryTheory.Limits.kernel.lift g.unop (CategoryTheory.Limits.cokernel.π g).unop ⋯).op
-- Batteries.Classes.Order
Std.TransOrd.instOn : ∀ {β : Type u_1} {α : Type u_2} [ord : Ord β] [Std.TransOrd β] (f : α → β), Std.TransOrd α
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `f` has a local max on `s` at `a` and `y` belongs to the positive tangent cone
of `s` at `a`, then `f' y ≤ 0`.  -/
IsLocalMaxOn.fderivWithin_nonpos : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E},
  IsLocalMaxOn f s a → y ∈ posTangentConeAt s a → (fderivWithin ℝ f s a) y ≤ 0
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Any morphism between terminal objects is an isomorphism.  -/
CategoryTheory.Limits.isIso_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (hX : CategoryTheory.Limits.IsTerminal X)
  (hY : CategoryTheory.Limits.IsTerminal Y) (f : X ⟶ Y), CategoryTheory.IsIso f
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq_spec_2 : ∀ (a : ℤ) (a_1 : Int.Internal.Linear.Var) (a_2 : Int.Internal.Linear.Poly) (b : ℤ) (b_1 : Int.Internal.Linear.Var)
  (b_2 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add a a_1 a_2 == Int.Internal.Linear.Poly.add b b_1 b_2) =
    (a == b && (a_1 == b_1 && a_2 == b_2))
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- See `ramificationIdx_tower` for a version that does not assume primality.  -/
Ideal.ramificationIdx_tower' : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [inst_7 : q.IsPrime] [inst_8 : r.IsPrime] [inst_9 : r.LiesOver q]
  [inst_10 : Algebra (Localization.AtPrime q) (Localization.AtPrime r)] [Localization.AtPrime.IsLiesOverAlgebra q r]
  [Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)],
  r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.M.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat),
  MonCat.FilteredColimits.M F = (F.comp (CategoryTheory.forget MonCat)).ColimitType
-- Lean.Language.Basic
Lean.Language.TransformedSnap.mk.injEq : ∀ {α : Type} (raw : α) (transform : Lean.Language.SnapshotTreeTransform) (raw_1 : α)
  (transform_1 : Lean.Language.SnapshotTreeTransform),
  ({ raw := raw, transform := transform } = { raw := raw_1, transform := transform_1 }) =
    (raw = raw_1 ∧ transform = transform_1)
-- Init.Data.Nat.Lemmas
Nat.mul_ne_zero_iff : ∀ {n m : ℕ}, n * m ≠ 0 ↔ n ≠ 0 ∧ m ≠ 0
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A variant of `Sieve.functorInclusion` with universe lifting.  -/
CategoryTheory.Sieve.uliftFunctorInclusion : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (S : CategoryTheory.Sieve X) → S.uliftFunctor ⟶ CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.eval.match_1.splitter : (motive : Lean.Data.AC.Expr → Sort u_1) →
  (x : Lean.Data.AC.Expr) →
    ((idx : ℕ) → motive (Lean.Data.AC.Expr.var idx)) → ((l r : Lean.Data.AC.Expr) → motive (l.op r)) → motive x
-- Std.Data.ExtTreeSet.Basic
/-- Monadically computes a value by folding the given function over the elements in the tree set in
descending order.
 -/
Std.ExtTreeSet.foldrM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} →
      {m : Type w → Type w₂} →
        [inst : Monad m] → [LawfulMonad m] → [Std.TransCmp cmp] → (α → δ → m δ) → δ → Std.ExtTreeSet α cmp → m δ