mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.degrees_sub_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] [inst_1 : DecidableEq σ] {p q : MvPolynomial σ R},
  (p - q).degrees ≤ p.degrees ∪ q.degrees
-- Mathlib.Combinatorics.SimpleGraph.Circulant
SimpleGraph.cycleGraph_eq_circulantGraph : ∀ (n : ℕ), SimpleGraph.cycleGraph (n + 1) = SimpleGraph.circulantGraph {1}
-- Init.System.IO
/-- Tries to acquire an exclusive or shared lock on the handle and returns `true` if successful. Will
not block if the lock cannot be acquired, but instead returns `false`.

Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it
works on Unix-like systems but not on Windows.
 -/
IO.FS.Handle.tryLock : IO.FS.Handle → optParam Bool true → IO Bool
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.singleton_eq_iff_domain : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : Y ⟶ X),
  CategoryTheory.Presieve.singleton f g ↔ f = g
-- Mathlib.Tactic.Module
/-- Given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s
and a natural number), recursively construct a proof that in the `$R`-module `$M`, the sum of the
"linear combinations" represented by `l₁` and `l₂` is the linear combination represented by
`Module.qNF.add iR l₁ l₁`.  -/
Mathlib.Tactic.Module.qNF.mkAddProof : {u v : Lean.Level} →
  {M : Q(Type v)} →
    {R : Q(Type u)} →
      {iR : Q(Semiring «$R»)} →
        {iM : Q(AddCommMonoid «$M»)} →
          (iRM : Q(Module «$R» «$M»)) →
            (l₁ l₂ : Mathlib.Tactic.Module.qNF R M) →
              have a := (Mathlib.Tactic.Module.qNF.add iR l₁ l₂).toNF;
              have a_1 := l₂.toNF;
              have a_2 := l₁.toNF;
              Q(«$a_2».eval + «$a_1».eval = «$a».eval)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z}
  {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f)
  (hc : CategoryTheory.Limits.IsColimit c) (b : α),
  CategoryTheory.CategoryStruct.comp (f.proj b).op (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom = c.inj b
-- Mathlib.Data.Seq.Defs
Stream'.Seq.head_eq_some : ∀ {α : Type u} {s : Stream'.Seq α} {x : α}, s.head = some x → s = Stream'.Seq.cons x s.tail
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃)
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
      (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ))
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSystem_toLinearMap_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (f : Module.Dual K ↥H) (x : ↥H),
  ((LieAlgebra.IsKilling.rootSystem H).toLinearMap f) x = f x
-- Aesop.BaseM
Aesop.BaseM.State.mk : Aesop.RulePatternCache → Aesop.Stats → Aesop.BaseM.State
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {a : α}, t.isEmpty = true → t.get! a = default
-- Mathlib.MeasureTheory.Measure.TightNormed
/-- In a finite-dimensional inner product space,
a set of measures `S` is tight if and only if the function `r ↦ ⨆ μ ∈ S, μ {x | r < |⟪y, x⟫|}`
tends to `0` at infinity for all `y`.  -/
MeasureTheory.isTightMeasureSet_iff_inner_tendsto : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : NormedAddCommGroup E]
  (𝕜 : Type u_2) [inst_1 : RCLike 𝕜] [inst_2 : InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E],
  MeasureTheory.IsTightMeasureSet S ↔
    ∀ (y : E), Filter.Tendsto (fun r => ⨆ μ ∈ S, μ {x | r < ‖inner 𝕜 y x‖}) Filter.atTop (nhds 0)
-- Init.Data.List.Lemmas
List.head_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α} (h : l₁ ≠ []), (l₁ ++ l₂).head ⋯ = l₁.head h
-- Lean.Setup
Lean.instInhabitedModuleSetup.default : Lean.ModuleSetup
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.predictablePart.eq_1 : ∀ {Ω : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m0 : MeasurableSpace Ω}
  (f : ℕ → Ω → E) (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω) (n : ℕ),
  MeasureTheory.predictablePart f ℱ μ n = ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | ↑ℱ i]
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.ext_iff : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommRing R] {m : R}
  {A B : FixedDetMatrix n R m}, A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j
-- Mathlib.CategoryTheory.Bicategory.Product
/-- `sectL B c` is the strictly unitary pseudofunctor `B ⥤ B × C` given by `X ↦ (X, c)`.  -/
CategoryTheory.Bicategory.Prod.sectL : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} → [inst_1 : CategoryTheory.Bicategory C] → C → CategoryTheory.StrictlyUnitaryPseudofunctor B (B × C)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsFunctor_map : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] {X Y : Rep.{u, u, u} k G} (f : X ⟶ Y),
  (groupHomology.chainsFunctor k G).map f = groupHomology.chainsMap (MonoidHom.id G) f
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.liftOfRightInverse.eq_1 : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : AddGroup G₃]
  (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f),
  f.liftOfRightInverse f_inv hf =
    { toFun := fun g => f.liftOfRightInverseAux f_inv hf ↑g ⋯, invFun := fun φ => ⟨φ.comp f, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.induction_add : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] (i : ι) {p : ι → Prop},
  (∀ (i : ι), p i → p ((P.reflectionPerm i) i)) →
    (∀ i ∈ b.support, p i) → (∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k) → p i
