mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Util.PPExt
Lean.PPFns.mk.injEq : ∀ (ppExprWithInfos : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos)
  (ppConstNameWithInfos : Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos)
  (ppTerm : Lean.PPContext → Lean.Term → IO Std.Format) (ppLevel : Lean.PPContext → Lean.Level → IO Std.Format)
  (ppGoal : Lean.PPContext → Lean.MVarId → IO Std.Format)
  (ppExprWithInfos_1 : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos)
  (ppConstNameWithInfos_1 : Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos)
  (ppTerm_1 : Lean.PPContext → Lean.Term → IO Std.Format) (ppLevel_1 : Lean.PPContext → Lean.Level → IO Std.Format)
  (ppGoal_1 : Lean.PPContext → Lean.MVarId → IO Std.Format),
  ({ ppExprWithInfos := ppExprWithInfos, ppConstNameWithInfos := ppConstNameWithInfos, ppTerm := ppTerm,
        ppLevel := ppLevel, ppGoal := ppGoal } =
      { ppExprWithInfos := ppExprWithInfos_1, ppConstNameWithInfos := ppConstNameWithInfos_1, ppTerm := ppTerm_1,
        ppLevel := ppLevel_1, ppGoal := ppGoal_1 }) =
    (ppExprWithInfos = ppExprWithInfos_1 ∧
      ppConstNameWithInfos = ppConstNameWithInfos_1 ∧ ppTerm = ppTerm_1 ∧ ppLevel = ppLevel_1 ∧ ppGoal = ppGoal_1)
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.vars_sub_of_disjoint : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R}
  [inst_1 : DecidableEq σ], Disjoint p.vars q.vars → (p - q).vars = p.vars ∪ q.vars
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_iff_keysArray_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α Unit cmp},
  t₁.Equiv t₂ ↔ t₁.keysArray.Perm t₂.keysArray
-- Init.Conv
/-- `any_goals tac` applies the tactic `tac` to every goal, and succeeds if at
least one application succeeds.
 -/
