mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Extr
IsMaxOn.comp_mapsTo : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set δ} {g : δ → α}
  {b : δ}, IsMaxOn f s a → Set.MapsTo g t s → g b = a → IsMaxOn (f ∘ g) t b
-- Mathlib.Algebra.Group.Even
/-- **Alias** of the reverse direction of `isSquare_inv`. -/
IsSquare.inv : ∀ {α : Type u_2} [inst : DivisionMonoid α] {a : α}, IsSquare a → IsSquare a⁻¹
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.filterMap! f t) k =
    (Std.DTreeMap.Internal.Impl.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_equivariantMap_injective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α},
  Function.Injective ⇑(SubAddAction.ofFixingAddSubgroup_equivariantMap M s)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_inv : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  hU.isoSpec.inv =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))
      (↑U).isoSpec.inv
-- Aesop.Tree.Data
Aesop.NodeState.isUnknown : Aesop.NodeState → Bool
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Convenience reformulation of the second iterated derivative, as a map from `E` to linear maps
`E ⊗[𝕜] E →ₗ[𝕜] F`.
 -/
tensorIteratedFDerivWithinTwo : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → (E → F) → Set E → E → TensorProduct 𝕜 E E →ₗ[𝕜] F
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) =
    CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
/-- If `f` is absolutely continuous on `[d, b]` and there is a collection of pairwise disjoint
closed subintervals of `(d, b)` of total length `b - d` such that the sum of `dist (f x) (f y)` for
`[x, y]` in the collection is equal to `y`, then `dist (f b) (f d) ≤ y`.  -/
AbsolutelyContinuousOnInterval.dist_le_of_pairwiseDisjoint_hasSum : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {f : ℝ → X} {d b y : ℝ},
  d ≤ b →
    AbsolutelyContinuousOnInterval f d b →
      ∀ {u : Set (ℝ × ℝ)},
        (∀ z ∈ u, d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) →
          (u.PairwiseDisjoint fun z => Set.Icc z.1 z.2) →
            HasSum (fun z => (↑z).2 - (↑z).1) (b - d) →
              HasSum (fun z => dist (f (↑z).1) (f (↑z).2)) y → dist (f d) (f b) ≤ y
-- Mathlib.Geometry.Manifold.StructureGroupoid
Pregroupoid.mk : {H : Type u_2} →
  [inst : TopologicalSpace H] →
    (property : (H → H) → Set H → Prop) →
      (∀ {f g : H → H} {u v : Set H},
          property f u → property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property (g ∘ f) (u ∩ f ⁻¹' v)) →
        property id Set.univ →
          (∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u) →
            (∀ {f g : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, g x = f x) → property f u → property g u) → Pregroupoid H
-- Init.Data.Order.Opposite
LT.lt_opposite_iff : ∀ {α : Type u_1} {lt : LT α} {a b : α}, a < b ↔ b < a
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `Finset.analyticOn_sum`

---

Finite sums of analytic functions are analytic  -/
Finset.analyticOn_fun_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {f : α → E → F} {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOn 𝕜 (f n) s) → AnalyticOn 𝕜 (fun a => ∑ c ∈ N, f c a) s
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.mapFrameHom_apply : ∀ {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] (I : Ideal R),
  (IsLocalization.mapFrameHom M S) I = Ideal.map (algebraMap R S) I
-- Mathlib.Topology.Constructions.SumProd
nhds_prod_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {y : Y},
  nhds (x, y) = nhds x ×ˢ nhds y
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.neg_mk : ∀ {R : Type u_1} {a b : R} [inst : Neg R] (x y : R), -{ re := x, im := y } = { re := -x, im := -y }
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_sdiff_eq_sdiff_union : ∀ {α : Type u_1} {s t u : Set α}, u ⊆ s → s \ (t \ u) = s \ t ∪ u
-- Std.Async.System
Std.Async.System.instInhabitedSystemUser : Inhabited Std.Async.System.SystemUser
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_isPrime_of_surjective : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] {f : F},
  Function.Surjective ⇑f → ∀ {I : Ideal R} [H : I.IsPrime], RingHom.ker f ≤ I → (Ideal.map f I).IsPrime
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.seminormedAddCommGroup : {E : Type u_2} → [SeminormedAddCommGroup E] → SeminormedAddCommGroup Eᵒᵈ
-- Mathlib.Order.Fin.Tuple
Fin.insertNthOrderIso_toEquiv : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)),
  (Fin.insertNthOrderIso α p).toEquiv = Fin.insertNthEquiv α p
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValRat.lt_add_of_lt : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r₁ r₂ : ℚ},
  r₁ + r₂ ≠ 0 →
    padicValRat p q < padicValRat p r₁ → padicValRat p q < padicValRat p r₂ → padicValRat p q < padicValRat p (r₁ + r₂)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.stabilizer_mul_eq_right : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Group α] [SMulCommClass G α α]
  (a b : α), MulAction.stabilizer G (a * b) = MulAction.stabilizer G b
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_fun_sum : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [inst : Fintype ι],
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    ProbabilityTheory.variance (fun ω => ∑ i, X i ω) μ = ∑ i, ∑ j, ProbabilityTheory.covariance (X i) (X j) μ
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.mk : {A : Type u} →
  [inst : Ring A] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module A M] →
          (toRelations : Module.Relations A) →
            (toSolution : toRelations.Solution M) → toSolution.IsPresentation → Module.Presentation A M