-- Mathlib.Analysis.Complex.Basic
Filter.tendsto_ofReal_iff : ∀ {α : Type u_2} {l : Filter α} {f : α → ℝ} {x : ℝ},
  Filter.Tendsto (fun x => ↑(f x)) l (nhds ↑x) ↔ Filter.Tendsto f l (nhds x)
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax.sizeOf_spec : ∀ {kind : Lean.SyntaxNodeKind} (a : Lean.TSyntax kind),
  sizeOf (Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax a) = 1 + sizeOf kind + sizeOf a
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Coalgebra.Repr.mul_index : ∀ {R : Type u_1} {A : Type u_2} {ι : Type u_4} {κ : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] {a b : A} (ℛ₁ : Coalgebra.Repr R a ι) (ℛ₂ : Coalgebra.Repr R b κ),
  (ℛ₁.mul ℛ₂).index = ℛ₁.index ×ˢ ℛ₂.index
-- Lean.Server.Rpc.Basic
/-- The address of an object in an `RpcObjectStore` that clients can refer to.
Its JSON encoding depends on the RPC wire format.

The language server may serve the same `RpcRef` multiple times.
It maintains a reference count to track how many times it has served the reference.
If clients want to release the object associated with an `RpcRef`,
they must release the reference as many times as they have received it from the server.
 -/
Lean.Lsp.RpcRef : Type
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_add_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
  f.eraseLead + Polynomial.C f.leadingCoeff * Polynomial.X ^ f.natDegree = f
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.leftRegular_projective : ∀ {k : Type u} [inst : CommRing k] {G : Type u} [inst_1 : Group G], CategoryTheory.Projective (Rep.leftRegular k G)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.comp_ofComplex_of_im_le_zero : ∀ (f : UpperHalfPlane → ℂ) (z z' : ℂ),
  z.im ≤ 0 → z'.im ≤ 0 → (f ∘ ↑UpperHalfPlane.ofComplex) z = (f ∘ ↑UpperHalfPlane.ofComplex) z'
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousWithinAt.norm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α}
  {a : α}, ContinuousWithinAt f s a → ContinuousWithinAt (fun x => ‖f x‖) s a
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.addEquivBoundedOfCompact_symm_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  [inst_3 : AddMonoid β] [inst_4 : LipschitzAdd β],
  ⇑(ContinuousMap.addEquivBoundedOfCompact α β).symm = ⇑(BoundedContinuousFunction.toContinuousMapAddMonoidHom α β)
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.Nat.Partrec.Code.pappAck.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.MeasureTheory.Integral.Lebesgue.Countable
/-- Markov's inequality for the counting measure with hypothesis using `tsum` in `ℝ≥0`.  -/
NNReal.count_const_le_le_of_tsum_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {a : α → NNReal},
  Measurable a →
    Summable a →
      ∀ {c : NNReal}, ∑' (i : α), a i ≤ c → ∀ {ε : NNReal}, ε ≠ 0 → MeasureTheory.Measure.count {i | ε ≤ a i} ≤ ↑c / ↑ε
-- Mathlib.Analysis.RCLike.Basic
RCLike.abs_re_div_norm_le_one : ∀ {K : Type u_1} [inst : RCLike K] (z : K), |RCLike.re z / ‖z‖| ≤ 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).maxKey? =
        Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.maxKey?
-- Init.Coe
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
or by double type ascription `((x : α) : β)`.  -/
CoeOTC.coe : {α : Sort u} → {β : Sort v} → [self : CoeOTC α β] → α → β
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_apply : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S)
  (I : FractionalIdeal (nonZeroDivisors R) K),
  (FractionalIdeal.ringEquivOfRingEquiv K L f) I =
    ⟨Submodule.map ↑(IsFractionRing.semilinearEquivOfRingEquiv K L f) ↑I, ⋯⟩
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.mem_rangeS_self : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (x : R),
  f x ∈ f.rangeS
-- Init.Data.Range.Polymorphic.PRange
/-- A range of elements of `α` with an open lower and upper bounds.

`a<...b` or `a<...<b` is the range of all values greater than `a : α` and less than
`b : α`. This is notation for `Roo.mk a b`.
 -/
Std.Roo : Type u → Type u
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.instCoeTCReal : CoeTC ℝ ℝ*
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.quasiIso_τ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂),
  S₁.ShortExact → S₂.ShortExact → QuasiIso φ.τ₁ → QuasiIso φ.τ₂ → QuasiIso φ.τ₃
