mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Relation
Relation.EqvGen.eqvGen_reflGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.EqvGen (Relation.ReflGen r) = Relation.EqvGen r
-- Mathlib.Algebra.AddConstMap.Equiv
/-- The identity map as an `AddConstEquiv`.  -/
AddConstEquiv.refl : {G : Type u_1} → [inst : Add G] → (a : G) → AddConstEquiv G G a a
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iic_ofDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : αᵒᵈ),
  Finset.Iic (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ici a)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.neg_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (m : M) (x : MonoidAlgebra R M), (-x).coeff m = -x.coeff m
-- Mathlib.Data.Fintype.Inv
/-- Given a fintype `α` and a predicate `p`, associate to a proof that there is a unique element of
`α` satisfying `p` this unique element, as an element of the corresponding subtype.  -/
Fintype.chooseX : {α : Type u_1} → [Fintype α] → (p : α → Prop) → [DecidablePred p] → (∃! a, p a) → { a // p a }
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.η_algSpec_left : ∀ {R : CommRingCat},
  CategoryTheory.Over.Hom.left (CategoryTheory.Functor.OplaxMonoidal.η (AlgebraicGeometry.algSpec R)) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The `Algebra.Presentation` associated to a standard etale presentation.  -/
StandardEtalePresentation.toPresentation : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → StandardEtalePresentation R S → Algebra.Presentation R S (Fin 2) (Fin 2)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_add_of_ne : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.degree f ≠ m.degree g → m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
-- Mathlib.Order.Hom.Bounded
BotHom.instSemilatticeSup : {α : Type u_2} →
  {β : Type u_3} → [inst : Bot α] → [inst_1 : SemilatticeSup β] → [inst_2 : OrderBot β] → SemilatticeSup (BotHom α β)
-- Mathlib.Algebra.Group.Invertible.Defs
/-- If `a` is invertible and `a = b`, then `⅟a = ⅟b`.  -/
Invertible.congr : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a] [inst_2 : Invertible b], a = b → ⅟a = ⅟b
-- Lean.Data.Json.Basic
Lean.Json.arr : Array Lean.Json → Lean.Json
-- Mathlib.GroupTheory.MonoidLocalization.Away
Localization.Away.mk_eq_monoidOf_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] (x : M),
  Localization.mk = Submonoid.LocalizationMap.mk' (Localization.Away.monoidOf x)
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.seminormedGroup : {E : Type u_2} → [SeminormedGroup E] → SeminormedGroup (ULift.{u_5, u_2} E)
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_mod_of_dvd : ∀ (a b : UInt16), b.toNat ∣ 256 → (a % b).toUInt8 = a.toUInt8 % b.toUInt8
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.single_zero_one_eq_one : ∀ {R : Type u_1} [inst : Semiring R], AddMonoidAlgebra.single 0 1 = 1
-- Mathlib.Algebra.Group.Submonoid.Support
/-- **Alias** of the reverse direction of `isPointed_iff_support_eq_bot`. -/
AddSubmonoid.IsPointed.of_support_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, M.support = ⊥ → M.IsPointed
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.pow_left : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} {m : ℕ}, IsCoprime x y → IsCoprime (x ^ m) y
-- Init.Data.UInt.Bitwise
USize.not_or_self : ∀ {a : USize}, ~~~a ||| a = -1
-- Mathlib.Algebra.Star.Basic
Invertible.star : {R : Type u_1} → [inst : MulOneClass R] → [inst_1 : StarMul R] → (r : R) → [Invertible r] → Invertible (star r)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.measurableSet_negAt_plusPart : ∀ {K : Type u_1} [inst : Field K] (s : Set { w // w.IsReal }) (A : Set (NumberField.mixedEmbedding.mixedSpace K))
  [NumberField K],
  MeasurableSet A → MeasurableSet (⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A)
-- Mathlib.NumberTheory.ModularForms.DedekindEta
/-- For any `k`, the function `q ↦ ∏' n, (1 - q^(n+1))^k` is differentiable on the
open unit disc.  -/
ModularForm.differentiableOn_tprod_one_sub_pow_pow : ∀ (k : ℕ), DifferentiableOn ℂ (fun q => ∏' (n : ℕ), (1 - q ^ (n + 1)) ^ k) (Metric.ball 0 1)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
strictMono_mul_right_of_pos : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [MulPosStrictMono M₀],
  0 < a → StrictMono fun x => x * a
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 3} (φ : R₁ ⟶ R₂),
  R₁.map' 0 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2
        CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4 =
      0 →
    (CategoryTheory.ComposableArrows.mk₂
          (R₁.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
            CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4)
          (R₁.map' 2 3 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4
            CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_7)).Exact →
      (CategoryTheory.ComposableArrows.mk₂
            (R₂.map' 0 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_9
              CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_11)
            (R₂.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
              CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4)).Exact →
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_13) →
          CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_11) →
            CategoryTheory.Mono
                (CategoryTheory.ComposableArrows.app' φ 3
                  CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_7) →
              CategoryTheory.Mono
                (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Adds `y` as an occurrence of `x`.
That is, `x` occurs in `lowers[y]`, `uppers[y]`, or `diseqs[y]`.
 -/
Lean.Meta.Grind.Arith.Linear.addOcc : Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Mathlib.Data.Nat.Totient
/-- Euler's totient function. This counts the number of naturals strictly less than `n` which are
coprime with `n`.  -/
Nat.termφ : Lean.ParserDescr
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_comp_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} (x : FreeAbelianGroup α),
  (FreeAbelianGroup.map (g ∘ f)) x = (FreeAbelianGroup.map g) ((FreeAbelianGroup.map f) x)
