mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.alter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] (a : α)
  (f : Option (β a) → Option (β a)) (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.alter ⟨{ size := size, buckets := buckets }, hm⟩ a f =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bkt = true then
        let buckets' := buckets.uset i Std.DHashMap.Internal.AssocList.nil h;
        let bkt' := Std.DHashMap.Internal.AssocList.alter a f bkt;
        have size' := if Std.DHashMap.Internal.AssocList.contains a bkt' = true then size else size - 1;
        ⟨{ size := size', buckets := buckets'.uset i bkt' ⋯ }, ⋯⟩
      else
        match f none with
        | none => ⟨{ size := size, buckets := buckets }, hm⟩
        | some b =>
          have size' := size + 1;
          let buckets' := buckets.uset i (Std.DHashMap.Internal.AssocList.cons a b bkt) h;
          Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerDone_flatMapM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ : Std.IterM m β},
  it₁.IsPlausibleStep Std.IterStep.done → (Std.IterM.flatMapAfterM f it₁ none).IsPlausibleStep Std.IterStep.done
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.foldM.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (le : α → α → Bool)
  (s : Batteries.PairingHeapImp.Heap α) (init : β) (f : β → α → m β),
  Batteries.PairingHeapImp.Heap.foldM le s init f =
    match eq : Batteries.PairingHeapImp.Heap.deleteMin le s with
    | none => pure init
    | some (hd, tl) =>
      have this := ⋯;
      do
      let __do_lift ← f init hd
      Batteries.PairingHeapImp.Heap.foldM le tl __do_lift f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- If `t` is a limit pullback cone over `f` and `g` and `h : W ⟶ X` and `k : W ⟶ Y` are such that
`h ≫ f = k ≫ g`, then we have `l : W ⟶ t.pt` satisfying `l ≫ fst t = h` and `l ≫ snd t = k`.
 -/
CategoryTheory.Limits.PullbackCone.IsLimit.lift' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {t : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsLimit t →
              {W : C} →
                (h : W ⟶ X) →
                  (k : W ⟶ Y) →
                    CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g →
                      { l //
                        CategoryTheory.CategoryStruct.comp l t.fst = h ∧
                          CategoryTheory.CategoryStruct.comp l t.snd = k }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], k ∉ t₁ → (t₁ \ t₂).get! k = default
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.lift.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) [inst_2 : I.IsPrime]
  (f f_1 : R →+* S) (e_f : f = f_1) (hf₁ : I ≤ RingHom.ker f)
  (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)),
  Ideal.ResidueField.lift I f hf₁ hf₂ = Ideal.ResidueField.lift I f_1 ⋯ ⋯
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
/-- The length of an object in `SemiSimplexCategory`  -/
SemiSimplexCategory.len : SemiSimplexCategory → ℕ
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.inl_ne_inr : ∀ (X Y : AlgebraicGeometry.Scheme) (x : ↥X) (y : ↥Y),
  CategoryTheory.Limits.coprod.inl x ≠ CategoryTheory.Limits.coprod.inr y
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.instForwardPatternForallCharBool : {p : Char → Bool} → String.Slice.Pattern.ForwardPattern p
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.eraseVars : Lean.Elab.Term.Do.VarSet → Array Lean.Elab.Term.Do.Var → Lean.Elab.Term.Do.VarSet
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_injective : ∀ {R : Type u_1} {A : Type u_2} [inst : Zero R], Function.Injective Unitization.inr
-- Mathlib.Analysis.Normed.Group.Defs
AddGroupNorm.toNormedAddGroup.eq_1 : ∀ {E : Type u_5} [inst : AddGroup E] (f : AddGroupNorm E),
  f.toNormedAddGroup =
    { toNorm := f.toSeminormedAddGroup.toNorm, toAddGroup := f.toSeminormedAddGroup.toAddGroup,
      toPseudoMetricSpace := f.toSeminormedAddGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.ext_iff : ∀ {X Y : AddMonCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_iff_submodule_quotient : ∀ {R : Type u_1} {N : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] (S : Submodule R N),
  IsNoetherian R N ↔ IsNoetherian R ↥S ∧ IsNoetherian R (N ⧸ S)
-- Mathlib.Algebra.Regular.SMul
/-- A product is `M`-regular if and only if the factors are.  -/
IsSMulRegular.mul_iff : ∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : CommSemigroup R] [inst_1 : SMul R M] [IsScalarTower R R M],
  IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
-- Mathlib.Computability.Language
Language.mem_inf : ∀ {α : Type u_1} {x : List α} {l m : Language α}, x ∈ l ⊓ m ↔ x ∈ l ∧ x ∈ m
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_finset_sdiff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s t : Finset β} {a : α}, a ≠ 0 → a • (s \ t) = a • s \ a • t
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv'_symm_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C}
  [inst_2 : CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] {n a : ℤ}
  (x y :
    Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X))
  (a' : ℤ) (h : n + a = a'),
  (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm (x + y) =
    (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm x + (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm y
-- Batteries.Tactic.Lint.Frontend
/-- Traces via `IO.println` if `inIO` is `true`, and via `trace[...]` otherwise. Prepends
`currentModule` and `linter` (if present).

This declaration is `macro_inline`, so it should have the same thunky behavior as `trace[...]`.  -/
Batteries.Tactic.Lint.traceLint : String → Bool → optParam (Option Lean.Name) none → optParam (Option Lean.Name) none → Lean.CoreM Unit
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isCodetecting_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C),
  P.op.IsCodetecting ↔ P.IsDetecting
-- Mathlib.Algebra.Lie.Nilpotent
Function.Surjective.lieModule_lcs_map_eq : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] {L₂ : Type u_1}
  {M₂ : Type u_2} [inst_7 : LieRing L₂] [inst_8 : LieAlgebra R L₂] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : LieRingModule L₂ M₂] {f : L →ₗ⁅R⁆ L₂} {g : M →ₗ[R] M₂},
  (∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) →
    ∀ [LieModule R L₂ M₂],
      Function.Surjective ⇑f →
        Function.Surjective ⇑g →
          ∀ (k : ℕ), Submodule.map g ↑(LieModule.lowerCentralSeries R L M k) = ↑(LieModule.lowerCentralSeries R L₂ M₂ k)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.let : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetDecl pu → Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_add_two_pi : ∀ (x : ℂ), Complex.cos (x + 2 * ↑Real.pi) = Complex.cos x