-- Init.Data.String.Basic
String.Pos.Raw.utf8SetAux.eq_2 : ∀ (c' : Char) (x x_1 : String.Pos.Raw) (c : Char) (cs : List Char),
  String.Pos.Raw.utf8SetAux c' (c :: cs) x x_1 =
    if x = x_1 then c' :: cs else c :: String.Pos.Raw.utf8SetAux c' cs (x + c) x_1
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Subtracts `i`-th row multiplied by `coef` from `j`-th row.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.subtractRow : {α : ℕ → ℕ → Type} →
  [self : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α] → {n m : ℕ} → α n m → ℕ → ℕ → ℚ → α n m
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k' : α) →
                (v : β k') →
                  (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)) →
            motive t
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  DiscreteTopology ↥(NumberField.mixedEmbedding.idealLattice K I)
-- Mathlib.Condensed.Module
/-- The left adjoint to the forgetful functor. The *free condensed `R`-module* on a condensed set.
 -/
Condensed.free : (R : Type (u + 1)) → [inst : Ring R] → CategoryTheory.Functor CondensedSet (CondensedMod R)
-- Mathlib.Data.Vector.Basic
List.Vector.toList_ofFn : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α), (List.Vector.ofFn f).toList = List.ofFn f
-- Mathlib.Analysis.Convex.Hull
/-- **Alias** of the reverse direction of `convexHull_nonempty_iff`. -/
Set.Nonempty.convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, s.Nonempty → ((convexHull 𝕜) s).Nonempty
-- Batteries.Data.Array.Match
/-- KMP matcher structure  -/
Array.Matcher : Type u_1 → Type u_1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_iExs : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {γ : Type u_3} [inst_1 : Finite γ]
  {φ : L.Formula (α ⊕ γ)} {v : α → M}, (FirstOrder.Language.Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.SymbolPriorityEntry.mk : Lean.Name → ℕ → Lean.Meta.Grind.SymbolPriorityEntry
-- Mathlib.Algebra.Star.TensorProduct
TensorProduct.star_tmul : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : AddCommMonoid B]
  [inst_7 : StarAddMonoid B] [inst_8 : Module R B] [inst_9 : StarModule R B] (x : A) (y : B),
  star (x ⊗ₜ[R] y) = star x ⊗ₜ[R] star y
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_inf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
  {v : α → M} {xs : Fin l → M}, (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs
-- Mathlib.Topology.Instances.Matrix
HasSum.matrix_blockDiagonal' : ∀ {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq l]
  {f : X → (i : l) → Matrix (m' i) (n' i) R} {a : (i : l) → Matrix (m' i) (n' i) R},
  HasSum f a L → HasSum (fun x => Matrix.blockDiagonal' (f x)) (Matrix.blockDiagonal' a) L
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toArray_eq_match_rcc : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α],
  r.toArray =
    match Std.PRange.succ? r.lower with
    | none => #[]
    | some next => (next...=r.upper).toArray