-- Mathlib.Algebra.Order.Monoid.Basic
OrderEmbedding.mulLeft_apply : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : LinearOrder α] [inst_2 : MulLeftStrictMono α] (m n : α),
  (OrderEmbedding.mulLeft m) n = m * n
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.hasRightHomology_iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.HasRightHomology ↔ S.op.HasLeftHomology
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.instInjectiveXIntAsHomologicalComplexUpHomotopicObjPlusObjPlusQuotientInjectiveObjectMapCochainComplexPlusι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex.Plus (CategoryTheory.InjectiveObject C)) (n : ℤ),
  CategoryTheory.Injective
    (((HomotopyCategory.Plus.quotient C).obj
              ((CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus.obj K)).obj.as.X
      n)
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.IsQuasiAffine.toCompactSpace : ∀ {X : AlgebraicGeometry.Scheme} [self : X.IsQuasiAffine], CompactSpace ↥X
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₂.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.u₂✝ S = FermatLastTheoremForThreeGen.Solution.u₂✝ S_1
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_symm_some_below : ∀ {n : ℕ} {i : Fin (n + 1)} {m : Fin n}, m.castSucc < i → (finSuccEquiv' i).symm (some m) = m.castSucc
-- Mathlib.RingTheory.Idempotents
/-- The corner associated to an element `e` in a semigroup
is the subsemigroup of all elements of the form `e * r * e`.  -/
Subsemigroup.corner : {R : Type u_1} → R → [inst : Semigroup R] → Subsemigroup R
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey? k = none
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x` is an additive semigroup
if `β` is an additive semigroup.  -/
FunLike.addSemigroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Add F] → [inst_2 : AddSemigroup β] → [IsAddApply F α β] → AddSemigroup F
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.State.mk.injEq : ∀ (f fType : Lean.Expr) (namedArgs : List Lean.Elab.Term.NamedArg) (args : List Lean.Elab.Term.Arg)
  (instMVars : Array Lean.MVarId) (idx : ℕ) (motive? : Option Lean.Expr) (f_1 fType_1 : Lean.Expr)
  (namedArgs_1 : List Lean.Elab.Term.NamedArg) (args_1 : List Lean.Elab.Term.Arg) (instMVars_1 : Array Lean.MVarId)
  (idx_1 : ℕ) (motive?_1 : Option Lean.Expr),
  ({ f := f, fType := fType, namedArgs := namedArgs, args := args, instMVars := instMVars, idx := idx,
        motive? := motive? } =
      { f := f_1, fType := fType_1, namedArgs := namedArgs_1, args := args_1, instMVars := instMVars_1, idx := idx_1,
        motive? := motive?_1 }) =
    (f = f_1 ∧
      fType = fType_1 ∧
        namedArgs = namedArgs_1 ∧ args = args_1 ∧ instMVars = instMVars_1 ∧ idx = idx_1 ∧ motive? = motive?_1)
-- Mathlib.RingTheory.Jacobson.Radical
Module.jacobson_quotient_of_le : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M},
  N ≤ Module.jacobson R M → Module.jacobson R (M ⧸ N) = Submodule.map N.mkQ (Module.jacobson R M)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrCompHomotopy.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ i, c.Rel i j),
  HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc = HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_eq_false_iff_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {k : α}, m.contains k = false ↔ k ∉ m
-- Init.Core
Lean.Syntax.atom.inj : ∀ {info : Lean.SourceInfo} {val : String} {info_1 : Lean.SourceInfo} {val_1 : String},
  Lean.Syntax.atom info val = Lean.Syntax.atom info_1 val_1 → info = info_1 ∧ val = val_1
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.packingNumber_pos_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal}, 0 < Metric.packingNumber ε A ↔ A.Nonempty
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.pos_of_inv_pos : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a : R}, 0 < a⁻¹ → 0 < a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.alter t k f) k' =
    if cmp k k' = Ordering.eq then f (Std.ExtDTreeMap.Const.get? t k) else Std.ExtDTreeMap.Const.get? t k'
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.mk.injEq : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {E : Type u_11} {E₂ : Type u_12}
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (toLinearEquiv : E ≃ₛₗ[σ₁₂] E₂) (norm_map' : ∀ (x : E), ‖toLinearEquiv x‖ = ‖x‖) (toLinearEquiv_1 : E ≃ₛₗ[σ₁₂] E₂)
  (norm_map'_1 : ∀ (x : E), ‖toLinearEquiv_1 x‖ = ‖x‖),
  ({ toLinearEquiv := toLinearEquiv, norm_map' := norm_map' } =
      { toLinearEquiv := toLinearEquiv_1, norm_map' := norm_map'_1 }) =
    (toLinearEquiv = toLinearEquiv_1)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
SymmetricAlgebra.equivMvPolynomial_ι_apply : ∀ {κ : Type uκ} {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis κ R M) (i : κ),
  (SymmetricAlgebra.equivMvPolynomial b) ((SymmetricAlgebra.ι R M) (b i)) = MvPolynomial.X i
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.isClosedEmbedding_toContinuousMap : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [ContinuousAdd B] [T2Space B],
  Topology.IsClosedEmbedding ContinuousAddMonoidHom.toContinuousMap
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Subsumed by `Scheme.exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType`.  -/
_private.Mathlib.AlgebraicGeometry.AffineTransitionLimit.0.AlgebraicGeometry.Scheme.exists_hom_hom_comp_eq_comp_of_isAffine_of_locallyOfFiniteType : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (t : D ⟶ (CategoryTheory.Functor.const I).obj S) (f : X ⟶ S)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)]
  [AlgebraicGeometry.LocallyOfFiniteType f] [CategoryTheory.IsCofiltered I] [AlgebraicGeometry.IsAffine S]
  [AlgebraicGeometry.IsAffine X] [∀ (i : I), AlgebraicGeometry.IsAffine (D.obj i)] [AlgebraicGeometry.IsAffine c.pt]
  {i : I} (a : D.obj i ⟶ X),
  t.app i = CategoryTheory.CategoryStruct.comp a f →
    ∀ {j : I} (b : D.obj j ⟶ X),
      t.app j = CategoryTheory.CategoryStruct.comp b f →
        CategoryTheory.CategoryStruct.comp (c.π.app i) a = CategoryTheory.CategoryStruct.comp (c.π.app j) b →
          ∃ k hik hjk,
            CategoryTheory.CategoryStruct.comp (D.map hik) a = CategoryTheory.CategoryStruct.comp (D.map hjk) b
-- Mathlib.Algebra.Group.Prod
AddHom.prodMap.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : Add M] [inst_1 : Add N] [inst_2 : Add M']
  [inst_3 : Add N'] (f : M →ₙ+ M') (g : N →ₙ+ N'),
  f.prodMap g = (f.comp (AddHom.fst M N)).prod (g.comp (AddHom.snd M N))
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_sdiff : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  s₁ ⊆ s₂ → (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom_singleAddHom : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)],
  DFinsupp.sumAddHom (DFinsupp.singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Submodule.toAffineSubspace_direction : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] (s : Submodule k V),
  (↑s).direction = s
-- Mathlib.Data.Fin.Tuple.Basic
Fin.mem_find?_iff : ∀ {n : ℕ} {p : Fin n → Bool} {i : Fin n}, i ∈ Fin.find? p ↔ p i = true ∧ ∀ j < i, ¬p j = true
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {old aig : Std.Sat.AIG α} {out cout : aig.Ref}
  {hle : old.decls.size ≤ aig.decls.size} {aig_1 : Std.Sat.AIG α} {out_1 cout_1 : aig_1.Ref}
  {hle_1 : old.decls.size ≤ aig_1.decls.size},
  { aig := aig, out := out, cout := cout, hle := hle } = { aig := aig_1, out := out_1, cout := cout_1, hle := hle_1 } →
    aig = aig_1 ∧ out ≍ out_1 ∧ cout ≍ cout_1
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsSymm.smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α R] [inst_5 : SMulCommClass R α R] (a : α)
  {B : LinearMap.BilinForm R M}, B.IsSymm → (a • B).IsSymm
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.adjoinOne.eq_1 : MonCat.adjoinOne =
  { obj := fun S => MonCat.of (WithOne ↑S), map := fun {X Y} f => MonCat.ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f)),
    map_id := MonCat.adjoinOne._proof_1, map_comp := @MonCat.adjoinOne._proof_2 }
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ μ_1 : MeasureTheory.Measure α} (e_μ : μ = μ_1)
  [inst : PseudoEMetricSpace E] {f f_1 : ℕ → α → E} (e_f : f = f_1) {g g_1 : α → E} (e_g : g = g_1)
  (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (n n_1 : ℕ),
  n = n_1 →
    MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg n =
      MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux ⋯ n_1
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.ofMon_η : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Mon (CategoryTheory.Functor C C)),
  (CategoryTheory.Monad.ofMon M).η = CategoryTheory.MonObj.one
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The kernel of a morphism,
defined as the largest (quasi-coherent) ideal sheaf contained in the component-wise kernel.
This is usually only well-behaved when `f` is quasi-compact.  -/
AlgebraicGeometry.Scheme.Hom.ker : {X Y : AlgebraicGeometry.Scheme} → X.Hom Y → Y.IdealSheafData
-- Mathlib.Data.Nat.Cast.Defs
AddCommMonoidWithOne.toAddMonoidWithOne : {R : Type u_2} → [self : AddCommMonoidWithOne R] → AddMonoidWithOne R