-- Mathlib.Algebra.Order.Interval.Basic
Interval.bot_div : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : CommGroup α] [inst_2 : MulLeftMono α] (t : Interval α), ⊥ / t = ⊥
-- Mathlib.Order.Interval.Finset.Defs
Finset.card_Iic_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : LocallyFiniteOrderBot β] [inst_4 : DecidableLE (α × β)] (x : α × β),
  (Finset.Iic x).card = (Finset.Iic x.1).card * (Finset.Iic x.2).card
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.IsOneHypercoverDense.nonempty_oneHypercoverDenseData : ∀ {C₀ : Type u₀} {C : Type u} {inst : CategoryTheory.Category.{v₀, u₀} C₀} {inst_1 : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} [self : F.IsOneHypercoverDense J₀ J] (X : C),
  Nonempty (F.OneHypercoverDenseData J₀ J X)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
standardBorel_of_polish : ∀ {α : Type u_1} [inst : MeasurableSpace α] [τ : TopologicalSpace α] [BorelSpace α] [PolishSpace α],
  StandardBorelSpace α
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectROfProdMk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))],
  NeZero ((κ.sectR a) b)
-- Mathlib.Computability.Partrec
Nat.rfind_dom : ∀ {p : ℕ →. Bool}, (Nat.rfind p).Dom ↔ ∃ n, true ∈ p n ∧ ∀ {m : ℕ}, m < n → (p m).Dom
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateConst! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu →
    Lean.Name → List Lean.Level → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Std.Data.TreeMap.Lemmas
_private.Std.Data.TreeMap.Lemmas.0.GetElem?.match_1.splitter : (elem : outParam (Type u_1)) →
  (motive : Option elem → Sort u_2) →
    (x : Option elem) → ((e : elem) → motive (some e)) → (Unit → motive none) → motive x
-- Mathlib.LinearAlgebra.RootSystem.Reduced
/-- See also `RootPairing.pairingIn_neg_two_neg_two_iff`.  -/
RootPairing.pairing_neg_two_neg_two_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι) [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M], P.pairing i j = -2 ∧ P.pairing j i = -2 ↔ P.root i = -P.root j
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDTreeMap.filterMap f t).get? k = (t.get? k).bind (f k)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUdiv : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.sum_chartAt_inl : ∀ {H : Type u} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] (x : M),
  chartAt H (Sum.inl x) = (chartAt H x).lift_openEmbedding ⋯
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.abs_sub_coe_le_dist : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f g : BoundedContinuousFunction α β) {x : α}, ‖f x - g x‖ ≤ dist f g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_insertMany_list_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List (α × β)}, (Std.DHashMap.Raw.Const.insertMany m l).size ≤ m.size + l.length
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- `f` has the derivative `f'` at the point `x` along the direction `v`.
That is, `f (x + t v) = f x + t • f' + o (t)` when `t` tends to `0`.
Note that this definition is less well behaved than the total Fréchet derivative, which
should generally be favored over this one.  -/
HasLineDerivAt : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} →
      [inst_1 : NormedAddCommGroup F] →
        [NormedSpace 𝕜 F] → {E : Type u_3} → [inst_3 : AddCommGroup E] → [Module 𝕜 E] → (E → F) → F → E → E → Prop