-- Mathlib.Analysis.Normed.Operator.Banach
LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] (e : E ≃ₛₗ[σ] F) (h : Continuous ⇑e),
  ⇑(e.toContinuousLinearEquivOfContinuous h).symm = ⇑e.symm
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsTriangulatedPlus : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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), t.plus.IsTriangulated
-- Mathlib.Logic.Equiv.Defs
Quotient.congr_mk : ∀ {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α ≃ β)
  (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α), (Quotient.congr e eq) ⟦a⟧ = ⟦e a⟧
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → ∀ {km : α}, t.max? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Analysis.Convex.Function
/-- A strictly convex function on an open segment is strictly upper-bounded by the max of its
endpoints.  -/
StrictConvexOn.lt_on_openSegment : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  StrictConvexOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → x ≠ y → z ∈ openSegment 𝕜 x y → f z < max (f x) (f y)
-- Std.Data.TreeMap.Basic
/-- Folds the given monadic function over the mappings in the map in ascending order.  -/
Std.TreeMap.foldlM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (δ → α → β → m δ) → δ → Std.TreeMap α β cmp → m δ
-- Mathlib.SetTheory.ZFC.Class
Class.coe_sInter : ∀ {x : ZFSet.{u}}, x.Nonempty → ↑x.sInter = (↑x).sInter
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.not_isNonloop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → ¬M.IsNonloop e
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instCompleteSemilatticeInf.eq_1 : ∀ {α : Type u} [inst : Group α],
  GroupTopology.instCompleteSemilatticeInf =
    { toPartialOrder := inferInstance, toInfSet := inferInstance, isGLB_sInf := ⋯ }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.basicOpen_eq_union_of_projection : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A),
  ProjectiveSpectrum.basicOpen 𝒜 f = ⨆ i, ProjectiveSpectrum.basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f)
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- An `Injective` linear map `f : M →ₗ[R] M₂` defines a linear equivalence
between `M` and `f.range`. See also `LinearMap.ofLeftInverse`.  -/
LinearEquiv.ofInjective : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {module_M : Module R M} →
                  {module_M₂ : Module R₂ M₂} →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        (f : M →ₛₗ[σ₁₂] M₂) →
                          [inst_4 : RingHomInvPair σ₁₂ σ₂₁] →
                            [inst_5 : RingHomInvPair σ₂₁ σ₁₂] → Function.Injective ⇑f → M ≃ₛₗ[σ₁₂] ↥f.range
-- Mathlib.Analysis.Convex.Strong
UniformConcaveOn.strictConcaveOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ},
  UniformConcaveOn s φ f → (∀ (r : ℝ), r ≠ 0 → 0 < φ r) → StrictConcaveOn ℝ s f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Any functor between Cartesian-monoidal categories is oplax monoidal in a unique way.  -/
CategoryTheory.Functor.OplaxMonoidal.instSubsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D), Subsingleton F.OplaxMonoidal
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_pos : ∀ {n k : ℕ}, k ≤ n → 0 < n.choose k
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.preimage_id : ∀ {R : CommRingCat},
  AlgebraicGeometry.Spec.preimage (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)) =
    CategoryTheory.CategoryStruct.id R
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts.isStableUnderProductsOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.IsStableUnderFiniteProducts] (J : Type) [Finite J], W.IsStableUnderProductsOfShape J
-- Init.Data.List.Basic
List.beq.eq_1 : ∀ {α : Type u} [inst : BEq α], [].beq [] = true
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.restrictScalars_toMatrix : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} [inst_1 : Fintype m] [inst_2 : DecidableEq m] {A : Type u_4}
  {M : Type u_5} {n : Type u_6} [inst_3 : Fintype n] [inst_4 : DecidableEq n] [inst_5 : CommSemiring A]
  [inst_6 : AddCommMonoid M] [inst_7 : Module R M] [inst_8 : Module A M] [inst_9 : Algebra R A]
  [inst_10 : IsScalarTower R A M] (bA : Module.Basis m R A) (bM : Module.Basis n A M) (f : M →ₗ[A] M),
  (LinearMap.toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) =
    (Matrix.comp n n m m R) (((LinearMap.toMatrix bM bM) f).map ⇑(Algebra.leftMulMatrix bA))
-- Init.Data.Nat.Bitwise.Lemmas
Nat.eq_iff_testBit_eq : ∀ {n m : ℕ}, n = m ↔ ∀ (i : ℕ), n.testBit i = m.testBit i
-- Std.Data.DTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.DTreeMap.entryAtIdx? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → ℕ → Option ((a : α) × β a)
-- Mathlib.Order.Closure
/-- **Alias** of `ClosureOperator.setOfPred_isClosed_eq_range_closure`.

---

