mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.Exponential
selfAdjoint.expUnitary.congr_simp : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : ContinuousStar A]
  [inst_4 : CompleteSpace A] [inst_5 : StarModule ℂ A] (a a_1 : ↥(selfAdjoint A)),
  a = a_1 → selfAdjoint.expUnitary a = selfAdjoint.expUnitary a_1
-- Mathlib.Topology.EMetricSpace.Defs
/-- A `WeakPseudoEMetricSpace` is a topological space endowed with a `ℝ≥0∞`-value distance `edist`
which is *almost* an extended pseudometric space: the `edist` is reflexive, commutative and
satisfies the triangle inequality, but the topology on `α` need not *equal* the topology induced
by the `edist`. (It must be at least as fine, and agree with it on eballs of finite radius.)

This generalises both pseudo extended metric spaces and `ℝ≥0∞` (which have an extended distance,
which does not induce the order topology there).  -/
WeakPseudoEMetricSpace : (α : Type u) → [τ : TopologicalSpace α] → Type u
-- Mathlib.Data.Sym.Sym2
/-- Computably extract the element when known to be diagonal.  -/
Sym2.diagElem : {α : Type u_1} → (z : Sym2 α) → z.IsDiag → α
-- Std.Sync.CancellationToken
Std.CancellationToken.mk.inj : ∀ {state state_1 : Std.Mutex Std.CancellationToken.State}, { state := state } = { state := state_1 } → state = state_1
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The product in `CommRingCat` is the Cartesian product.  -/
CommRingCat.prodFanIsLimit : (A B : CommRingCat) → CategoryTheory.Limits.IsLimit (A.prodFan B)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite colimits, then `F.unop : C ⥤ D` reflects finite
limits.  -/
CategoryTheory.Limits.reflectsFiniteLimits_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteColimits F],
  CategoryTheory.Limits.ReflectsFiniteLimits F.unop
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.mk'.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x * y) = f x * f y),
  ContinuousMulEquiv.mk' f h = { toEquiv := f.toEquiv, map_mul' := h, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Lean.Elab.ConfigEval.Commands
/-- `ensure_eval_term_expr_instances t` is a macro for running both `ensure_eval_term_instance t`
and `ensure_eval_expr_instance t`, which ensurs there are `ConfigItem.EvalTerm t` and
`ConfigItem.EvalExpr t` instances by deriving one or more instances if it needs to.
 -/
Lean.Elab.ConfigEval.ensureEvalTermExprInstances : Lean.ParserDescr
-- Mathlib.Order.Booleanisation
/-- The order on `Booleanisation α` is as follows: For `a b : α`,
* `a < b` iff `a < b` in `α`
* `a < bᶜ` iff `a` and `b` are disjoint in `α`
* `aᶜ < bᶜ` iff `b < a` in `α`
* `¬ aᶜ < b`  -/
Booleanisation.instLT : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → LT (Booleanisation α)
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.stalk_open_algebraMap : ∀ {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {U : TopologicalSpace.Opens ↑X} (x : ↥U),
  algebraMap ↑(F.obj (Opposite.op U)) ↑(F.stalk ↑x) = CommRingCat.Hom.hom (F.germ U ↑x ⋯)
-- Std.Data.ExtTreeMap.Basic
/-- Returns `true` if the tree map contains no mappings.  -/
Std.ExtTreeMap.isEmpty : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.ExtTreeMap α β cmp → Bool
-- Init.Prelude
/-- The pseudo-kind assigned to identifiers: `` `ident ``.

The name `` `ident `` is not actually used as a kind for `Syntax.node` values. It is used by
convention as the kind of `Syntax.ident` values.
 -/
Lean.identKind : Lean.SyntaxNodeKind
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.image_neighborSet : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {v : V} (f : G ≃g G'),
  ⇑f '' G.neighborSet v = G'.neighborSet (f v)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mk.congr_simp : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] (toFun toFun_1 : X → Y) (e_toFun : toFun = toFun_1)
  (isLocallyConstant : IsLocallyConstant toFun),
  { toFun := toFun, isLocallyConstant := isLocallyConstant } = { toFun := toFun_1, isLocallyConstant := ⋯ }
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.toSubmodule_range : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), ↑f.range = (↑f).range
-- Mathlib.FieldTheory.IntermediateField.Basic
toSubalgebra_toIntermediateField : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : Subalgebra K L)
  (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S), (S.toIntermediateField inv_mem).toSubalgebra = S
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α],
  m.WF → ∀ {l : List α} {k : α}, k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKey! k = default