-- Mathlib.Logic.Function.Basic
Function.Involutive.bijective : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.Bijective f
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.logDeriv_one_sub_mul_cexp_comp : ∀ (r : ℂ) {g : ℂ → ℂ},
  Differentiable ℂ g →
    logDeriv ((fun z => 1 - r * Complex.exp z) ∘ g) = fun z =>
      -r * deriv g z * Complex.exp (g z) / (1 - r * Complex.exp (g z))
-- Mathlib.Control.ULift
/-- Embedding of pure values.  -/
PLift.pure : {α : Sort u} → α → PLift α
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Result : Type
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- For a given recursive call, and a choice of parameter and argument index,
try to prove equality, < or ≤.
 -/
Lean.Elab.WF.GuessLex.evalRecCall : Lean.Name →
  Option Lean.Elab.DecreasingBy →
    Array Lean.Elab.WF.GuessLex.BasicMeasure →
      Array Lean.Elab.WF.GuessLex.BasicMeasure →
        Lean.Elab.WF.GuessLex.RecCallWithContext → ℕ → ℕ → Lean.MetaM Lean.Elab.WF.GuessLex.GuessLexRel
-- Lean.Meta.Sym.Pattern
/-- Helper function for checking whether types `α` and `β` are definitionally equal during unification/matching.  -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqTypes : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.mk.sizeOf_spec : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} [inst_2 : SizeOf V] (hom : u.right ⟶ v.left)
  (comm :
    autoParam
      (CategoryTheory.Arrow.Hom.right f - CategoryTheory.Arrow.Hom.right g =
        CategoryTheory.CategoryStruct.comp hom v.hom)
      CategoryTheory.Arrow.RightHomotopy.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1 + sizeOf hom + sizeOf comm
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch : Type
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.instIsNegInvariantCount : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableNeg G],
  MeasureTheory.Measure.count.IsNegInvariant
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
/-- Interpret a homogeneous `DirectSum` as an `AddMonoidAlgebra`.  -/
DirectSum.toAddMonoidAlgebra : {ι : Type u_1} →
  {M : Type u_3} →
    [DecidableEq ι] →
      [inst : Semiring M] → [(m : M) → Decidable (m ≠ 0)] → (DirectSum ι fun x => M) → AddMonoidAlgebra M ι
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.comm_symm_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) (n : N),
  (TensorProduct.comm R M N).symm (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
/-- Typeclass characterising splitting fields.  -/
Polynomial.IsSplittingField : (K : Type v) → (L : Type w) → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → Polynomial K → Prop
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_C_mul_X_pow : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R],
  a ≠ 0 → ∀ (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).roots = n • {0}
-- Std.Sync.Mutex
_private.Std.Sync.Mutex.0.Std.CondvarImpl : NonemptyType
-- Mathlib.GroupTheory.Nilpotent
commGroupOfNilpotencyClass.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Group.IsNilpotent G] (h : Group.nilpotencyClass G ≤ 1),
  commGroupOfNilpotencyClass h = Group.commGroupOfCenterEqTop ⋯
-- Mathlib.Data.Bool.Count
List.count_not_add_count : ∀ (l : List Bool) (b : Bool), List.count (!b) l + List.count b l = l.length
-- Mathlib.Data.Finset.Update
Function.updateFinset_restrict : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] {s : Finset ι} (x : (i : ι) → π i),
  Function.updateFinset x s (s.restrict x) = x
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndunion_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.Nodup → s.ndunion t = s ∪ t
-- Mathlib.Topology.Sheaves.AddCommGrpCat
TopCat.Presheaf.restrict_sum : ∀ {X : TopCat} {U V : TopologicalSpace.Opens ↑X} {F : TopCat.Presheaf AddCommGrpCat X} (h : V ≤ U)
  (s t : ↑(F.obj (Opposite.op U))),
  TopCat.Presheaf.restrictOpen (s + t) V h = TopCat.Presheaf.restrictOpen s V h + TopCat.Presheaf.restrictOpen t V h
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_add : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : CommSemiring R] (M N : Matrix m n R),
  (M + N).toMvPolynomial = M.toMvPolynomial + N.toMvPolynomial