-- Mathlib.Topology.Algebra.Monoid
exists_mem_nhds_zero_mul_subset : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M] {K U : Set M},
  IsCompact K → U ∈ nhds 0 → ∃ V ∈ nhds 0, K * V ⊆ U
-- Mathlib.Topology.Separation.DisjointCover
/-- If `f` is a continuous map from a profinite space to a topological space with a
commutative additive monoid structure, then we can approximate `f` by finite sums of indicator
functions of clopen sets.

(Note no compatibility is assumed between the monoid structure on `V` and the topology.)  -/
ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal : ∀ {X : Type u_1} {V : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace V] [TotallyDisconnectedSpace X]
  [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) [inst_5 : AddCommMonoid V],
  S ∈ nhdsSet (Set.diagonal V) → ∃ n U v, ∀ (x : X), (f x, ∑ n, (↑(U n)).indicator (fun x => v n) x) ∈ S
-- Init.Prelude
/-- Parses using `p`, then pops the stack to create a new node with kind `kind`.
The precedence `prec` is used to determine whether the parser should apply given
the current precedence level.  -/
Lean.ParserDescr.node : Lean.SyntaxNodeKind → ℕ → Lean.ParserDescr → Lean.ParserDescr
-- Mathlib.Algebra.GCDMonoid.Basic
isUnit_gcd_one_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a : α), IsUnit (gcd 1 a)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt : Lean.Expr →
  Bool → Lean.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.SetTheory.Ordinal.Family
/-- An alias of `ciSup_le'` for discoverability.  -/
Ordinal.iSup_le : ∀ {ι : Sort u_3} {f : ι → Ordinal.{u_4}} {a : Ordinal.{u_4}}, (∀ (i : ι), f i ≤ a) → ⨆ i, f i ≤ a
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.coordChange_self : ∀ {ι : Type u_5} {B : Type u_6} [inst : TopologicalSpace B] {F : Type u_7} [inst_1 : TopologicalSpace F]
  (self : FiberBundleCore ι B F) (i : ι), ∀ x ∈ self.baseSet i, ∀ (v : F), self.coordChange i i x v = v
