mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isNoncomputable : Lean.Elab.Modifiers → Bool
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Finset «$α»)} (a : Q(«$α»)) (s' : Q(Finset «$α»)) (h : Q(«$a» ∉ «$s'»))
  (pf : Q(«$s» = Finset.cons «$a» «$s'» «$h»)) (a_1 : Q(«$α»)) (s'_1 : Q(Finset «$α»)) (h_1 : Q(«$a_1» ∉ «$s'_1»))
  (pf_1 : Q(«$s» = Finset.cons «$a_1» «$s'_1» «$h_1»)),
  (Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons a s' h pf =
      Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons a_1 s'_1 h_1 pf_1) =
    (a = a_1 ∧ s' = s'_1 ∧ h = h_1 ∧ pf = pf_1)
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailEIOOfNonempty : {ε : Type} → [Nonempty ε] → Lean.Order.MonadTail (EIO ε)
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.private : {α : Type} → Lean.VisibilityMap✝ α → α
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.corootSpace_eq_bot_iff : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L]
  [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L},
  LieAlgebra.corootSpace ⇑α = ⊥ ↔ α.IsZero
-- Lean.Elab.App
/-- When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`.
This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied.  -/
Lean.Elab.Term.LValResolution.projFn : Lean.Name → Lean.Name → Lean.Name → List Lean.Level → Lean.Elab.Term.LValResolution
-- Mathlib.Data.Seq.Basic
Stream'.Seq.enum_nil : ∀ {α : Type u}, Stream'.Seq.nil.enum = Stream'.Seq.nil
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} (h : t.WF),
  Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.filterMap f t) k =
    (Std.DTreeMap.Raw.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x
-- Mathlib.Order.SuccPred.Tree
RootedTree.subtree_root : ∀ (t : RootedTree) (v : SubRootedTree t), t.subtree v.root = v
-- Mathlib.CategoryTheory.Localization.Prod
CategoryTheory.Localization.Construction.prodIsLocalization : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [W₁.ContainsIdentities] [W₂.ContainsIdentities],
  (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)
-- Mathlib.CategoryTheory.SingleObj
MonCat.toCat_faithful : MonCat.toCat.Faithful
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ι_functorMapSrc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  (i : I) (t : A i ⟶ X) (b : B i ⟶ S)
  (w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b) (b' : B i ⟶ T)
  (hb' : CategoryTheory.CategoryStruct.comp b (CategoryTheory.Arrow.Hom.right τ) = b') (t' : A i ⟶ Y)
  (ht' : CategoryTheory.CategoryStruct.comp t (CategoryTheory.Arrow.Hom.left τ) = t') {Z : C}
  (h : ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πY ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjSrcFamily f πX)
        { i := i, t := t, b := b, w := w })
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapSrc f τ) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjSrcFamily f πY)
        { i := i, t := t', b := b', w := ⋯ })
      h
-- Mathlib.Topology.Neighborhoods
nhdsWithin.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X) (s : Set X), nhdsWithin x s = nhds x ⊓ Filter.principal s
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.Integrable.norm_integral_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F],
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable (fun ω => ‖∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω‖) μ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_10 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.arithShiftRight rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_10 w n lhs rhs
-- Init.Data.SInt.Lemmas
Int8.ofInt_eq_ofIntLE_mod : ∀ {a b : ℤ} (ha₁ : Int8.minValue.toInt ≤ a) (ha₂ : a ≤ Int8.maxValue.toInt) (hb₁ : Int8.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int8.maxValue.toInt), Int8.ofInt (a.tmod b) = Int8.ofIntLE a ha₁ ha₂ % Int8.ofIntLE b hb₁ hb₂
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.toHNot : {α : Type u_8} → [self : CompleteLinearOrder α] → HNot α
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressParams.toJson : Lean.Lsp.WorkDoneProgressParams → Lean.Json
-- Lean.Meta.Tactic.Grind.Proof
/-- Given `lhs` and `rhs` that are in the same equivalence class,
find the common expression that are in the paths from `lhs` and `rhs` to
the root of their equivalence class.
Recall that this expression must exist since it is the root itself in the
worst case.
 -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.findCommon : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The space of multilinear maps over an algebra over `R` is a module over `R`, for the pointwise
addition and scalar multiplication.  -/
AlternatingMap.instModule : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  {S : Type u_10} →
                    [inst_5 : Semiring S] → [inst_6 : Module S N] → [SMulCommClass R S N] → Module S (M [⋀^ι]→ₗ[R] N)
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.hom_C : ∀ {S : Type v} {σ : Type u_1} [inst : CommRing S] (f : MvPolynomial σ ℤ →+* S) (n : ℤ), f (MvPolynomial.C n) = ↑n
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `meromorphicNFOn_comp_add_const_iff_meromorphicNFOn`

---

`MeromorphicNFOn` is invariant under translation.  -/
meromorphicNFOn_fun_comp_add_const_iff_meromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {U : Set 𝕜},
  MeromorphicNFOn (fun x => f (x + c)) U ↔ MeromorphicNFOn f (U + {c})
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.prod_withDensity_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {mβ : MeasurableSpace β}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {g : β → ENNReal},
  Measurable g → μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun z => g z.2
-- Init.Data.SInt.Basic
instPowInt64Nat : Pow Int64 ℕ
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `(· \ a)` is left adjoint to `(· ⊔ a)`  -/
CompletelyDistribLattice.sdiff_le_iff : ∀ {α : Type u} [self : CompletelyDistribLattice α] (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {c₁ c₂ : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)} (a : c₁ ⟶ c₂),
  (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.map a).hom = CategoryTheory.Under.Hom.right a.hom
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_alter_eq_add_one : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, k ∉ m → (f m[k]?).isSome = true → (m.alter k f).size = m.size + 1
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationBy.vars : Lean.Elab.TerminationBy → Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]
-- Init.Grind.AC
/-- Given `lhs = rhs`, and a term `s := union a lhs`, rewrite it to `s' := union a rhs`
 -/
Lean.Grind.AC.simp_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (c lhs rhs s s' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_ac_cert c lhs rhs s s' = true →
    Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx s = Lean.Grind.AC.Seq.denote ctx s'
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.isPreconnected_setOfPred_sSameSide`. -/
AffineSubspace.isPreconnected_setOf_sSameSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P),
  IsPreconnected {y | s.SSameSide x y}
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxo.Iterator.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] (it : Std.Iter α),
  Std.Rxo.Iterator.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next =>
      if next < it.internalState.upperBound then
        Std.IterStep.yield
          { internalState := { next := Std.PRange.succ? next, upperBound := it.internalState.upperBound } } next
      else Std.IterStep.done
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.congr_arg : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (φ : A →ₗc[R] B) {x y : A}, x = y → φ x = φ y
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.mk.sizeOf_spec : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} [inst_4 : SizeOf N]
  [inst_5 : SizeOf E] [inst_6 : SizeOf G] [inst_7 : SizeOf E'] (toMulEquiv : E ≃* E')
  (inl_comm : ⇑toMulEquiv ∘ ⇑S.inl = ⇑S'.inl) (rightHom_comm : ⇑S'.rightHom ∘ ⇑toMulEquiv = ⇑S.rightHom),
  sizeOf { toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm } =
    1 + sizeOf toMulEquiv + sizeOf inl_comm + sizeOf rightHom_comm
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoKernel_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] [inst_3 : CategoryTheory.Limits.HasKernel S.g],
  S.cyclesIsoKernel.hom = CategoryTheory.Limits.kernel.lift S.g S.iCycles ⋯
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.addDeclToUnfoldCore : Lean.Meta.SimpTheorems → Lean.Name → Lean.Meta.SimpTheorems
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `F ⊣ G` and a `CommShift` structure on `G`, these are the candidate
`CommShift.iso a` isomorphisms for a compatible `CommShift` structure on `F`.
 -/
CategoryTheory.Adjunction.LeftAdjointCommShift.iso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {A : Type u_3} →
                [inst_2 : AddGroup A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] →
                      (a : A) →
                        [G.CommShift A] →
                          (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.mem_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → (k ∈ t₁ ↔ k ∈ t₂)
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- The assignment `x ↦ diracProba x` is continuous `X → ProbabilityMeasure X`.  -/
MeasureTheory.continuous_diracProba : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X],
  Continuous fun x => MeasureTheory.diracProba x
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] [inst_4 : DecidablePred fun x => x ≠ 0]
  {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (f : MeasureTheory.SimpleFunc α F),
  MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x
-- Mathlib.CategoryTheory.Category.Quiv
/-- The adjunction between forming the free category on a quiver, and forgetting a category to a quiver.
 -/
CategoryTheory.Quiv.adj : CategoryTheory.Cat.free ⊣ CategoryTheory.Quiv.forget
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioo_castSucc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioo a.castSucc b.castSucc, f i = ∑ i ∈ Finset.Ioo a b, f i.castSucc
-- Mathlib.FieldTheory.CardinalEmb
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.termB : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `L` with the spectral norm is a `NormedAddCommGroup`.  -/
spectralNorm.normedAddCommGroup : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [CompleteSpace K] → NormedAddCommGroup L
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.erase : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Std.TreeSet.Raw α cmp
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.norm_eq_infDist : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} (x : M ⧸ S), ‖x‖ = Metric.infDist 1 {m | ↑m = x}
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- **Alias** of the forward direction of `Finset.inv_nonempty_iff`. -/
Finset.Nonempty.of_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α}, s⁻¹.Nonempty → s.Nonempty
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.prim_iff₂ : ∀ {f : ℕ → ℕ → ℕ}, (Nat.Primrec' fun v => f v.head v.tail.head) ↔ Primrec₂ f
-- Mathlib.RingTheory.DividedPowers.Basic
/-- Lemma towards `dpow_sum` when we only have partial information on a divided power ideal  -/
DividedPowers.dpow_sum' : ∀ {A : Type u_1} [inst : CommSemiring A] {M : Type u_2} [inst_1 : AddCommMonoid M] {I : AddSubmonoid M}
  (dpow : ℕ → M → A),
  (∀ {x : M}, x ∈ I → dpow 0 x = 1) →
    (∀ {n : ℕ} {x y : M},
        x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dpow k.1 x * dpow k.2 y) →
      (∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0) →
        ∀ {ι : Type u_3} [inst_2 : DecidableEq ι] {s : Finset ι} {x : ι → M},
          (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- If `S` is `R`-standard smooth, `Ω[S⁄R]` is a free `S`-module.  -/
Algebra.IsStandardSmooth.free_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardSmooth R S], Module.Free S Ω[S⁄R]
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (↑(m.insert k v)).isEmpty = false
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.clift_apply_mk : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : FreeAddMonoid (M ⊕ N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0)
  (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0)
  (hM :
    ∀ (x y : M),
      f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y)))
  (hN :
    ∀ (x y : N),
      f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y)))
  (w : FreeAddMonoid (M ⊕ N)), (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.mk w) = f w
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- The separable degree of a polynomial is the degree of a given separable contraction.  -/
Polynomial.HasSeparableContraction.degree : {F : Type u_1} → [inst : CommSemiring F] → {q : ℕ} → {f : Polynomial F} → Polynomial.HasSeparableContraction q f → ℕ
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed thickening `Metric.cthickening δ E` with a fixed thickening radius `δ` is
an increasing function of the subset `E`.  -/
Metric.cthickening_subset_of_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) {E₁ E₂ : Set α},
  E₁ ⊆ E₂ → Metric.cthickening δ E₁ ⊆ Metric.cthickening δ E₂
-- Mathlib.Topology.Algebra.Group.Basic
topologicalGroup_of_discreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Group H] [DiscreteTopology H], IsTopologicalGroup H
-- Lean.ProjFns
Lean.projectionFnInfoExt : Lean.MapDeclarationExtension Lean.ProjectionFunctionInfo
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.exp_lt_exp : ∀ {G : Type u_3} [inst : Preorder G] {a b : G}, WithZero.exp a < WithZero.exp b ↔ a < b
-- Mathlib.Topology.Compactness.Lindelof
/-- A closed subset of a Lindelöf set is a Lindelöf set.  -/
IsLindelof.of_isClosed_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsClosed t → t ⊆ s → IsLindelof t
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.idCompId_simplex : ∀ {X : SSet} (x : X.obj (Opposite.op { len := 0 })),
  (SSet.Edge.CompStruct.idCompId x).simplex =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X 0))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X 0)) x)
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.foldlM.match_1.splitter : {m : Type u_3 → Type u_4} →
  {s : Type u_3} →
    {α : Type u_1} →
      (motive : (s → α → m s) → s → List α → Sort u_2) →
        (x : s → α → m s) →
          (x_1 : s) →
            (x_2 : List α) →
              ((x : s → α → m s) → (s : s) → motive x s []) →
                ((f : s → α → m s) → (s : s) → (a : α) → (as : List α) → motive f s (a :: as)) → motive x x_1 x_2
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_unique : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] [inst_2 : Unique α] {f : α →₀ M}
  {g : α → M → N}, (f default = 0 → g default 0 = 1) → f.prod g = g default (f default)
-- Mathlib.Algebra.Order.Group.Abs
mabs_mabs_div_mabs_le_mabs_div : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a b : G), ||a|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.exists_isCompact_closure_measure_compl_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P] (ε : ENNReal), 0 < ε → ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε
-- Mathlib.Algebra.Group.Units.Equiv
AddUnits.addRight_symm : ∀ {M : Type u_3} [inst : AddMonoid M] (u : AddUnits M), Equiv.symm u.addRight = (-u).addRight
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjMap_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6)
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  {F₂ F₂' : CategoryTheory.Functor C₂ D₂} (τ₂ : F₂ ⟶ F₂') (F₃ : CategoryTheory.Functor C₃ D₃),
  (CategoryTheory.Functor.whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂).app F₃ =
    CategoryTheory.Functor.whiskerRight
      ((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))
            (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).map
        (((CategoryTheory.Functor.whiskeringLeft₂ E).map τ₂).app F₃))
      ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).obj F₁)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqRequestID.beq : Lean.JsonRpc.RequestID → Lean.JsonRpc.RequestID → Bool