mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.card_isUnramified_compl : ∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : NumberField K]
  [inst_4 : NumberField k] [IsGalois k K],
  {w | NumberField.InfinitePlace.IsUnramified k w}ᶜ.card =
    {w | NumberField.InfinitePlace.IsUnramifiedIn K w}ᶜ.card * (Module.finrank k K / 2)
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetAux_perm_powersetAux' : ∀ {α : Type u_1} {l : List α}, (Multiset.powersetAux l).Perm (Multiset.powersetAux' l)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_inverseImage_strictMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D),
  ((P.strictMap F).inverseImage F).strictMap F = P.strictMap F
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- The characteristic function is even.
 -/
ValueDistribution.characteristic_even : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {a : WithTop E},
  Function.Even (ValueDistribution.characteristic f a)
-- Batteries.Data.AssocList
/-- `O(n)`. Returns the first entry in the list whose entry satisfies `p`.  -/
Batteries.AssocList.findEntryP? : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → Batteries.AssocList α β → Option (α × β)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.surjective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), Function.Surjective ⇑e
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, m.contains a = true → m.getKey? a = some (m.getKey! a)
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comap_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (x : τ → R),
  MvPolynomial.comap (MvPolynomial.rename f) x = x ∘ f
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mul_mk'_eq_mk'_of_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x y : R) (z : ↥M),
  (algebraMap R S) x * IsLocalization.mk' S y z = IsLocalization.mk' S (x * y) z
-- Mathlib.Data.ENNReal.Basic
ENNReal.instOrderTop : OrderTop ENNReal
-- Mathlib.Tactic.GRewrite.Core
/-- The rewritten expression  -/
Mathlib.Tactic.GRewrite.GRewriteResult.eNew : Mathlib.Tactic.GRewrite.GRewriteResult → Lean.Expr
-- Mathlib.Data.Countable.Defs
/-- A type `α` is countable if there exists an injective map `α → ℕ`.  -/
Countable : Sort u → Prop
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose_eq : ∀ (n k : ℕ), n.multichoose k = (n + k - 1).choose k
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.Pair.ext_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} {inst : (i : ι) → Monoid (M i)} {i : ι} {x y : Monoid.CoprodI.Word.Pair M i},
  x = y ↔ x.head = y.head ∧ x.tail = y.tail
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`.  -/
AffineBasis.instMulAction : {ι : Type u_1} →
  {G : Type u_3} →
    {k : Type u_5} →
      {V : Type u_6} →
        [inst : AddCommGroup V] →
          [inst_1 : Ring k] →
            [inst_2 : Module k V] →
              [inst_3 : Group G] →
                [inst_4 : DistribMulAction G V] → [SMulCommClass G k V] → MulAction G (AffineBasis ι k V)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instCommRingOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : CommRing Mᵃᵒᵖ], DomAddAct.instCommRingOfAddOpposite = inst
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp.congr_simp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : CommSemiring R] (s s_1 : ℤˣ),
  s = s_1 → ∀ (A A_1 : Matrix n n R), A = A_1 → Matrix.detp s A = Matrix.detp s_1 A_1
-- Mathlib.Data.Set.Prod
Set.preimage_swap_prod : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.withConstants.congr_simp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S S_1 : L.Substructure M) (e_S : S = S_1) {A : Set M}
  (h : A ⊆ ↑S), S.withConstants h = S_1.withConstants ⋯
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.tensor.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (a : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a_1 : C),
  sizeOf (a.tensor a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Order.Basic
Sum.const_le_elim_iff : ∀ {β : Type u_3} {α₁ : Type u_5} {α₂ : Type u_6} [inst : LE β] {b : β} {v₁ : α₁ → β} {v₂ : α₂ → β},
  Function.const (α₁ ⊕ α₂) b ≤ Sum.elim v₁ v₂ ↔ Function.const α₁ b ≤ v₁ ∧ Function.const α₂ b ≤ v₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go : ℕ → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly
-- Mathlib.Condensed.Discrete.Colimit
/-- Auxiliary definition for `isoFinYoneda`.  -/
LightCondensed.isoFinYonedaComponents : (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] →
    (X : LightProfinite) →
      [Finite ↑X.toTop] → F.obj (Opposite.op X) ≅ ↑X.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
-- Mathlib.Data.List.AList
AList.insertRec.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {C : AList β → Sort u_1} (H0 : C ∅)
  (IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)) (c : Sigma β) (l : List (Sigma β))
  (h : (c :: l).NodupKeys),
  AList.insertRec H0 IH { entries := c :: l, nodupKeys := h } =
    ⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (AList.insertRec H0 IH { entries := l, nodupKeys := ⋯ }))
-- Mathlib.Algebra.Lie.Basis.Base
LieModule.Weight.IsZero.eq_1 : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : LieModule.Weight R L M), χ.IsZero = (⇑χ = 0)
-- Std.Internal.Parsec.String
_private.Std.Internal.Parsec.String.0.Std.Internal.Parsec.String.digitsCore.go.eq_def : ∀ {s : String} (it : s.Pos) (acc : ℕ),
  Std.Internal.Parsec.String.digitsCore.go✝ it acc =
    if h : ¬it.IsAtEnd then
      have candidate := it.get h;
      if '0' ≤ candidate ∧ candidate ≤ '9' then
        have digit := Std.Internal.Parsec.String.digitToNat✝ candidate;
        have acc := acc * 10 + digit;
        Std.Internal.Parsec.String.digitsCore.go✝ (it.next h) acc
      else (acc, it)
    else (acc, it)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_pos_of_pos_of_nonneg`.  -/