-- Mathlib.Tactic.NthRewrite
/-- `nth_rw` is a variant of `rw` that only changes the `n₁, ..., nₖ`ᵗʰ _occurrence_ of the expression
to be rewritten. Like `rw`, and unlike `nth_rewrite`, it will try to close the goal by trying `rfl`
afterwards. `nth_rw n₁ ... nₖ [eq₁, eq₂,..., eqₘ]` will rewrite the `n₁, ..., nₖ`ᵗʰ _occurrence_ of
each of the `m` equalities `eqᵢ`in that order. Occurrences are counted beginning with `1` in
order of precedence. For example,
```lean
example (h : a = 1) : a + a + a + a + a = 5 := by
  nth_rw 2 3 [h]
/-
a: ℕ
h: a = 1
⊢ a + 1 + 1 + a + a = 5
-/
```
Notice that the second and third occurrences of `a` from the left have been rewritten by
`nth_rw`.

To understand the importance of order of precedence, consider the example below
```lean
example (a b c : Nat) : (a + b) + c = (b + a) + c := by
  nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c
```
Here, although the occurrence parameter is `2`, `(a + b)` is rewritten to `(b + a)`. This happens
because in order of precedence, the first occurrence of `_ + _` is the one that adds `a + b` to `c`.
The occurrence in `a + b` counts as the second occurrence.

If a term `t` is introduced by rewriting with `eqᵢ`, then this instance of `t` will be counted as an
_occurrence_ of `t` for all subsequent rewrites of `t` with `eqⱼ` for `j > i`. This behaviour is
illustrated by the example below
```lean
example (h : a = a + b) : a + a + a + a + a = 0 := by
  nth_rw 3 [h, h]
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b + b) + a + a = 0
-/
```
Here, the first `nth_rw` with `h` introduces an additional occurrence of `a` in the goal. That is,
the goal state after the first rewrite looks like below
```lean
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b) + a + a = 0
-/
```
This new instance of `a` also turns out to be the third _occurrence_ of `a`.  Therefore,
the next `nth_rw` with `h` rewrites this `a`.

Further, `nth_rw` will close the remaining goal with `rfl` if possible.
 -/
Mathlib.Tactic.tacticNth_rw_____ : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.isIso_iff_of_mono : ∀ {n m : SimplexCategory} (f : n ⟶ m) [hf : CategoryTheory.Mono f], CategoryTheory.IsIso f ↔ n.len = m.len
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂FunctorObj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)),
  (CategoryTheory.bifunctorComp₁₂FunctorObj F₁₂).obj G = CategoryTheory.bifunctorComp₁₂ F₁₂ G
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sumInl_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S) (val : E.I₀), (E.sumInl F).s₀ val = Sum.inl val
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `AlgCat R`.  -/
AlgCat.of : (R : Type u) → [inst : CommRing R] → (X : Type v) → [inst_1 : Ring X] → [Algebra R X] → AlgCat R
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
WithLp.contDiff_toLp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {p : ENNReal}
  [inst_5 : Fact (1 ≤ p)] {n : WithTop ℕ∞}, ContDiff 𝕜 n (WithLp.toLp p)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map_apply_inr : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N') (x : N),
  (AddMonoid.Coprod.map f g) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inr (g x)
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_lt_top_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [I.FiniteHeight] [I.IsPrime], I.height < ⊤
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- Any bounded set is contained in a `BoxIntegral.Box` with integral vertices.  -/
BoxIntegral.le_hasIntegralVertices_of_isBounded : ∀ {ι : Type u_1} [Finite ι] {s : Set (ι → ℝ)}, Bornology.IsBounded s → ∃ B, BoxIntegral.hasIntegralVertices B ∧ s ⊆ ↑B
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.hasMFDerivAt : ∀ {𝕜 : 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) {x : H},
  HasMFDerivAt% (↑I) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.single_eq_of_ne : ∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {i i' : ι},
  i' ≠ i → ∀ (a : β i), (PiLp.single p i a).ofLp i' = 0
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.instIsLocallyInjectiveToSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [J.WEqualsLocallyBijective A] [inst_5 : CategoryTheory.HasWeakSheafify J A] (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
-- Mathlib.Logic.Relator
Relator.RightTotal.refl : ∀ {α : Type u_1} {r₁₁ : α → α → Prop}, (∀ (a : α), r₁₁ a a) → Relator.RightTotal r₁₁
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.op_nonneg : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {a : α}, 0 ≤ MulOpposite.op a ↔ 0 ≤ a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.filter_equiv_self_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {f : α → β → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter f m)).Equiv ↑m ↔
      ∀ (a : α) (h : m.contains a = true), f (m.getKey a h) (Std.DHashMap.Internal.Raw₀.Const.get m a h) = true)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.map_comap_eq_self : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] {f : L →ₐ[K] L'} {S : IntermediateField K L'},
  S ≤ f.fieldRange → IntermediateField.map f (IntermediateField.comap f S) = S