-- Mathlib.Order.Filter.Map
Filter.map_inf_le : ∀ {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β}, Filter.map m (f ⊓ g) ≤ Filter.map m f ⊓ Filter.map m g
-- Mathlib.Analysis.Distribution.Support
Distribution.IsVanishingOn.iteratedLineDerivOp : ∀ {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E}
  {F : Type u_12} [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F]
  [inst_5 : IsTopologicalAddGroup F] [inst_6 : ContinuousSMul ℝ F] {f : Distribution Ω F ⊤} {s : Set E} {n : ℕ},
  Distribution.IsVanishingOn (⇑f) s →
    ∀ (m : Fin n → E), Distribution.IsVanishingOn (⇑(LineDeriv.iteratedLineDerivOp m f)) s
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.lift_unique : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {P : Type u₁} [inst_5 : L.Structure P]
  (F : L.Embedding (FirstOrder.Language.DirectLimit G f) P) (x : FirstOrder.Language.DirectLimit G f),
  F x =
    (FirstOrder.Language.DirectLimit.lift L ι G f (fun i => F.comp (FirstOrder.Language.DirectLimit.of L ι G f i)) ⋯) x
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.good_lt_maxProducts : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
      (q :
        ↑(Profinite.NobelingProof.GoodProducts
            (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))
      (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)), List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.braiding_inv_apply : ∀ {X Y : TopCat} {x : ↑X} {y : ↑Y}, (CategoryTheory.ConcreteCategory.hom (β_ X Y).inv) (y, x) = (x, y)
-- Init.Data.Dyadic.Basic
Dyadic.mul.eq_2 : ∀ (x : Dyadic), (x = Dyadic.zero → False) → x.mul Dyadic.zero = Dyadic.zero
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.hasAssignedUVars.go : Array (Option Lean.Level) → Lean.Level → Bool
-- Init.Data.Int.Gcd
Int.gcd_le_natAbs_right : ∀ {b : ℤ} (a : ℤ), b ≠ 0 → a.gcd b ≤ b.natAbs
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.mk.sizeOf_spec : ∀ {α : Type u_6} [inst : SizeOf α] (sets : Set (Set α)) (nonempty : sets.Nonempty)
  (inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y),
  sizeOf { sets := sets, nonempty := nonempty, inter_sets := inter_sets } = 1 + sizeOf nonempty
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The copy from an induced subgraph to the initial simple graph.  -/
SimpleGraph.Copy.induce : {V : Type u_1} → (G : SimpleGraph V) → (s : Set V) → (SimpleGraph.induce s G).Copy G
-- Mathlib.Order.Interval.Set.InitialSeg
Set.principalSegIio_apply : ∀ {α : Type u_1} [inst : Preorder α] {j : α} (k : ↑(Set.Iio j)), (Set.principalSegIio j).toRelEmbedding k = ↑k
-- Mathlib.Algebra.Ring.Nat
Nat.instAddCommMonoidWithOne : AddCommMonoidWithOne ℕ
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorems.mk : Lean.SMap Lean.Name (List Lean.Meta.SimpCongrTheorem) → Lean.Meta.SimpCongrTheorems
-- Mathlib.Analysis.Convex.Topology
Real.ball_eq_openSegment : ∀ {r ε : ℝ}, 0 < ε → Metric.ball r ε = openSegment ℝ (r - ε) (r + ε)
-- Mathlib.Order.Lattice
/-- A subtype forms a distributive lattice if `⊔` and `⊓` preserve the property.
See note [reducible non-instances].  -/
Subtype.distribLattice : {α : Type u} →
  [inst : DistribLattice α] →
    {P : α → Prop} →
      (∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)) → (∀ ⦃s t : α⦄, P s → P t → P (s ⊓ t)) → DistribLattice (Subtype P)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.sset.congr_simp : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  fvarId = fvarId_1 →
    ∀ (i i_1 : ℕ),
      i = i_1 →
        ∀ (offset offset_1 : ℕ),
          offset = offset_1 →
            ∀ (y y_1 : Lean.FVarId),
              y = y_1 →
                ∀ (ty ty_1 : Lean.Expr),
                  ty = ty_1 →
                    ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
                      k = k_1 →
                        ∀ (h : pu = Lean.Compiler.LCNF.Purity.impure),
                          Lean.Compiler.LCNF.Code.sset fvarId i offset y ty k h =
                            Lean.Compiler.LCNF.Code.sset fvarId_1 i_1 offset_1 y_1 ty_1 k_1 h
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.hsymmPart.eq_1 : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] {n : ℕ}
  (μ : n.Partition), MvPolynomial.hsymmPart σ R μ = (Multiset.map (MvPolynomial.hsymm σ R) μ.parts).prod
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_cons : ∀ {m n : ℕ}, m < n → (m...n).toList = m :: ((m + 1)...n).toList
-- Std.Time.Date.Unit.Year
/-- Calculates the number of weeks in the specified `year`.
 -/