Right.add_pos_of_pos_of_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b : α},
  0 < a → 0 ≤ b → 0 < a + b
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instSub : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → Sub (ContDiffMapSupportedIn E F n K)
-- Mathlib.FieldTheory.Finite.Valuation
FiniteField.valuation_algebraMap_le_one : ∀ {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [inst : Field Fq] [Finite Fq] [inst_2 : Ring A] [inst_3 : Algebra Fq A]
  [inst_4 : LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ) (a : Fq), v ((algebraMap Fq A) a) ≤ 1
-- Lean.Meta.Basic
/-- Similar to `lambdaTelescope` but for lambda and let expressions.

- If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
- If `preserveNondep` is `false`, all `have`s are converted to `let`s.

See also `mapLambdaLetTelescope` for entering and rebuilding the telescope.
 -/
Lean.Meta.lambdaLetTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} → Lean.Expr → (Array Lean.Expr → Lean.Expr → n α) → optParam Bool false → optParam Bool true → n α
-- Mathlib.RingTheory.Ideal.Cotangent
/-- The equivalence of the two definitions of `I / I ^ 2`, either as the quotient of `I` or the
ideal of `R / I ^ 2`.  -/
Ideal.cotangentEquivIdeal : {R : Type u} → [inst : CommRing R] → (I : Ideal R) → I.Cotangent ≃ₗ[R] ↥I.cotangentIdeal
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Integrability in the change of variable formula for differentiable functions: if a real
function `f` is antitone and differentiable on a measurable set `s`, then a function
`g : ℝ → F` is integrable on `f '' s` if and only if `-f' x • g ∘ f` is integrable on `s` .  -/
MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      AntitoneOn f s →
        ∀ (g : ℝ → F),
          MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume ↔
            MeasureTheory.IntegrableOn (fun x => -f' x • g (f x)) s MeasureTheory.volume
-- Mathlib.Data.Setoid.Basic
/-- The kernel of the quotient map induced by an equivalence relation r equals r.  -/
Setoid.ker_mk_eq : ∀ {α : Type u_1} (r : Setoid α), Setoid.ker Quotient.mk'' = r
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C)
  (t : CategoryTheory.Limits.FormalCoproduct C) (s : (i : 𝒜) → f i ⟶ t)
  (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I),
  ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t).symm s).f p = (s p.fst).f p.snd
