mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instContinuousMapClass : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R], ContinuousMapClass (ContinuousMapZero X R) X R
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation_rightAngleRotation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x : E), o.rightAngleRotation (o.rightAngleRotation x) = -x
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_add_left' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∀ (g : α → ENNReal), ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.inv_ne_zero : ∀ {p q r : ℝ}, p.HolderTriple q r → p⁻¹ ≠ 0
-- Std.Data.TreeMap.Raw.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.TreeMap.Raw.insertMany : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {ρ : Type u_1} → [ForIn Id ρ (α × β)] → Std.TreeMap.Raw α β cmp → ρ → Std.TreeMap.Raw α β cmp
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instInhabited : (α : Type u_2) → [inst : InfSet α] → Inhabited (sInfHom α α)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.mul_X_pow_cancel : ∀ {R : Type u_1} [inst : Semiring R] {k : ℕ} {φ ψ : PowerSeries R},
  φ * PowerSeries.X ^ k = ψ * PowerSeries.X ^ k → φ = ψ
-- Lean.Language.Lean.Types
Lean.Language.Lean.instToSnapshotTreeCommandParsedSnapshot : Lean.Language.ToSnapshotTree Lean.Language.Lean.CommandParsedSnapshot
-- Mathlib.Order.Category.Semilat
SemilatInfCat.coe_forget_to_partOrd : ∀ (X : SemilatInfCat), ↑((CategoryTheory.forget₂ SemilatInfCat PartOrd).obj X) = X.X
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropy_iUnion_le : ∀ {X : Type u_1} {ι : Type u_2} [inst : UniformSpace X] (T : X → X) (F : ι → Set X),
  ⨆ i, Dynamics.coverEntropy T (F i) ≤ Dynamics.coverEntropy T (⋃ i, F i)