Std.Time.Year.Offset.weeks : Std.Time.Year.Offset → Std.Time.Internal.Bounded.LE 52 53
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Binary strict **rearrangement inequality**.  -/
mul_add_mul_lt_mul_add_mul : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b c d : R} [AddLeftReflectLT R] [ExistsAddOfLE R]
  [MulPosStrictMono R] [AddLeftStrictMono R], a < b → c < d → a * d + b * c < a * c + b * d
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldRevM_eq_foldrM_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → (a : α) → β a → m' δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRevM f init ↑m = List.foldrM (fun a b => f b a.fst a.snd) init (↑m).toList
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.one_vle_div_iff : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {a b : K}, b ≠ 0 → (1 ≤ᵥ a / b ↔ b ≤ᵥ a)
-- Aesop.RuleSet.Name
Aesop.builtinRuleSetName : Aesop.RuleSetName
-- Mathlib.RingTheory.SimpleModule.Isotypic
isFullyInvariant_iff_isTwoSided : ∀ {R : Type u_5} [inst : Semiring R] {I : Ideal R}, Submodule.IsFullyInvariant I ↔ I.IsTwoSided
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.mk_nsmul : ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ), DomAddAct.mk (n • a) = n • DomAddAct.mk a
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Erase a complete match.  -/
Aesop.ForwardRuleMatches.erase : Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatches → Aesop.ForwardRuleMatches
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.map.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq sq_1 : f ⟶ g)
  (e_sq : sq = sq_1) [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.Limits.image.map sq = CategoryTheory.Limits.image.map sq_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {len : ℕ} {lhs : aig.RefVec len}
  {bit : aig.Ref} {lhs_1 : aig.RefVec len} {bit_1 : aig.Ref},
  { lhs := lhs, bit := bit } = { lhs := lhs_1, bit := bit_1 } → lhs = lhs_1 ∧ bit = bit_1
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def : ∀ {α : Type u_2} (f : α → ℚ → ℝ) (a : α) (x : ℝ),
  ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a x = ⨅ q, f a ↑q
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.support_ker : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f],
  ↑(AlgebraicGeometry.Scheme.Hom.ker f).support = closure (Set.range ⇑f)
-- Lean.Declaration
Lean.ConstantInfo.recInfo : Lean.RecursorVal → Lean.ConstantInfo
-- Mathlib.Data.List.Sigma
List.kreplace_of_forall_not : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)},
  (∀ (b : β a), ⟨a, b⟩ ∉ l) → List.kreplace a b l = l
-- Mathlib.ModelTheory.Types
/-- The clopen set of complete types which contain a formula.  -/
FirstOrder.Language.Theory.typesWith : {L : FirstOrder.Language} → {α : Type w} → (T : L.Theory) → (L.withConstants α).Sentence → Set (T.CompleteType α)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symmL.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1) [inst_9 : Bundle.Trivialization.IsLinear R e]
  (b : B), Bundle.Trivialization.symmL R e b = Bundle.Trivialization.symmL R e_1 b
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
MeasureTheory.AEStronglyMeasurable.sinc : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => Real.sinc (f x)) μ
-- Mathlib.Order.Hom.CompleteLattice
/-- The proposition that a `sSupHom` commutes with arbitrary suprema/joins.  -/
sSupHom.map_sSup' : ∀ {α : Type u_8} {β : Type u_9} [inst : SupSet α] [inst_1 : SupSet β] (self : sSupHom α β) (s : Set α),
  self.toFun (sSup s) = sSup (self.toFun '' s)