The set of closed elements for `c` is exactly its range.  -/
ClosureOperator.setOf_isClosed_eq_range_closure : ∀ {α : Type u_1} [inst : Preorder α] {c : ClosureOperator α}, {x | c.IsClosed x} = Set.range ⇑c
-- Mathlib.Algebra.Star.Basic
isRightRegular_star_iff : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x : R}, IsRightRegular (star x) ↔ IsLeftRegular x
-- Mathlib.Topology.EMetricSpace.Paracompact
Metric.t4Space : ∀ {α : Type u_1} [inst : EMetricSpace α], T4Space α
-- Mathlib.Dynamics.FixedPoints.Support
/-- If `f` and `g` have compact fixed support, then so does their composition `f ∘ g`.  -/
Function.HasCompactFixedSupport.comp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f g : X → X},
  Function.HasCompactFixedSupport f → Function.HasCompactFixedSupport g → Function.HasCompactFixedSupport (f ∘ g)
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supportedEquivMvPolynomial_symm_C : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] (s : Set σ) (x : R),
  (MvPolynomial.supportedEquivMvPolynomial s).symm (MvPolynomial.C x) = (algebraMap R ↥(MvPolynomial.supported R s)) x
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- `adjMatrix G α` is the matrix `A` such that `A i j = (1 : α)` if `i` and `j` are
adjacent in the simple graph `G`, and otherwise `A i j = 0`.  -/
SimpleGraph.adjMatrix : (α : Type u_1) → {V : Type u_2} → (G : SimpleGraph V) → [DecidableRel G.Adj] → [Zero α] → [One α] → Matrix V V α
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.ext_iff : ∀ {M N : SemiNormedGrp} {f₁ f₂ : M ⟶ N},
  f₁ = f₂ ↔ ∀ (x : M.carrier), (CategoryTheory.ConcreteCategory.hom f₁) x = (CategoryTheory.ConcreteCategory.hom f₂) x
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of the reverse direction of `hnot_le_iff_codisjoint_left`. -/
Codisjoint.hnot_le_left : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, Codisjoint a b → ￢b ≤ a
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul'.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A], LinearMap.mul' R A = LinearMap.mul' R A
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.hom_ext_iff : ∀ {n : Type u} {S X : AlgebraicGeometry.Scheme} {f g : X ⟶ AlgebraicGeometry.AffineSpace n S},
  f = g ↔
    CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.AffineSpace n S ↘ S) =
        CategoryTheory.CategoryStruct.comp g (AlgebraicGeometry.AffineSpace n S ↘ S) ∧
      ∀ (i : n),
        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
            (AlgebraicGeometry.AffineSpace.coord S i) =
          (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop g))
            (AlgebraicGeometry.AffineSpace.coord S i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {h' : k ∈ Std.TreeMap.Raw.filter f t} (h : t.WF), (Std.TreeMap.Raw.filter f t)[k] = t[k]
-- Mathlib.Data.Finmap
Finmap.lookup_union_left_of_not_in : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finmap β},
  a ∉ s₂ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₁
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecTheorem.mk.injEq : ∀ (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (name_1 : Lean.Name)
  (levelParams_1 : List Lean.Name) (type_1 : Lean.Expr),
  ({ name := name, levelParams := levelParams, type := type } =
      { name := name_1, levelParams := levelParams_1, type := type_1 }) =
    (name = name_1 ∧ levelParams = levelParams_1 ∧ type = type_1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.bin.injEq : ∀ {w : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr w) (op : Std.Tactic.BVDecide.BVBinPred) (rhs : Std.Tactic.BVDecide.BVExpr w)
  (w_1 : ℕ) (lhs_1 : Std.Tactic.BVDecide.BVExpr w_1) (op_1 : Std.Tactic.BVDecide.BVBinPred)
  (rhs_1 : Std.Tactic.BVDecide.BVExpr w_1),
  (Std.Tactic.BVDecide.BVPred.bin lhs op rhs = Std.Tactic.BVDecide.BVPred.bin lhs_1 op_1 rhs_1) =
    (w = w_1 ∧ lhs ≍ lhs_1 ∧ op = op_1 ∧ rhs ≍ rhs_1)
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Additive inverse of a rational function.  -/
RatFunc.neg : {K : Type u_1} → [inst : CommRing K] → RatFunc K → RatFunc K
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.cancelVar.induct_unfolding : ∀ (x : Lean.Grind.CommRing.Var) (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Prop),
  motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit →
    (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
        (p.x == x) = true → motive (Lean.Grind.CommRing.Mon.mult p m) m) →
      (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
          (p.x == x) = false →
            motive m (m.cancelVar x) →
              motive (Lean.Grind.CommRing.Mon.mult p m) (Lean.Grind.CommRing.Mon.mult p (m.cancelVar x))) →
        ∀ (m : Lean.Grind.CommRing.Mon), motive m (m.cancelVar x)
-- Mathlib.Analysis.Complex.Circle
Circle.coeHom_apply : ∀ (self : ↥(Submonoid.unitSphere ℂ)), Circle.coeHom self = ↑self
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_one : ∀ {R : Type u_1} [inst : Semiring R] (x y : R), Polynomial.evalEval x y 1 = 1
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDedekindDomain A] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A),
  IsPrincipalIdealRing ↥(IsDedekindDomain.HeightOneSpectrum.valuation K v).integer