-- Mathlib.Logic.Denumerable
/-- A denumerable collection of denumerable types is denumerable.  -/
Denumerable.sigma : {α : Type u_1} → [Denumerable α] → {γ : α → Type u_3} → [(a : α) → Denumerable (γ a)] → Denumerable (Sigma γ)
-- Mathlib.Computability.TuringMachine.Tape
/-- The portion of the tape going off to the left.  -/
Turing.Tape.left : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.Tape Γ → Turing.ListBlank Γ
-- Init.Data.Int.Order
Int.sub_le_sub_right_iff : ∀ {a b c : ℤ}, a - c ≤ b - c ↔ a ≤ b
-- Mathlib.Algebra.Group.Hom.Defs
/-- The identity map from a type with addition to itself.  -/
AddHom.id : (M : Type u_10) → [inst : Add M] → M →ₙ+ M
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionAssocIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᴹᵒᵖ D] (x : D) (x_1 x_2 : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x x_1 x_2 =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso { unmop := x_2 } { unmop := x_1 } x
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.toTree : Lean.Syntax → Lean.Elab.TermElabM FBinopElab.Tree✝
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasure_smul : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {R : Type u_2} [inst_1 : SMul R NNReal] [inst_2 : SMul R ENNReal]
  [inst_3 : IsScalarTower R NNReal ENNReal] [inst_4 : IsScalarTower R ENNReal ENNReal] (c : R)
  (μ : MeasureTheory.FiniteMeasure Ω), ↑(c • μ) = c • ↑μ
-- Init.Data.List.Find
List.find?_replicate_of_neg : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α}, ¬p a = true → List.find? p (List.replicate n a) = none
-- Mathlib.Algebra.BigOperators.Finprod
/-- If the multiplicative support of `f` is finite, then for every `x` in the domain of `f`, `f x`
divides `finprod f`.  -/
finprod_mem_dvd : ∀ {α : Type u_1} {N : Type u_6} [inst : CommMonoid N] {f : α → N} (a : α),
  Function.HasFiniteMulSupport f → f a ∣ finprod f
-- Mathlib.Topology.ContinuousOn
/-- **Alias** of `continuousWithinAt_sdiff_self`.

---

See also `continuousWithinAt_sdiff_singleton` for the case of `s \ {y}`, but
requiring `T1Space α`.  -/
continuousWithinAt_diff_self : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : SizeOf α]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] (countdown : ℕ) (inner : Std.IterM m β)
  (finite : countdown > 0 ∨ Std.Iterators.Finite α m),
  sizeOf { countdown := countdown, inner := inner, finite := finite } =
    1 + sizeOf countdown + sizeOf inner + sizeOf finite
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a bounded order
with possibly different definitional equalities.  -/
BoundedOrder.copy : {α : Type u} →
  {h h' : LE α} →
    (c : BoundedOrder α) → (top : α) → top = ⊤ → (bot : α) → bot = ⊥ → (∀ (x y : α), x ≤ y ↔ x ≤ y) → BoundedOrder α
-- Mathlib.AlgebraicGeometry.Properties
/-- [Stacks Tag 02I4](https://stacks.math.columbia.edu/tag/02I4) -/
AlgebraicGeometry.coheight_eq_of_isOpenImmersion : ∀ {U X : AlgebraicGeometry.Scheme} {x : ↥U} (f : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion f],
  Order.coheight (f x) = Order.coheight x
-- Mathlib.Order.Filter.IsBounded
Filter.isBounded_ge_of_bot : ∀ {α : Type u_1} [inst : LE α] [OrderBot α] {f : Filter α}, Filter.IsBounded (fun x1 x2 => x2 ≤ x1) f
-- Init.Data.UInt.Lemmas
USize.le_total : ∀ (a b : USize), a ≤ b ∨ b ≤ a
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingProd_cons' : ∀ {G : Type u_7} [inst : CommGroup G] (a : G) (l : List G), (a :: l).alternatingProd = a * l.alternatingProd⁻¹
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor establishing the equivalence `StructuredArrow.preEquivalence`.  -/
CategoryTheory.StructuredArrow.preEquivalenceFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              {G : CategoryTheory.Functor D E} →
                {e : E} →
                  (f : CategoryTheory.StructuredArrow e G) →
                    CategoryTheory.Functor (CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G))
                      (CategoryTheory.StructuredArrow f.right F)
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.SparseCasesOnInfo.mk.inj : ∀ {indName : Lean.Name} {majorPos arity : ℕ} {insterestingCtors : Array Lean.Name} {indName_1 : Lean.Name}
  {majorPos_1 arity_1 : ℕ} {insterestingCtors_1 : Array Lean.Name},
  { indName := indName, majorPos := majorPos, arity := arity, insterestingCtors := insterestingCtors } =
      { indName := indName_1, majorPos := majorPos_1, arity := arity_1, insterestingCtors := insterestingCtors_1 } →
    indName = indName_1 ∧ majorPos = majorPos_1 ∧ arity = arity_1 ∧ insterestingCtors = insterestingCtors_1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_apply_of_isReal : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal)
  (x : NumberField.mixedEmbedding.mixedSpace K), (NumberField.mixedEmbedding.normAtPlace w) x = ‖x.1 ⟨w, hw⟩‖