Lean.Parser.Tactic.Conv.anyGoals : Lean.ParserDescr
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_const_sub_iff`. -/
Wbtw.const_sub : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Wbtw R x y z → Wbtw R (v - x) (v - y) (v - z)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.val_sdiff : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L), ↑(a \ b) = ↑a \ ↑b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.fst_epi : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsSplitEpi CategoryTheory.Limits.biprod.fst
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.instMulEquivClass : ∀ {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},
  MulEquivClass (S.Equiv S') E E'
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg : ∀ {R : Type u} [inst : NonAssocRing R],
  CanLift (Set R) (Subring R) SetLike.coe fun s =>
    0 ∈ s ∧
      (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧
        1 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : R}, x ∈ s → -x ∈ s
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.coe_restrictScalars' : ∀ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [inst : Semiring A] [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module A M₁] [inst_4 : Module R M₁] [inst_5 : TopologicalSpace M₁]
  [inst_6 : AddCommMonoid M₂] [inst_7 : Module A M₂] [inst_8 : Module R M₂] [inst_9 : TopologicalSpace M₂]
  [inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A] (f : M₁ →L[A] M₂), ⇑(ContinuousLinearMap.restrictScalars R f) = ⇑f
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.map_desc_assoc : ∀ {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} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (c : CategoryTheory.Limits.Cocone F) (α : G ⟶ F) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap α)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc F c) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.desc G ((CategoryTheory.Limits.Cocone.precompose α).obj c)) h
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_ne_top : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] [Nontrivial S] (f : F), RingHom.ker f ≠ ⊤
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.vadd_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : VAdd R M] [inst_3 : ContinuousConstVAdd R M] (c : R) (f : C(α, M)) (a : α), (c +ᵥ f) a = c +ᵥ f a
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.eq_of_subset_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {C C' : Set α}, M.IsCircuit C → M.IsCircuit C' → C ⊆ C' → C = C'
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a b : E → 𝔸},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 a s x →
      DifferentiableWithinAt 𝕜 b s x →
        fderivWithin 𝕜 (a * b) s x = a x • fderivWithin 𝕜 b s x + MulOpposite.op (b x) • fderivWithin 𝕜 a s x
-- Lean.Data.Json.Elab
Lean.Json.json.quot : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionOntoL_apply_right : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) (x : ↥q), (p.projectionOntoL q h) ↑x = 0
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor],
  (CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint c t).A = c.pt
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.Realize.match_1.eq_3 : ∀ {L : FirstOrder.Language} {M : Type u_5} {α : Type u_3}
  (motive : (x : ℕ) → L.BoundedFormula α x → (α → M) → (Fin x → M) → Sort u_4) (x l : ℕ) (R : L.Relations l)
  (ts : Fin l → L.Term (α ⊕ Fin x)) (v : α → M) (xs : Fin x → M)
  (h_1 : (x : ℕ) → (_v : α → M) → (_xs : Fin x → M) → motive x FirstOrder.Language.BoundedFormula.falsum _v _xs)
  (h_2 :
    (x : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin x)) →
        (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂) v xs)
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin x)) →
          (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.rel R ts) v xs)
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → (v : α → M) → (xs : Fin x → M) → motive x (f₁.imp f₂) v xs)
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → (v : α → M) → (xs : Fin x → M) → motive x f.all v xs),
  (match x, FirstOrder.Language.BoundedFormula.rel R ts, v, xs with
    | x, FirstOrder.Language.BoundedFormula.falsum, _v, _xs => h_1 x _v _xs
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂, v, xs => h_2 x t₁ t₂ v xs
    | x, FirstOrder.Language.BoundedFormula.rel R ts, v, xs => h_3 x l R ts v xs
    | x, f₁.imp f₂, v, xs => h_4 x f₁ f₂ v xs
    | x, f.all, v, xs => h_5 x f v xs) =
    h_3 x l R ts v xs
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_mono : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I J : LieIdeal R L},
  I ≤ J → ∀ (k : ℕ), LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L k J
-- Lean.Meta.Sym.Util
/-- Quick filter for checking whether we can skip `normalizeLevels`.  -/
_private.Lean.Meta.Sym.Util.0.Lean.Meta.Sym.levelsAlreadyNormalized : Lean.Expr → Bool
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.bound_lt_top : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [h : ProbabilityTheory.IsFiniteKernel κ], κ.bound < ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.fstPiMap_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (b : J.R) {Z : C} (h : I.right b ⟶ Z),
  CategoryTheory.CategoryStruct.comp I.fstPiMap
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.fst b))
      (CategoryTheory.CategoryStruct.comp (I.fst b) h)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.copy_eq : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q), Q.copy Q' h = Q
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.multisetProd : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {ι : Type u_16} {s : Multiset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'},
  (∀ i ∈ s, f i =Θ[l] g i) →
    (fun x => (Multiset.map (fun x_1 => f x_1 x) s).prod) =Θ[l] fun x => (Multiset.map (fun x_1 => g x_1 x) s).prod
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.contains a = (m.getKey? a).isSome
-- Mathlib.Order.UpperLower.Relative
/-- A subset that is a lower set is additionally a _relative_ lower set.  -/
IsRelLowerSet.mono_isLowerSet : ∀ {α : Type u_1} {s t : Set α} {P : α → Prop} [inst : LE α],
  IsRelLowerSet t P → IsLowerSet s → s ⊆ t → IsRelLowerSet s P
-- Lean.ErrorExplanation
/-- Metadata for an error explanation.

* `summary` gives a short description of the error
* `sinceVersion` indicates the version of Lean in which an error with this error name was introduced
* `severity` is the severity of the diagnostic
* `removedVersion` indicates the version of Lean in which this error name was retired, if applicable
 -/
Lean.ErrorExplanation.Metadata : Type
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : CochainComplex.mappingCone g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).hom
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).inv h) =
    h
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.homInduction_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P : {x y : CategoryTheory.Join C D} → (x ⟶ y) → Sort u_1}
  (left : (x y : C) → (f : x ⟶ y) → P ((CategoryTheory.Join.inclLeft C D).map f))
  (right : (x y : D) → (f : x ⟶ y) → P ((CategoryTheory.Join.inclRight C D).map f))
  (edge : (c : C) → (d : D) → P (CategoryTheory.Join.edge c d)) {x y : C} (f : x ⟶ y),
  CategoryTheory.Join.homInduction left right edge ((CategoryTheory.Join.inclLeft C D).map f) = left x y f
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addEmpty.inj : ∀ {β : Type u} {α : Type v} {id : ℕ} {rupHints : Array ℕ} {id_1 : ℕ} {rupHints_1 : Array ℕ},
  Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints = Std.Tactic.BVDecide.LRAT.Action.addEmpty id_1 rupHints_1 →
    id = id_1 ∧ rupHints = rupHints_1
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.instEmptyCollection : (α : Type u) → (cmp : α → α → Ordering) → EmptyCollection (RBTree.RBSet α cmp)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_Ioo : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} [OrderClosedTopology α], MeasurableSet (Set.Ioo a b)
-- Mathlib.GroupTheory.MonoidLocalization.Away
AddSubmonoid.LocalizationMap.AwayMap.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (x : M) (N' : Type u_4) [inst_1 : AddCommMonoid N'],
  AddSubmonoid.LocalizationMap.AwayMap x N' = (AddSubmonoid.multiples x).LocalizationMap N'
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- A surjective `AddGroup` homomorphism `φ : G →+ H` with `N = ker(φ)` descends
(i.e. `lift`s) to an `AddGroup` isomorphism `G/N ≃+ H`.  -/
QuotientAddGroup.liftEquiv : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup H] →
        (N : AddSubgroup G) → [nN : N.Normal] → {φ : G →+ H} → Function.Surjective ⇑φ → N = φ.ker → G ⧸ N ≃+ H
-- Mathlib.Analysis.Convex.Radon
/-- **Helly's theorem** for sets of compact convex sets in its classical version.

If `F` is a (possibly infinite) set of more than `d + 1` compact convex sets in a vector space of
finite dimension `d`, and any `d + 1` sets from `F` intersect nontrivially,
then all sets from `F` intersect nontrivially.  -/
Convex.helly_theorem_set_compact : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] [inst_6 : TopologicalSpace E] [T2Space E]
  {F : Set (Set E)},
  ↑(Module.finrank 𝕜 E) + 1 ≤ F.encard →
    (∀ X ∈ F, Convex 𝕜 X) →
      (∀ X ∈ F, IsCompact X) →
        (∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = Module.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty) → (⋂₀ F).Nonempty
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.noEdge_le_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α}, Graph.noEdge X β ≤ G ↔ X ⊆ G.vertexSet
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_zero_one : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : Zero ι] [inst_2 : GradedMonoid.GOne A]
  [inst_3 : (i : ι) → AddCommMonoid (A i)], (DirectSum.of A 0) 1 = 1
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctorPreCore B C) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
  self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.Topology.EMetricSpace.Basic
/-- For a set `s` in a pseudo emetric space, if for every `ε > 0` there exists a countable
set that is `ε`-dense in `s`, then there exists a countable subset `t ⊆ s` that is dense in `s`.  -/
EMetric.subset_countable_closure_of_almost_dense_set : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (s : Set α),
  (∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, Metric.closedEBall x ε) → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.instReprStartsWithResult : Repr Lean.Grind.AC.StartsWithResult✝
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty_diff_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂
-- Mathlib.Algebra.GroupWithZero.Invertible
div_self_of_invertible : ∀ {α : Type u} [inst : GroupWithZero α] (a : α) [Invertible a], a / a = 1
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- Family of elements over a covering in `K`. Note that it is not necessarily compatible.  -/
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : CategoryTheory.Precoverage C} →
      {ι : C → Type w} →
        {X : C} →
          {R : CategoryTheory.Presieve X} →
            R ∈ K.coverings X →
              (⦃W : C⦄ → (r : W ⟶ X) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W) →
                CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι X
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.multisetSum_zero : ∀ {n : ℕ} {s : Multiset ℕ}, (∀ x ∈ s, x ≡ 0 [MOD n]) → s.sum ≡ 0 [MOD n]
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- The conditional cdf tends to 1 at +∞ for all `a : α`.  -/
ProbabilityTheory.tendsto_condCDF_atTop : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α),
  Filter.Tendsto (↑(ProbabilityTheory.condCDF ρ a)) Filter.atTop (nhds 1)
-- Std.Time.Date.Unit.Weekday
/-- Converts a `Weekday` to a `Ordinal`.
 -/
Std.Time.Weekday.toOrdinal : Std.Time.Weekday → Std.Time.Weekday.Ordinal
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousOn.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {s t : Set α},
  SemicontinuousOn r s → t ⊆ s → SemicontinuousOn r t
-- Mathlib.CategoryTheory.ConnectedComponents
/-- Each connected component of the category is nonempty.  -/
CategoryTheory.instNonemptyComponent : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] (j : CategoryTheory.ConnectedComponents J),
  Nonempty j.Component
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_eq_zero_of_notMem_vars : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {i : σ} {f : MvPolynomial σ R},
  i ∉ f.vars → (MvPolynomial.pderiv i) f = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_filter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool}, (Std.DTreeMap.filter f t).size ≤ t.size
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.isEmpty_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.Equiv t₂ → t₁.isEmpty = t₂.isEmpty
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Restrict a simple function `f : α →ₛ β` to a set `s`. If `s` is measurable,
then `f.restrict s a = if a ∈ s then f a else 0`, otherwise `f.restrict s = const α 0`.  -/
MeasureTheory.SimpleFunc.restrict : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → [Zero β] → MeasureTheory.SimpleFunc α β → Set α → MeasureTheory.SimpleFunc α β
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Auxiliary method for adding a local simp theorem to a `SimpTheorems` datastructure.  -/
Lean.Meta.SimpTheorems.add : Lean.Meta.SimpTheorems →
  Lean.Meta.Origin →
    Array Lean.Name →
      Lean.Expr →
        optParam Bool false →
          optParam Bool true →
            optParam ℕ 1000 →
              optParam Lean.Meta.ConfigWithKey Lean.Meta.simpGlobalConfig → Lean.MetaM Lean.Meta.SimpTheorems
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.toList_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {l : List ((_ : α) × β)},
  (List.map (fun p => (p.fst, f p.fst p.snd)) l).Perm
    (List.map (fun p => (p.fst, p.snd)) (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l))
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.id_whisker_left : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A morphism `(⨿ (i : X.I), X.obj i) ⟶ (⨿ (j : Y.I), Y.obj i)` is given by first a function
on the indexing sets `f : X.I → Y.I`, and then for each `i : X.I` a morphism
`X.obj i ⟶ Y.obj (f i)`.  -/
CategoryTheory.Limits.FormalCoproduct.Hom : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Limits.FormalCoproduct C → CategoryTheory.Limits.FormalCoproduct C → Type (max v w)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_equiv : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : ι ≃ ι') {f : ι' → M} {s : Set ι}, LinearIndepOn R (f ∘ ⇑e) s ↔ LinearIndepOn R f (⇑e '' s)
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanlM_loop_eq_scanlMFast_loop : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] {f : β → α → m β} {init : β} {as : Array α}
  {h_size : Array.SizeFitsUSize✝ as} {start stop : ℕ} {h_start : start ≤ as.size} {h_stop : stop ≤ as.size}
  {acc : Array β},
  Array.scanlM.loop f init as start stop h_stop acc =
    Array.scanlMFast.loop✝ f init as (USize.ofNat start) (USize.ofNat stop) ⋯ acc
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousAt.const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {b : β}, ContinuousAt g b → ∀ (c : M), ContinuousAt (c • g) b
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Given a map `r : I₁ × I₂ × I₃ → J`, a `BifunctorComp₂₃IndexData r` consists of the data
of a type `I₂₃`, maps `p : I₂ × I₃ → I₂₃` and `q : I₁ × I₂₃ → J`, such that `r` is obtained
by composition of `p` and `q`.  -/
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} → {J : Type u_10} → (I₁ × I₂ × I₃ → J) → Type (max (max (max (max u_10 (u_11 + 1)) u_7) u_8) u_9)
-- Mathlib.Data.EReal.Inv
EReal.inv_neg_of_neg_ne_bot : ∀ {a : EReal}, a < 0 → a ≠ ⊥ → a⁻¹ < 0
-- Mathlib.Order.CountableSupClosed
countableInfClosed_preimage_toDual : ∀ {α : Type u_2} [inst : LE α] {s : Set αᵒᵈ}, CountableInfClosed (⇑OrderDual.toDual ⁻¹' s) ↔ CountableSupClosed s
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_reflectionPerm_self_left : ∀ {ι : 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 : ι),
  P.pairing ((P.reflectionPerm i) i) j = -P.pairing i j
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.forget₂_faithful : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {D : Type u_3} [inst_3 : CategoryTheory.Category.{v_2, u_3} D]
  {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)}
  [inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : CategoryTheory.HasForget₂ C D], (CategoryTheory.forget₂ C D).Faithful