-- Lean.Attributes
Lean.AttributeImpl.erase : Lean.AttributeImpl → Lean.Name → Lean.AttrM Unit
-- Mathlib.Order.Defs.LinearOrder
max_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, b < a → c < a → max b c < a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblU_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} (P : Fin 3 → F),
  W.dblU P = (W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2)) ^ 3 / P 2 ^ 2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.contDiff_cosh : ∀ {n : WithTop ℕ∞}, ContDiff ℂ n Complex.cosh
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_eq_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : LawfulBEq α]
  [inst_1 : Inhabited β] {a : α}, Std.ExtDHashMap.Const.get! m a = m.get! a
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.one_le_abs : ∀ {z : ℤ}, z ≠ 0 → 1 ≤ |z|
-- Init.Data.String.Basic
String.Pos.Raw.utf8SetAux_of_gt : ∀ (c' : Char) (cs : List Char) {i p : String.Pos.Raw}, i > p → String.Pos.Raw.utf8SetAux c' cs i p = cs
-- Mathlib.LinearAlgebra.Dual.Lemmas
TensorProduct.dualDistrib_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : Module.Dual R M) (g : Module.Dual R N)
  (m : M) (n : N), ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = f m * g n
-- Mathlib.GroupTheory.Sylow
IsPGroup.inf_normalizer_sylow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P : Subgroup G},
  IsPGroup p ↥P → ∀ (Q : Sylow p G), P ⊓ Subgroup.normalizer ↑Q = P ⊓ ↑Q
-- Mathlib.Order.BooleanAlgebra.Set
Set.pair_sdiff_left : ∀ {α : Type u_1} {a b : α}, a ≠ b → {a, b} \ {a} = {b}
-- Aesop.Tree.Data
Aesop.RappId.mk.injEq : ∀ (toNat toNat_1 : ℕ), ({ toNat := toNat } = { toNat := toNat_1 }) = (toNat = toNat_1)
-- Mathlib.Algebra.Group.Int.Units
Int.isUnit_add_isUnit_eq_isUnit_add_isUnit : ∀ {a b c d : ℤ}, IsUnit a → IsUnit b → IsUnit c → IsUnit d → (a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c)
-- Mathlib.Order.Atoms
isCoatom_iff_eq_bot : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α] {a : α}, IsCoatom a ↔ a = ⊥
-- Mathlib.LinearAlgebra.Prod
LinearMap.snd_comp_inr : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂ = LinearMap.id
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.of_isPullback : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  {UX UY : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine UY] {iY : UY ⟶ Y}
  [AlgebraicGeometry.IsOpenImmersion iY] {iX : UX ⟶ X} {f' : UX ⟶ UY}, CategoryTheory.IsPullback iX f' f iY → P f → Q f'
-- Lean.Meta.Tactic.Simp.Types
/-- `Simproc` entry. It is the .olean entry plus the actual function.
 -/
Lean.Meta.Simp.SimprocEntry : Type
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) [inst_3 : CategoryTheory.Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
  [inst_4 : CategoryTheory.Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)], hS.cokerIsoKer k hk = hS.cokerIsoKer k hk
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.coneOfHasLimitEval_π_app_f : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))] (j : J) (x : ι),
  ((HomologicalComplex.coneOfHasLimitEval F).π.app j).f x =
    CategoryTheory.Limits.limit.π (F.comp (HomologicalComplex.eval C c x)) j
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The chosen end of a functor `Jᵒᵖ ⥤ J ⥤ C`.  -/
CategoryTheory.Limits.chosenEnd : {J : Type u_3} →
  {C : Type u_4} →
    [inst : CategoryTheory.Category.{v_3, u_4} C] →
      [inst_1 : CategoryTheory.Category.{v_4, u_3} J] →
        CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C) → [CategoryTheory.Limits.ChosenEndsOfShape J C] → C
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`.  -/
Localization.awayMap : {R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Type u_3} →
      [inst_1 : CommSemiring P] → (f : R →+* P) → (r : R) → Localization.Away r →+* Localization.Away (f r)
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.prod_apply : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : M →+ N) (g : M →+ P) (x : M), (f.prod g) x = (f x, g x)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.BifibrantObject C} (f : X ⟶ Y) [hf : HomotopicalAlgebra.WeakEquivalence f],
  CategoryTheory.IsIso (HomotopicalAlgebra.BifibrantObject.toHoCat.map f)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_get_eq : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {k v : α} {w : k ∈ m}, m.get k w = v → k ∈ m
-- Lean.Compiler.LCNF.Basic
/-- Declaration being processed by the Lean to Lean compiler passes.
 -/
Lean.Compiler.LCNF.Decl : Lean.Compiler.LCNF.Purity → Type