-- Aesop.Stats.Basic
/-- Number of successful applications of a rule.
 -/
Aesop.RuleStatsTotals.numSuccessful : Aesop.RuleStatsTotals → ℕ
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
evalRingHom_mapMatrix_comp_polyToMatrix : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {S : Type u_3}
  [inst_3 : CommSemiring S] (f : S →+* Matrix n n R),
  (Polynomial.evalRingHom 0).mapMatrix.comp f.polyToMatrix = f.comp (Polynomial.evalRingHom 0)
-- Mathlib.Algebra.Algebra.Basic
algebraMap_comp_intCast : ∀ (R : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  ⇑(algebraMap R A) ∘ Int.cast = Int.cast
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.inducedStructure : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → (S : L.ElementarySubstructure M) → L.Structure ↥S
-- Mathlib.Data.Vector.Defs
List.Vector.instHAppendHAddNat : {α : Type u_1} → {n m : ℕ} → HAppend (List.Vector α n) (List.Vector α m) (List.Vector α (n + m))
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.toNNNorm : {E : Type u_2} → [NNNorm E] → NNNorm Eᵒᵈ
-- Mathlib.Data.Semiquot
Semiquot.mk'.injEq : ∀ {α : Type u_1} (s : Set α) (val : Trunc ↑s) (s_1 : Set α) (val_1 : Trunc ↑s_1),
  ({ s := s, val := val } = { s := s_1, val := val_1 }) = (s = s_1 ∧ val ≍ val_1)
-- Std.Sat.AIG.CNF
/-- The CNF within the state is unsat.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Unsat : {aig : Std.Sat.AIG ℕ} → Std.Sat.AIG.toCNF.State✝ aig → Prop
-- Init.Data.BitVec.Lemmas
BitVec.getLsb.eq_1 : ∀ {w : ℕ} (x : BitVec w) (i : Fin w), x.getLsb i = x.toNat.testBit ↑i
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_union_sdiff_cancel`. -/
Set.diff_union_diff_cancel : ∀ {α : Type u_1} {s t u : Set α}, t ⊆ s → u ⊆ t → s \ t ∪ t \ u = s \ u
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.instInhabitedMatchEqns : Inhabited Lean.Meta.Match.MatchEqns
-- Mathlib.NumberTheory.Padics.PadicNumbers
Int.padicValuation_self : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], (Int.padicValuation p) ↑p = WithZero.exp (-1)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.map_id : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.FreeGroupoid.map (CategoryTheory.Functor.id C) =
    CategoryTheory.Functor.id (CategoryTheory.FreeGroupoid C)
-- Mathlib.Data.Set.Operations
Function.Bijective.eq_1 : ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), Function.Bijective f = (Function.Injective f ∧ Function.Surjective f)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.gciMapComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f), Submonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls.match_1.eq_2 : ∀ (motive : Lean.Expr → Sort u_1) (x : Lean.Expr) (h_1 : (origFVar : Lean.FVarId) → motive (Lean.Expr.fvar origFVar))
  (h_2 : (x : Lean.Expr) → motive x),
  (∀ (origFVar : Lean.FVarId), x = Lean.Expr.fvar origFVar → False) →
    (match x with
      | Lean.Expr.fvar origFVar => h_1 origFVar
      | x => h_2 x) =
      h_2 x
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.homInhabited : {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.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.AddMonObj A] → (M : CategoryTheory.AddMod D A) → Inhabited (M.Hom M)
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.XIso.eq_1 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) {i : Option ι} {j : ι} (hj : i = some j),
  HomologicalComplex.extend.XIso K hj = CategoryTheory.eqToIso ⋯
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.addFieldInfo : Lean.SubExpr.Pos → Lean.Name → Lean.Name → Lean.Syntax → Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM Unit
-- Mathlib.Algebra.Order.Field.Basic
sub_inv_antitoneOn_Ioi : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {c : α},
  AntitoneOn (fun x => (x - c)⁻¹) (Set.Ioi c)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_add_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (z : ℤ),
  ⌈a + ↑z⌉ = ⌈a⌉ + z
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializedParams.mk.sizeOf_spec : sizeOf Lean.Lsp.InitializedParams.mk = 1
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsIntegrallyClosedIn R A] {x : A} {n : ℕ}, 0 < n → IsIntegral R (x ^ n) → ∃ y, (algebraMap R A) y = x