-- Lean.PrettyPrinter.Formatter
_private.Lean.PrettyPrinter.Formatter.0.Lean.PrettyPrinter.Formatter.SourceInfo.getExprPos? : Lean.SourceInfo → Option String.Pos.Raw
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_1.eq_2 : ∀ (motive : Std.Tactic.BVDecide.BVBinPred → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinPred.eq)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinPred.ult),
  (match Std.Tactic.BVDecide.BVBinPred.ult with
    | Std.Tactic.BVDecide.BVBinPred.eq => h_1 ()
    | Std.Tactic.BVDecide.BVBinPred.ult => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- If the implicit equation `f` is $C^n$ at `(u₁, u₂)`, then its implicit function `ψ` around `u₁`
is also $C^n$ at `u₁`.  -/
ContDiffAt.contDiffAt_implicitFunction : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  ContDiffAt 𝕜 n (cdf.implicitFunction pn if₂) u.1
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.finalize : Lean.Elab.Term.CollectPatternVars.Context → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.instHasOxfordStringsMessageData : Lean.HasOxfordStrings✝ Lean.MessageData
-- Init.Data.UInt.Lemmas
UInt16.ne_iff_toBitVec_ne : ∀ {a b : UInt16}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.Data.Set.Card
Set.odd_ncard_compl_iff : ∀ {α : Type u_1} [Finite α], Even (Nat.card α) → ∀ (s : Set α), Odd sᶜ.ncard ↔ Odd s.ncard
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of an `AddMonoid` by an additive congruence relation is
an `AddMonoid`.  -/
AddCon.addZeroClass : {M : Type u_1} → [inst : AddZeroClass M] → (c : AddCon M) → AddZeroClass c.Quotient
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getKey : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.DHashMap.Internal.Raw₀ α β) → (a : α) → m.contains a = true → α
-- Mathlib.Topology.Order.Monotone
IsClosed.csInf_mem : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, IsClosed s → s.Nonempty → BddBelow s → sInf s ∈ s
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.ι_D₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (j j' : J) (i₁ : I₁) (i₂ : I₂)
  (h : c₁.π c₂ c (i₁, i₂) = j),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
      (HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j') =
    HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j'
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- In a space with an inner regular measure for finite measure sets, any measurable set of finite
measure coincides almost everywhere with its everywhere positive subset.  -/
MeasureTheory.Measure.everywherePosSubset_ae_eq_of_measure_ne_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [OpensMeasurableSpace α] [μ.InnerRegularCompactLTTop], MeasurableSet s → μ s ≠ ⊤ → μ.everywherePosSubset s =ᵐ[μ] s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂)[k]! = m₁[k]!
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.objAppend1.eq_1 : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (a : P.A) (f' : (P.drop.B a).Arrow α)
  (f : P.last.B a → β), P.objAppend1 a f' f = ⟨a, TypeVec.splitFun f' f⟩
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_pi_div_three : Real.tan (Real.pi / 3) = √3
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
intervalIntegral.integrable_deriv_smul_comp_iff_of_deriv_nonneg : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ f' x) →
        (IntervalIntegrable (fun x => f' x • (g ∘ f) x) MeasureTheory.volume a b ↔
          IntervalIntegrable g MeasureTheory.volume (f a) (f b))
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.forIn'_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.done c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_2 c
-- Init.Data.SInt.IntToBitVec
Bool.toBitVec64_toISize : ∀ {b : Bool} (h : System.Platform.numBits = 64), b.toISize.toBitVec64 h = BitVec.setWidth 64 (BitVec.ofBool b)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)],
  Std.DTreeMap.Internal.Impl.leaf.maxEntry! =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.maxEntry!" 390 13
      "Map is empty"
-- Mathlib.Data.List.Sym
/-- `xs.sym2` is a list of all unordered pairs of elements from `xs`.
If `xs` has no duplicates then neither does `xs.sym2`.  -/
List.sym2 : {α : Type u_1} → List α → List (Sym2 α)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.continuousSemilinearEquivClass : ∀ {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 σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂], ContinuousSemilinearEquivClass (M₁ ≃SL[σ₁₂] M₂) σ₁₂ M₁ M₂
-- Mathlib.Order.Heyting.Regular
Heyting.IsRegular.himp : ∀ {α : Type u_1} [inst : HeytingAlgebra α] {a b : α},
  Heyting.IsRegular a → Heyting.IsRegular b → Heyting.IsRegular (a ⇨ b)
-- Mathlib.Topology.Category.Compactum
Compactum.isClosed_cl : ∀ {X : Compactum} (A : Set X.A), IsClosed (Compactum.cl✝ A)
-- Mathlib.Data.Matrix.Mul
RingHom.map_vecMul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [inst : Fintype n] [inst_1 : NonAssocSemiring R]
  [inst_2 : NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R) (v : n → R) (i : m),
  f (Matrix.vecMul v M i) = Matrix.vecMul (⇑f ∘ v) (M.map ⇑f) i
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoindAux_snd_mul_inv : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep.{w, u, v} k ↥S} (g₁ g₂ g₃ : G) (a : ↑A),
  (A.indToCoindAux g₁) a (g₂ * g₃⁻¹) = (A.indToCoindAux (g₁ * g₃)) a g₂
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.foldlM.loop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match 0 with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_1 ()
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.Const.getThenInsertIfNew? : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} {a : α} {b : β},
  m.WF → (Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b).2.WF
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Balanced.balancedCore_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E},
  Balanced 𝕜 s → balancedCore 𝕜 s = s
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Turn an element of a type `F` satisfying `MonoidHomClass F A B` and `ContinuousMapClass F A B`
into a `ContinuousMonoidHom`. This is declared as the default coercion from `F` to
`(A →ₜ* B)`.  -/
ContinuousMonoidHom.toContinuousMonoidHom : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            {F : Type u_7} →
              [inst_4 : FunLike F A B] → [MonoidHomClass F A B] → [ContinuousMapClass F A B] → F → A →ₜ* B
-- Lean.Data.Options
Lean.Option.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (name : Lean.Name) (defValue : α),
  sizeOf { name := name, defValue := defValue } = 1 + sizeOf name + sizeOf defValue
-- Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
_private.Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral.0.term𝓟_1 : Lean.ParserDescr
-- Mathlib.Data.EReal.Basic
EReal.lt_iff_exists_real_btwn : ∀ {a b : EReal}, a < b ↔ ∃ x, a < ↑x ∧ ↑x < b
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.leftOp_counitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ Dᵒᵖ) (X : D), e.leftOp.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.op X)).unop
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedMonoid.mk : {E : Type u_8} →
  [inst : TopologicalSpace E] →
    [toContinuousENorm : ContinuousENorm E] →
      [toMonoid : Monoid E] → ‖1‖ₑ = 0 → (∀ (x y : E), ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ) → ESeminormedMonoid E
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSimple.eq_top_of_isAtom : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSimple R L] (I : LieIdeal R L), IsAtom I → I = ⊤
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_iInf : ∀ {α : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] (f : ι → α),
  LowerSet.Iic (⨅ i, f i) = ⨅ i, LowerSet.Iic (f i)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_basisFun : ∀ {R : Type u_1} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂]
  [inst_2 : Module R N₂] [inst_3 : Fintype n] [inst_4 : Fintype m] [inst_5 : DecidableEq m] [inst_6 : DecidableEq n],
  LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = LinearMap.toMatrix₂' R
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap'.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A B : Subalgebra R S), A.mulMap' B = (↑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯)).comp (A.mulMap B).rangeRestrict
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The homology functor to graded objects.  -/
HomologicalComplex.gradedHomologyFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          [CategoryTheory.CategoryWithHomology C] →
            CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.GradedObject ι C)
-- Mathlib.Analysis.InnerProductSpace.Subspace
orthonormal_span : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → Orthonormal 𝕜 fun i => ⟨v i, ⋯⟩
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_shiftLeft : ∀ {i j : ℕ} (x : ℕ), (x <<< i).testBit j = (decide (j ≥ i) && x.testBit (j - i))
-- Init.Data.Nat.Gcd
Nat.gcd_add_left_right_of_dvd : ∀ {n k : ℕ} (m : ℕ), n ∣ k → n.gcd (k + m) = n.gcd m
-- Mathlib.Data.Sym.NatCard
/-- A version of `card_sym_eq_multichoose` that does not need finiteness.  -/
Sym.natCard_sym_eq_multichoose : ∀ (α : Type u_1) (k : ℕ), Nat.card (Sym α k) = (Nat.card α).multichoose k
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.map_comp : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Type u_6} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  (f : M →ₗ[R] N) (g : N →ₗ[R] P),
  DividedPowerAlgebra.map R (g ∘ₗ f) = (DividedPowerAlgebra.map R g).comp (DividedPowerAlgebra.map R f)
-- Mathlib.Algebra.Order.Floor.Defs
Int.floor_nonpos : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, a ≤ 0 → ⌊a⌋ ≤ 0
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.find?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String} {pos : s.Pos},
  s.find? p = some pos ↔
    ∃ (h : pos ≠ s.endPos), p (pos.get h) = true ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), p (pos'.get ⋯) = false
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Spec.germ_stalkMapIso_hom : ∀ {R : CommRingCat} (x : PrimeSpectrum ↑R),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial)
      (AlgebraicGeometry.Spec.stalkIso R x).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom
      (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)))
-- Init.Data.UInt.Bitwise
UInt32.and_self : ∀ {a : UInt32}, a &&& a = a
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_image_nhds_mem_nhds_of_mem_interior_range : ∀ {𝕜 : 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]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M},
  x ∈ f.source →
    ↑(f.extend I) x ∈ interior (Set.range ↑I) → ∀ {s : Set M}, s ∈ nhds x → ↑(f.extend I) '' s ∈ nhds (↑(f.extend I) x)
-- Mathlib.FieldTheory.SeparableDegree
/-- The minimal polynomial of an element `x` of `E / F` of exponential characteristic `q` has
separable degree one if and only if the minimal polynomial is of the form
`(X - x) ^ (q ^ n)` for some `n : ℕ`.  -/
minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E] (q : ℕ)
  [hF : ExpChar F q] {x : E},
  (minpoly F x).natSepDegree = 1 ↔
    ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.isCommutative : Lean.Meta.Grind.AC.ACM Bool