-- Mathlib.NumberTheory.Dioph
Dioph.dioph_comp : ∀ {α : Type} {n : ℕ} {S : Set (Vector3 ℕ n)},
  Dioph S → ∀ (f : Vector3 ((α → ℕ) → ℕ) n), VectorAllP Dioph.DiophFn f → Dioph {v | (fun i => f i v) ∈ S}
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddZeroClass.eq_1 : ∀ {α : Type u_1} [inst : AddZeroClass α],
  Colex.instAddZeroClass = { toZero := Colex.instZero, toAdd := Colex.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
/-- An auxiliary lemma en route to `RootPairing.Base.lie_e_f_same`.  -/
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations.0.RootPairing.GeckConstruction.lie_e_f_same_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  (i : ↥b.support) [P.IsReduced] (k : ι),
  k ≠ ↑i →
    k ≠ (P.reflectionPerm ↑i) ↑i →
      ⁅RootPairing.GeckConstruction.e i, RootPairing.GeckConstruction.f i⁆ (Sum.inr k) (Sum.inr k) =
        RootPairing.GeckConstruction.h i (Sum.inr k) (Sum.inr k)
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.instInhabited : {α : Type u_1} → [inst : PseudoEMetricSpace α] → Inhabited (α →ᵈ α)
-- Mathlib.Dynamics.OmegaLimit
/-- The ω-limit w.r.t. `Filter.atTop`.  -/
omegaLimit.«termω⁺» : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffWithinAt.prodMk_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {s : Set M}
  {x : M} {n : WithTop ℕ∞} {f : M → E'} {g : M → F'},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n f s x →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n g s x →
      ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (E' × F')) n (fun x => (f x, g x)) s x
-- Mathlib.CategoryTheory.SmallObject.Basic
/-- A class of morphisms `I : MorphismProperty C` satisfies the property
`HasSmallObjectArgument.{w} I` if it permits the small object argument,
i.e. there exists a regular cardinal `κ : Cardinal.{w}` such that
`IsCardinalForSmallObjectArgument I κ` holds.  -/
CategoryTheory.MorphismProperty.HasSmallObjectArgument : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Data.Nat.Log
/-- For `b > 1`, `clog b` and `(b ^ ·)` form a Galois connection.

See also `clog_le_of_le_pow` for the implication that does not require `1 < b`.  -/
Nat.clog_le_iff_le_pow : ∀ {b : ℕ}, 1 < b → ∀ {x y : ℕ}, Nat.clog b x ≤ y ↔ x ≤ b ^ y
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.comp_assoc : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} {ι : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Semiring D] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Algebra R C] [inst_8 : Algebra R D] [inst_9 : DecidableEq ι] [inst_10 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} {𝒟 : ι → Submodule R D}
  [inst_11 : GradedAlgebra 𝒜] [inst_12 : GradedAlgebra ℬ] [inst_13 : GradedAlgebra 𝒞] [inst_14 : GradedAlgebra 𝒟]
  (fCD : 𝒞 →ₐᵍ[R] 𝒟) (fBC : ℬ →ₐᵍ[R] 𝒞) (fAB : 𝒜 →ₐᵍ[R] ℬ), (fCD.comp fBC).comp fAB = fCD.comp (fBC.comp fAB)
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_support : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq β] {f : α → β}
  {s : α →₀ M}, (Finsupp.mapDomain f s).support ⊆ Finset.image f s.support
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toRingEquiv_op : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B),
  (AlgEquiv.op f).toRingEquiv = RingEquiv.op f.toRingEquiv
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
/-- The `MonoidWithZero` version of `inv_mul_eq_inv_mul_iff_mul_eq_mul`.  -/
Commute.inv_mul_eq_inv_mul_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c d : G₀},
  Commute b d → b ≠ 0 → d ≠ 0 → (b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c)
-- Init.Data.SInt.Bitwise
Int64.toInt16_not : ∀ (a : Int64), (~~~a).toInt16 = ~~~a.toInt16
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.PredTrans.pushOption.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x