-- Mathlib.Algebra.Group.Units.Basic
RightCancelMonoid.eq_one_of_mul_right : ∀ {α : Type u} [inst : RightCancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 → a = 1
-- Mathlib.Data.Multiset.ZeroCons
/-- This is a `rfl` and `simp` version of `bot_eq_zero`.  -/
Multiset.bot_eq_zero : ∀ {α : Type u_1}, ⊥ = 0
-- Mathlib.Data.QPF.Univariate.Basic
QPF.P : (F : Type u → Type v) → [self : QPF F] → PFunctor.{u, u'}
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The pointwise division of finsets `s / t` is defined as `{x / y | x ∈ s, y ∈ t}` in locale
`Pointwise`.  -/
Finset.div : {α : Type u_2} → [DecidableEq α] → [Div α] → Div (Finset α)
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.hasDerivAtFilter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter (𝕜 × 𝕜)},
  HasDerivAt f f' x → L ≤ nhds x ×ˢ pure x → HasDerivAtFilter f f' L
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.instUniqueElemForall : {S : Type u_1} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {X : Type u_2} → [inst_2 : Fintype X] → [IsOrderedRing S] → [Unique X] → Unique ↑(stdSimplex S X)
-- Mathlib.Data.Int.GCD
intGCD_nsmul_eq_zero : ∀ {M : Type u_1} [inst : AddGroup M] {a : M} {m n : ℤ}, m.gcd n • a = 0 ↔ m • a = 0 ∧ n • a = 0
-- Mathlib.Tactic.Simproc.Divisors
_private.Mathlib.Tactic.Simproc.Divisors.0.Nat.properDivisors_ofNat.unsafe_impl_5 : ℕ → Lean.TransformStep
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_map_lid_symm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] (f : M →ₗ[R] M'),
  ↑(TensorProduct.assoc R M' R N).symm ∘ₗ TensorProduct.map f ↑(TensorProduct.lid R N).symm =
    TensorProduct.map (TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm) LinearMap.id
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
/-- For `P` a projective family of measures, we define an additive content on the measurable
cylinders, by setting `projectiveFamilyContent s = P I S` for `s = cylinder I S`, where `I` is
a finite set of indices and `S` is a measurable set in `Π i : I, α i`.  -/
MeasureTheory.projectiveFamilyContent : {ι : Type u_1} →
  {α : ι → Type u_2} →
    {mα : (i : ι) → MeasurableSpace (α i)} →
      {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} →
        MeasureTheory.IsProjectiveMeasureFamily P →
          MeasureTheory.AddContent ENNReal (MeasureTheory.measurableCylinders α)
-- Mathlib.RingTheory.Extension.Basic
/-- Given a commuting square
```
R --→ P -→ S
|          |
↓          ↓
R' -→ P' → S
```
A hom between `P` and `P'` is a ring homomorphism that makes the two squares commute.
 -/
Algebra.Extension.Hom : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          Algebra.Extension R S →
            {R' : Type u_1} →
              {S' : Type u_2} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      Algebra.Extension R' S' → [Algebra R R'] → [Algebra S S'] → Type (max u_3 w)
-- Lean.Meta.Sym.SymM
/-- Returns the internalized `Ordering.eq`.   -/
Lean.Meta.Sym.getOrderingEqExpr : Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_eq_norm_app_of_nonzero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : PadicSeq p}, ¬f ≈ 0 → ∃ k, f.norm = padicNorm p k ∧ k ≠ 0
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The linear equivalence between `ContinuousLinearMapWOT` and `ContinuousLinearMap`.  -/
ContinuousLinearMapWOT.linearEquiv : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          (S : Type u_5) →
                            [inst_8 : Semiring S] →
                              [inst_9 : Module S F] →
                                [inst_10 : SMulCommClass 𝕜₂ S F] →
                                  [inst_11 : ContinuousConstSMul S F] →
                                    [inst_12 : IsTopologicalAddGroup F] → (E →SWOT[σ] F) ≃ₗ[S] E →SL[σ] F
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.map_get_revPositionsFrom_endPos : ∀ {s : String.Slice},
  List.map (fun p => (↑p).get ⋯) (String.Slice.Model.revPositionsFrom s.endPos) = s.copy.toList.reverse
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.exists_conts_b_of_den : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K] {B : K},
  g.dens n = B → ∃ conts, g.conts n = conts ∧ conts.b = B
-- Mathlib.Analysis.SpecialFunctions.Arsinh
HasDerivAt.arsinh : ∀ {f : ℝ → ℝ} {a f' : ℝ}, HasDerivAt f f' a → HasDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [Inhabited α] {k : α} {f : β → β} {h : k ∈ m.modify k f}, (m.modify k f).getKey k h = k
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_intCast : ∀ (x : ℂ) (n : ℤ), x ^ ↑n = x ^ n
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.min_firstDiff_le : ∀ {E : ℕ → Type u_1} (x y z : (n : ℕ) → E n),
  x ≠ z → min (PiNat.firstDiff x y) (PiNat.firstDiff y z) ≤ PiNat.firstDiff x z
-- Init.Data.Nat.Basic
Nat.zero_lt_sub_of_lt : ∀ {i a : ℕ}, i < a → 0 < a - i
-- Mathlib.Algebra.Group.Commute.Units
Units.commute_iff_mul_inv_cancel : ∀ {M : Type u_1} [inst : Monoid M] {u : Mˣ} {a : M}, Commute (↑u) a ↔ ↑u * a * ↑u⁻¹ = a
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The `p`-adic valuation of `m` equals zero if it is between `p * k` and `p * (k + 1)` for
some `k`.  -/
padicValNat_eq_zero_of_mem_Ioo : ∀ {p m k : ℕ}, m ∈ Set.Ioo (p * k) (p * (k + 1)) → padicValNat p m = 0
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_le_encard_self : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} (A : Set X), Metric.coveringNumber ε A ≤ A.encard
-- Mathlib.Order.Cover
covBy_iff_wcovBy_and_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b ↔ a ⩿ b ∧ a < b
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_solve_combine' : ∀ {x d₁ a₁ p₁ d₂ a₂ p₂ α β d : ℤ},
  α * a₁ * d₂ + β * a₂ * d₁ = d → d₁ ∣ a₁ * x + p₁ → d₂ ∣ a₂ * x + p₂ → d₁ * d₂ ∣ d * x + α * d₂ * p₁ + β * d₁ * p₂
-- Mathlib.Analysis.Normed.Ring.Units
/-- The function `fun t ↦ Ring.inverse (x + t) - x⁻¹` is `O(t)` as `t → 0`.  -/
NormedRing.inverse_add_norm_diff_first_order : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ),
  (fun t => Ring.inverse (↑x + t) - ↑x⁻¹) =O[nhds 0] fun t => ‖t‖
-- Mathlib.CategoryTheory.Category.KleisliCat
CategoryTheory.KleisliCat.ext : ∀ {m : Type u → Type v} [inst : Monad m] (α β : CategoryTheory.KleisliCat m) (f g : α ⟶ β),
  (∀ (x : α), f x = g x) → f = g
-- Init.Data.SInt.Basic
/-- Subtracts one word-sized signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.sub : ISize → ISize → ISize
-- Mathlib.Order.Antichain
/-- An antichain is a set such that no two distinct elements are related.  -/
IsAntichain : {α : Type u_1} → (α → α → Prop) → Set α → Prop
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.of_boundedUnder_abs_im : ∀ {l : Filter ℂ},
  Filter.Tendsto Complex.re l Filter.atTop →
    (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun z => |z.im|) → Complex.IsExpCmpFilter l
-- Init.Data.Int.DivMod.Bootstrap
Int.sub_emod : ∀ (a b n : ℤ), (a - b) % n = (a % n - b % n) % n
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.instToJsonCallHierarchy : Lean.ToJson Lean.Lsp.Ipc.CallHierarchy
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : EInt} (f : X ⟶ Y) (j : C),
  ((t.eTriangleLTGE.map f).app j).hom₃ = (t.eTruncGE.map f).app j
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.coe_toLinearMap : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁ →qᵢ Q₂), ⇑f.toLinearMap = ⇑f
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.Basis.sumQuot_repr_inl_of_mem : ∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (v : V) (hv : v ∈ W) (i : m),
  ((bW.sumQuot bQ).repr v) (Sum.inl i) = (bW.repr ⟨v, hv⟩) i