-- Mathlib.Order.Hom.WithTopBot
InfHom.withTop'_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β]
  (f : InfHom α β) (a : WithTop α), f.withTop' a = Option.elim a ⊤ ⇑f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instInhabitedPoly : Inhabited Lean.Grind.CommRing.Poly
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_prod_eq_sup_of_pairwise_ne : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M},
  ((↑s).Pairwise fun i j => ‖f i‖₊ ≠ ‖f j‖₊) → ‖∏ i ∈ s, f i‖₊ = s.sup fun i => ‖f i‖₊
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instCategory : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] → CategoryTheory.Category.{v, v + 1} (ContinuousGeneratedByCat X)
-- Mathlib.Data.Set.Constructions
/-- `univ_mem` states that `Set.univ` is in `S`.  -/
FiniteInter.univ_mem : ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ S
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι}
  (f : i ⟶ j) {Z : C}
  (h : X.E (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₁ n₂ hn₂).hom
      (CategoryTheory.CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv h) =
    CategoryTheory.CategoryStruct.comp
      (X.πE (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂) h
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II_δ : ∀ {n : ℕ} (i : Fin (n + 2)), SimplexCategory.II.δ i = (SimplexCategory.σ i).op
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.leftToRight_app_map_adj₁_unit_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  (X : C) {Z : D} (h : H.obj (G.obj (F.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.leftToRight.app X)
      (CategoryTheory.CategoryStruct.comp (H.map (t.adj₁.unit.app X)) h) =
    CategoryTheory.CategoryStruct.comp (t.adj₂.unit.app (F.obj X)) h
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E}
  {x : E}, AnalyticWithinAt 𝕜 f s x → Set.EqOn g f s → g x = f x → AnalyticWithinAt 𝕜 g s x
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.orthogonalDecomposition_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (a : WithLp 2 (↥K × ↥Kᗮ)),
  K.orthogonalDecomposition.symm a = ↑a.fst + ↑a.snd
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Rat.instMeasurableSpace : MeasurableSpace ℚ
-- Mathlib.Order.SuccPred.Limit
IsLUB.isSuccLimit_of_notMem : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α] {s : Set α}, IsLUB s a → s.Nonempty → a ∉ s → Order.IsSuccLimit a
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D] {X Y : W.FunctorsInverting D} (τ : X ⟶ Y) (X_1 : W.Localization),
  ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).map τ).app X_1 =
    CategoryTheory.Localization.Construction.NatTransExtension.app
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp τ.hom (CategoryTheory.eqToHom ⋯)))
      X_1
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.Entry.toDeclName : Lean.Compiler.CSimp.Entry → Lean.Name
-- Batteries.Linter.UnnecessarySeqFocus
Batteries.Linter.UnnecessarySeqFocus.Entry.mk.injEq : ∀ (stx : Lean.Syntax) (used : Bool) (stx_1 : Lean.Syntax) (used_1 : Bool),
  ({ stx := stx, used := used } = { stx := stx_1, used := used_1 }) = (stx = stx_1 ∧ used = used_1)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.linearIndepOn_basisSet : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  LinearIndepOn ℚ (⇑toRatVec✝) (IsProperLinearSet.basisSet✝ hs)
-- Mathlib.RingTheory.Discriminant
/-- If `L/K` is a field extension and `b : ι → L`, then `discr K b` is the square of the
determinant of the matrix whose `(i, j)` coefficient is `σⱼ (b i)`, where `σⱼ : L →ₐ[K] E` is the
embedding in an algebraically closed field `E` corresponding to `j : ι` via a bijection
`e : ι ≃ (L →ₐ[K] E)`.  -/
Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two : ∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} (E : Type z) [inst_2 : Field K]
  [inst_3 : Field L] [inst_4 : Field E] [inst_5 : Algebra K L] [inst_6 : Algebra K E] [Module.Finite K L]
  [IsAlgClosed E] (b : ι → L) [Algebra.IsSeparable K L] (e : ι ≃ (L →ₐ[K] E)),
  (algebraMap K E) (Algebra.discr K b) = (Algebra.embeddingsMatrixReindex K E b e).det ^ 2
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_linearEquivTuple_symm : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R],
  ⇑(QuaternionAlgebra.linearEquivTuple c₁ c₂ c₃).symm = ⇑(QuaternionAlgebra.equivTuple c₁ c₂ c₃).symm
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_toSubgroup' : ∀ {G : Type u_1} [inst : Group G] (S : AddSubgroup (Additive G)) (g : G),
  g ∈ AddSubgroup.toSubgroup' S ↔ Additive.ofMul g ∈ S