mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) (p q n : ℤ) (h : p + n = q),
  CochainComplex.HomComplex.Cochain.fromSingleMk 0 h = 0
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.nsmul_atTop : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f : α → M}, Filter.Tendsto f l Filter.atTop → ∀ {n : ℕ}, 0 < n → Filter.Tendsto (fun x => n • f x) l Filter.atTop
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.hasBasis_nhds_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (nhds OnePoint.infty).HasBasis (fun s => IsClosed s ∧ IsCompact s) fun s => OnePoint.some '' sᶜ ∪ {OnePoint.infty}
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` is lower hemicontinuous if, for any `x`, whenever `t` is an open set
intersecting `f x`, then `t` also intersects `f x'` for all `x'` sufficiently close to `x`.  -/
LowerHemicontinuous : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → Prop
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ ∈ m), m.get k₁ h₁ = m.get k₂ ⋯
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isBasis'_iff_isBasis_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X
-- Mathlib.Order.Antisymmetrization
/-- The antisymmetrization relation as an equivalence relation.  -/
AntisymmRel.setoid : (α : Type u_1) → (r : α → α → Prop) → [IsPreorder α r] → Setoid α
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)}
  {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) = true →
      Std.Internal.List.containsKey k l = true
-- Mathlib.Data.Num.Lemmas
Num.ofNat'_eq : ∀ (n : ℕ), Num.ofNat' n = ↑n
-- Mathlib.Topology.Homotopy.LocallyContractible
ContinuousMap.inclusion.congr_simp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} (h : s ⊆ t),
  ContinuousMap.inclusion h = ContinuousMap.inclusion h
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalGroup.isInducing_iff_nhds_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {H : Type u_1} [inst_3 : Group H]
  [inst_4 : TopologicalSpace H] [IsTopologicalGroup H] {F : Type u_2} [inst_6 : FunLike F G H] [MonoidHomClass F G H]
  {f : F}, Topology.IsInducing ⇑f ↔ nhds 1 = Filter.comap (⇑f) (nhds 1)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_const_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x * a) '' Set.Iio b = Set.Iio (b * a)
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- **Alias** of `WithAbs.moduleLeft`. -/
WithAbs.instModule_left : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        {T : Type u_4} →
          [inst_2 : Semiring R] →
            (v : AbsoluteValue R S) → [inst_3 : AddCommMonoid T] → [Module R T] → Module (WithAbs v) T
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.instFullIncl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.WithInitial.incl.Full
-- Std.Net.Addr
Std.Net.AddressFamily.ipv6.sizeOf_spec : sizeOf Std.Net.AddressFamily.ipv6 = 1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat : Lean.Expr →
  Lean.Expr →
    ℕ →
      Lean.Meta.Grind.Arith.Linear.LinExpr →
        Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_iff_of_associated : ∀ {α : Type u} [inst : CommSemiring α] {I : Ideal α} {x y : α}, Associated x y → (x ∈ I ↔ y ∈ I)
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NonAssocCommRing.mul_comm : ∀ {α : Type u} [self : NonAssocCommRing α] (a b : α), a * b = b * a
-- Init.Prelude
/-- A node in the syntax tree that may have further syntax as child nodes. The node's `kind`
determines its interpretation.

For nodes produced by the parser, the `info` field is typically `Lean.SourceInfo.none`, and source
information is stored in the corresponding fields of identifiers and atoms. This field is used in
two ways:
 1. The delaborator uses it to associate nodes with metadata that are used to implement
    interactive features.
 2. Nodes created by quotations use the field to mark the syntax as synthetic (storing the result
    of `Lean.SourceInfo.fromRef`) even when its leading or trailing tokens are not.
 -/
Lean.Syntax.node : Lean.SourceInfo → Lean.SyntaxNodeKind → Array Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.quotientMk_of : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} (i : ι) (x : G i),
  (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (FreeCommRing.of ⟨i, x⟩) =
    (Ring.DirectLimit.of G f i) x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_comap_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (S : Subsemigroup N),
  Subsemigroup.map f (Subsemigroup.comap f S) = S ⊓ f.srange
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.sum_le' : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : Finset α},
  (∀ i ∈ s, padicNorm p (F i) ≤ t) → 0 ≤ t → padicNorm p (∑ i ∈ s, F i) ≤ t
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `L` with the spectral norm is a `NormedAlgebra` over any intermediate `E`
that is a normed algebra over `K`.  -/
spectralNorm.normedAlgebra' : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    [hu : IsUltrametricDist K] →
      [inst_1 : CompleteSpace K] →
        (E : Type u_2) →
          (L : Type u_3) →
            [inst_2 : Field L] →
              [inst_3 : Algebra K L] →
                [inst_4 : Algebra.IsAlgebraic K L] →
                  [inst_5 : NormedField E] →
                    [inst_6 : NormedAlgebra K E] → [inst_7 : Algebra E L] → [IsScalarTower K E L] → NormedAlgebra E L
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a a_1 : Associates α),
  a = a_1 → a.factors = a_1.factors
-- Init.Data.Option.Lemmas
Option.isSome_of_mem : ∀ {α : Type u_1} {x : Option α} {y : α}, y ∈ x → x.isSome = true
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred
Std.Tactic.BVDecide.BVPred.denote_bitblast : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig input.cache →
    ⟦assign.toAIGAssignment,
        { aig := (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).aig,
          ref := (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).ref }⟧ =
      Std.Tactic.BVDecide.BVPred.eval assign input.val
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- A non-unital star algebra homomorphism of complex C⋆-algebras is norm contractive.  -/
NonUnitalStarAlgHom.norm_apply_le : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (a : A), ‖φ a‖ ≤ ‖a‖
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.isNat_prime_2 : ∀ {n n' : ℕ},
  Mathlib.Meta.NormNum.IsNat n n' → Nat.ble 2 n' = true → Mathlib.Meta.NormNum.IsNat n'.minFac n' → Nat.Prime n
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.val_pow : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  (a : GroupLike R A) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.zpow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, MeromorphicAt f x → ∀ (n : ℤ), MeromorphicAt (f ^ n) x
-- Init.Data.List.Lemmas
List.eq_or_mem_of_mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l → a = b ∨ a ∈ l
-- Lean.Elab.PreDefinition.Main
Lean.Elab.shouldUsePartialFixpoint : Array Lean.Elab.PreDefinition → Bool
-- Mathlib.Order.Lattice
Function.update_inf : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → SemilatticeInf (π i)] (f : (i : ι) → π i)
  (i : ι) (a b : π i), Function.update f i (a ⊓ b) = Function.update f i a ⊓ Function.update f i b
-- Init.Data.Iterators.Consumers.Monadic.Total
/-- For an iterator `it`, `it.ensureTermination` provides variants of consumers that always
terminate.
 -/
Std.IterM.ensureTermination : {α β : Type w} → {m : Type w → Type w'} → Std.IterM m β → Std.IterM.Total m β
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.get? (t.minD fallback) = some (t.minD fallback)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.altsInfo : Lean.Meta.ElimInfo → Array Lean.Meta.ElimAltInfo
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instMul : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : Mul γ] → [ContinuousMul γ] → Mul (α →ₘ[μ] γ)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- **Alias** of `hasFDerivAt_finsetProd`. -/
hasFDerivAt_finset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} [inst_3 : DecidableEq ι] [Finite ι] {x : ι → 𝔸'},
  HasFDerivAt (fun x => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • ContinuousLinearMap.proj i) x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_fst' : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ⇑(ContinuousLinearMap.fst R M₁ M₂) = Prod.fst
-- Mathlib.Data.Set.Function
Function.invFunOn_neg : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [inst : Nonempty α],
  (¬∃ a ∈ s, f a = b) → Function.invFunOn f s b = Classical.choice inst
-- Batteries.CodeAction.Attr
Batteries.CodeAction.instInhabitedTacticCodeActions.default : Batteries.CodeAction.TacticCodeActions
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.symm_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  e.symm.target = e.source
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.centralizer_univ : ∀ (M : Type u_1) [inst : AddSemigroup M], AddSubsemigroup.centralizer Set.univ = AddSubsemigroup.center M
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
/-- Every maximal ideal of a commutative Noetherian total ring of fractions `A` is
an associated prime of the `A`-module `A`.  -/
Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRing : ∀ (A : Type u) [inst : CommRing A] [IsNoetherianRing A] [IsFractionRing A A] (I : Ideal A) [hI : I.IsMaximal],
  I ∈ associatedPrimes A A
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.step.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (upper : α),
  { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper }.step = Std.IterStep.done
-- Mathlib.Condensed.Explicit
/-- A `CondensedMod` version of `Condensed.ofSheafCompHaus`.  -/
CondensedMod.ofSheafCompHaus : (R : Type (u + 1)) →
  [inst : Ring R] →
    (F : CategoryTheory.Functor CompHausᵒᵖ (ModuleCat R)) →
      [CategoryTheory.Limits.PreservesFiniteProducts F] →
        CategoryTheory.regularTopology.EqualizerCondition F → CondensedMod R
-- Mathlib.Data.Finset.Update
Function.updateFinset_updateFinset_of_subset : ∀ {ι : Type u_1} {π : ι → Sort u_2} [inst : DecidableEq ι] {s t : Finset ι},
  s ⊆ t →
    ∀ (x : (i : ι) → π i) (y : (i : ↥s) → π ↑i) (z : (i : ↥t) → π ↑i),
      Function.updateFinset (Function.updateFinset x s y) t z = Function.updateFinset x t z
-- Lean.Server.References
Lean.Server.RefInfo.mk.inj : ∀ {definition : Option Lean.Server.Reference} {usages : Array Lean.Server.Reference}
  {definition_1 : Option Lean.Server.Reference} {usages_1 : Array Lean.Server.Reference},
  { definition := definition, usages := usages } = { definition := definition_1, usages := usages_1 } →
    definition = definition_1 ∧ usages = usages_1
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n f (insert x s) x
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unoneD_eq_unone : ∀ {α : Type u} {d : α} {x : WithOne α} (hx : x ≠ 1), WithOne.unoneD d x = WithOne.unone hx
-- Mathlib.Data.EReal.Inv
EReal.inv_nonneg_of_nonneg : ∀ {a : EReal}, 0 ≤ a → 0 ≤ a⁻¹
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.scalarTensorEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : CommMonoid M] (m : M) (a : A),
  (MonoidAlgebra.scalarTensorEquiv R A).symm (MonoidAlgebra.single m a) = a ⊗ₜ[R] MonoidAlgebra.single m 1
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans'_source : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z)
  (h : e.target = e'.source), (e.trans' e' h).source = e.source
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.neg : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasFiniteRange → (-f).HasFiniteRange
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.name : {Self : Type} → Lean.Lsp.DocumentSymbolAux Self → String
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.zero_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), ↑0 n = 0
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Inserts the handler into the trie. The expectation is that a handler is not already
installed at a given key (use `HandlerTrie.find?` to verify this ahead of time),
but it is implemented to replace handlers.

`EvalConfigItemHandler.key` is modified
 -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.insert : Lean.Elab.ConfigEval.HandlerTrie✝ →
  (h : Lean.Elab.ConfigEval.EvalConfigItemHandler) → optParam Lean.Name h.key → Lean.Elab.ConfigEval.HandlerTrie✝
-- Init.Data.Iterators.Basic
/-- Termination measure to be used in well-founded recursive functions recursing over a productive
iterator (see also `Productive`).
 -/
Std.IterM.finitelyManySkips : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.Iterators.Productive α m] → Std.IterM m β → Std.IterM.TerminationMeasures.Productive α m
-- Mathlib.Order.BooleanAlgebra.Set
/-- See also `Set.inter_sdiff_assoc`.  -/
Set.sdiff_inter_right_comm : ∀ {α : Type u_1} (s t u : Set α), s \ t ∩ u = (s ∩ u) \ t
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
WfDvdMonoid.iff_wellFounded_associates : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α], WfDvdMonoid α ↔ WellFoundedLT (Associates α)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (W : Submodule R M)
  (φ : ↥W.dualAnnihilator) (x : M), (W.dualQuotEquivDualAnnihilator.symm φ) (Submodule.Quotient.mk x) = φ x
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  RingHom.ker (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app I.subschemeι ↑U)) = I.ideal U
-- Mathlib.Algebra.Torsor.Basic
vadd_vsub_vadd_cancel_left : ∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] (v : G) (p₁ p₂ : P),
  (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂
-- Mathlib.Order.Monotone.MonovaryOrder
/-- **Alias** of the forward direction of `monovary_iff_exists_antitone`. -/
Monovary.exists_antitone : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Monovary f g → ∃ x, Antitone f ∧ Antitone g
-- Mathlib.Order.Fin.Basic
/-- A function `f` on `Fin (n + 1)` is antitone if and only if `f (i + 1) ≤ f i` for all `i`.  -/
Fin.antitone_iff_succ_le : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α}, Antitone f ↔ ∀ (i : Fin n), f i.succ ≤ f i.castSucc
-- Lean.ExtraModUses
Lean.indirectModUseExt : Lean.SimplePersistentEnvExtension Lean.IndirectModUse (Std.HashMap Lean.Name (Array Lean.ModuleIdx))
-- Init.Data.SInt.Lemmas
Int16.toBitVec_toInt8 : ∀ (x : Int16), x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `S` is the localization of `R` at `r`, this is the canonical submersive presentation
of `S` as `R`-algebra.  -/
Algebra.SubmersivePresentation.localizationAway : {R : Type u} →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (r : R) → [IsLocalization.Away r S] → Algebra.SubmersivePresentation R S Unit Unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.add_point : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} (P Q : W.Point),
  (P + Q).point = W.addMap P.point Q.point
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_add_left_zero : ∀ {α : Type u_2} [inst : AddGroup α] {a : α}, Finset.preimage 0 (fun x => a + x) ⋯ = {-a}
-- Mathlib.Algebra.Group.Prod
Prod.instAddCommGroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H],
  Prod.instAddCommGroup = { toAddGroup := Prod.instAddGroup, add_comm := ⋯ }
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.id_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (A : Rep.{w, u, v} k G) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.complete_graph_degree : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (v : V),
  (SimpleGraph.completeGraph V).degree v = Fintype.card V - 1
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_psigma : ∀ {α : Sort u_5} {E : α → Sort u_4}, IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.skipPrefix?_string_eq_some_iff : ∀ {pat s : String} {pos : s.Pos}, s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat t
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
cfc_tsub : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : PartialOrder A] [inst_3 : StarRing A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [IsTopologicalRing A] [T2Space A]
  [inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (f g : NNReal → NNReal)
  (a : A),
  (∀ x ∈ spectrum NNReal a, g x ≤ f x) →
    autoParam (0 ≤ a) cfc_tsub._auto_1 →
      autoParam (ContinuousOn f (spectrum NNReal a)) cfc_tsub._auto_3 →
        autoParam (ContinuousOn g (spectrum NNReal a)) cfc_tsub._auto_5 → cfc (fun x => f x - g x) a = cfc f a - cfc g a
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.NoRepetition.append_singleton_of_not_suffix : ∀ {α : Type u} {a : α} {l : List α}, NoRepetition✝ a l → ¬[a] <:+ l → NoRepetition✝ a (l ++ [a])
-- Mathlib.Topology.CompactOpen
ContinuousMap.eventually_mapsTo : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {K : Set X} {U : Set Y}
  {f : C(X, Y)}, IsCompact K → IsOpen U → Set.MapsTo (⇑f) K U → ∀ᶠ (g : C(X, Y)) in nhds f, Set.MapsTo (⇑g) K U
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.toMonoid.unique : ∀ {α : Type u_3} {M : Type u_4} [inst : AddMonoid M] (f : α → M) {rels : FreeAddMonoid α → FreeAddMonoid α → Prop}
  (h : ∀ (a b : FreeAddMonoid α), rels a b → (FreeAddMonoid.lift f) a = (FreeAddMonoid.lift f) b)
  (g : (addConGen rels).Quotient →+ M),
  (∀ (a : α), g (PresentedAddMonoid.of rels a) = f a) → g = PresentedAddMonoid.lift f h
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.Fib.map_homMk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a b : HasFibers.Fib p S}
  (φ : (HasFibers.ι S).obj a ⟶ (HasFibers.ι S).obj b) [inst_3 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ],
  (HasFibers.ι S).map (HasFibers.Fib.homMk φ) = φ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback_hom_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : CategoryTheory.IsPullback fst snd f g)
  (h' : CategoryTheory.IsPullback fst' snd' f g) {Z_1 : C} (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').hom
      (CategoryTheory.CategoryStruct.comp fst' h_1) =
    CategoryTheory.CategoryStruct.comp fst h_1
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.precompose`.

---

Functorially precompose a cocone for `F` by a natural transformation `G ⟶ F` to give a cocone
for `G`.  -/
CategoryTheory.Limits.Cocones.postcompose : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (G ⟶ F) → CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone G)
-- Mathlib.Order.Disjointed
biUnion_Ioc_disjointed_of_monotone : ∀ {α : Type u_3} {ι : Type u_4} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : OrderBot ι]
  {f : ι → Set α}, Monotone f → ∀ {m n : ι}, n ≤ m → ⋃ i ∈ Finset.Ioc n m, disjointed f i = f m \ f n
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ioo_left : ∀ {α : Type v} [inst : Preorder α] [NoMinOrder α] (a : α), ⋃ b, Set.Ioo b a = Set.Iio a