-- Mathlib.Order.PiLex
Pi.Colex.isStrictOrder : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (a : ι) → PartialOrder (β a)],
  IsStrictOrder (Colex ((i : ι) → β i)) fun x1 x2 => x1 < x2
-- Lean.Language.Basic
Lean.Language.instToSnapshotTreeSnapshotLeaf : Lean.Language.ToSnapshotTree Lean.Language.SnapshotLeaf
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescr : Type
-- Mathlib.Combinatorics.Matroid.Map
Matroid.eq_of_restrictSubtype_eq : ∀ {α : Type u_1} {E : Set α} {M N : Matroid α}, M.E = E → N.E = E → M.restrictSubtype E = N.restrictSubtype E → M = N
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_symm_stdSimplex_id : ∀ (n : SimplexCategory),
  SSet.yonedaEquiv.symm (SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id n)) =
    CategoryTheory.CategoryStruct.id (SSet.stdSimplex.obj n)
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- Every nonarchimedean ring is naturally a nonarchimedean additive group.  -/
NonarchimedeanRing.to_nonarchimedeanAddGroup : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : TopologicalSpace R] [t : NonarchimedeanRing R], NonarchimedeanAddGroup R
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.AsSmall.down_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.AsSmall C} (f : X ⟶ Y),
  CategoryTheory.AsSmall.down.map f = f.down
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_of_comp_left : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i]
  [inst_4 : ∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ] [hφφ' : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')],
  QuasiIso φ'
-- Init.Data.List.Erase
List.eraseP_filter : ∀ {α : Type u_1} {p f : α → Bool} {l : List α},
  List.eraseP p (List.filter f l) = List.filter f (List.eraseP (fun x => p x && f x) l)
-- Init.Data.Bool
Bool.not'.eq_1 : ∀ (a : Bool), a.not' = Bool.rec true false a
-- Mathlib.Control.Bitraversable.Instances
Bicompr.bitraverse.eq_1 : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] (F : Type u → Type u) [inst_1 : Traversable F]
  {m : Type u → Type u} [inst_2 : Applicative m] {α β α' β' : Type u} (f : α → m β) (f' : α' → m β'),
  Bicompr.bitraverse F f f' = traverse (bitraverse f f')
-- Mathlib.Analysis.Calculus.DSlope
ContinuousAt.of_dslope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜}, ContinuousAt (dslope f a) b → ContinuousAt f b
-- Mathlib.Topology.Defs.Basic
isOpenQuotientMap_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  IsOpenQuotientMap f ↔ Function.Surjective f ∧ Continuous f ∧ IsOpenMap f
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeftObjIdIso_hom_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (X : CategoryTheory.Functor C E) (X_1 : C),
  (CategoryTheory.Functor.whiskeringLeftObjIdIso.hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instPreadditive : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Preadditive (DerivedCategory C)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (f : CategoryTheory.yoneda.obj X ⟶ F),
  CategoryTheory.yonedaEquiv f =
    (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) (CategoryTheory.CategoryStruct.id X)