mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- Given additive functors that are related by an isomorphism `F ⋙ G ≅ H`, this is
the corresponding isomorphism on the corresponding functor between
the bounded below homotopy categories.  -/
CategoryTheory.Functor.mapHomotopyCategoryPlusCompIso : {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] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            {E : Type u_4} →
              [inst_4 : CategoryTheory.Category.{v_4, u_4} E] →
                [inst_5 : CategoryTheory.Preadditive E] →
                  {F : CategoryTheory.Functor C D} →
                    {G : CategoryTheory.Functor D E} →
                      {H : CategoryTheory.Functor C E} →
                        (F.comp G ≅ H) →
                          [inst_6 : F.Additive] →
                            [inst_7 : G.Additive] →
                              [inst_8 : H.Additive] →
                                F.mapHomotopyCategoryPlus.comp G.mapHomotopyCategoryPlus ≅ H.mapHomotopyCategoryPlus
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.equivFunOnFintype_symm_single : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι)
  (m : β i), DFinsupp.equivFunOnFintype.symm (Pi.single i m) = fun₀ | i => m
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.revMatchAt?_eq_revMatchAt?_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.revMatchAt? c pos = String.Slice.Pattern.Model.revMatchAt? (fun x => x == c) pos
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : U ≤ U'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V e) (Y.homOfLE i) =
    AlgebraicGeometry.Scheme.Hom.resLE f U' V ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g f)
      (CategoryTheory.Limits.pushoutSymmetry f g).inv =
    CategoryTheory.Limits.pushout.inr f g
-- Init.Data.Range.Polymorphic.RangeIterator
/-- The pure function mapping a range iterator of type `IterM` to the next step of the iterator.

This function is prefixed with `Monadic` in order to disambiguate it from the version for
iterators of type `Iter`.
 -/
Std.Rxc.Iterator.Monadic.step : {α : Type u} →
  [Std.PRange.UpwardEnumerable α] → [inst : LE α] → [DecidableLE α] → Std.IterM Id α → Std.IterStep (Std.IterM Id α) α
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)) {s : Set (((i : ι) → Em i) × G)},
  CPolynomialOn 𝕜 (fun p => (f p.1) p.2) s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
CliffordAlgebra.isUnit_of_isUnit_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) [Invertible 2] {m : M}, IsUnit ((CliffordAlgebra.ι Q) m) → IsUnit (Q m)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
Equiv.refl.eq_1 : ∀ (α : Sort u_1), Equiv.refl α = { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯ }
-- Lean.Parser.Term
/-- `binop_lazy%` is similar to `binop% f a b`, but it wraps `b` as a function from `Unit`.  -/
Lean.Parser.Term.binop_lazy : Lean.Parser.Parser
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- The image of the filter `atBot` on `Iio a` under the coercion equals `atBot`.  -/
Filter.map_val_Iio_atBot : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] [NoMinOrder α] (a : α),
  Filter.map Subtype.val Filter.atBot = Filter.atBot
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.liftOfRightInverse_comp : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g // f.ker ≤ g.ker }),
  ((f.liftOfRightInverse f_inv hf) g).comp f = ↑g
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.insertManyIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (l : ρ),
  m.insertManyIfNew l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have r := ⟨(↑r).insertIfNew a b, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insertIfNew a b)) →
              P m → P m' } :=
        __s
      pure r).run
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.createImportedEnvironmentSeq : {α : Type} →
  Lean.Core.Context →
    Lean.NameGenerator →
      Lean.Environment →
        (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
          ℕ → ℕ → BaseIO (Lean.Meta.LazyDiscrTree.InitResults α)
-- Mathlib.Order.Heyting.Basic
codisjoint_hnot_hnot_left_iff : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, Codisjoint (￢￢a) b ↔ Codisjoint a b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- the pullback  -/
CategoryTheory.Functor.PullbackObjObj.pt : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {X₁ Y₁ : C₁} → {f₁ : X₁ ⟶ Y₁} → {X₃ Y₃ : C₃} → {f₃ : X₃ ⟶ Y₃} → G.PullbackObjObj f₁ f₃ → C₂
-- Mathlib.CategoryTheory.Adhesive.Basic
/-- A pushout is van Kampen if and only if whenever it forms the bottom face of a commutative
"half-cube", the front faces are pullbacks if and only if there exist back faces which are pullbacks
and a top face which is a pushout.  -/
CategoryTheory.IsPushout.isVanKampen_iff' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  {H : CategoryTheory.IsPushout f g h i},
  H.IsVanKampen ↔
    ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
      CategoryTheory.CommSq h' αX αZ h →
        CategoryTheory.CommSq i' αY αZ i →
          ∀ [CategoryTheory.Limits.HasPullback αX f],
            CategoryTheory.IsPullback h' αX αZ h ∧ CategoryTheory.IsPullback i' αY αZ i ↔
              ∃ W' f' g' αW,
                CategoryTheory.IsPullback f' αW αX f ∧
                  CategoryTheory.IsPullback g' αW αY g ∧ CategoryTheory.IsPushout f' g' h' i'
-- Mathlib.Algebra.Category.Ring.Constructions
Algebra.TensorProduct.liftEquiv.congr_simp : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C],
  Algebra.TensorProduct.liftEquiv = Algebra.TensorProduct.liftEquiv
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from below: the measure of the union of a sequence of
(not necessarily measurable) sets is the supremum of the measures of the partial unions.  -/
MeasureTheory.measure_iUnion_eq_iSup_accumulate : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [IsDirectedOrder ι] [Filter.atTop.IsCountablyGenerated] {f : ι → Set α}, μ (⋃ i, f i) = ⨆ i, μ (Set.accumulate f i)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivWithinAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (s : Set M) (x : M),
  HasMFDerivAt[s] id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
-- Init.Data.String.PosRaw
String.instHAddRaw : HAdd String String.Pos.Raw String.Pos.Raw
-- Aesop.RuleSet
Aesop.BaseRuleSet.erase : Aesop.BaseRuleSet → Aesop.RuleFilter → Aesop.BaseRuleSet × Bool
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.union_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ ∪ t₂).Equiv (t₁ ∪ t₃)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_iff_upperBound? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp],
  x ∈ t ↔ ∃ y, t.upperBound? x = some y ∧ cmp x y = Ordering.eq
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The function `exp(x)/x^n` tends to `+∞` at `+∞`, for any natural number `n`  -/
Real.tendsto_exp_div_pow_atTop : ∀ (n : ℕ), Filter.Tendsto (fun x => Real.exp x / x ^ n) Filter.atTop Filter.atTop
-- Mathlib.Algebra.Group.Torsion
self_ne_inv : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {a : G}, a ≠ a⁻¹ ↔ a ≠ 1
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csInf_neg : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M]
  {s : Set M}, s.Nonempty → BddAbove s → sInf (-s) = -sSup s
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p q : MvPolynomial σ R) (n : σ →₀ ℕ),
  MvPolynomial.coeff n (p * q) =
    ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, MvPolynomial.coeff x.1 p * MvPolynomial.coeff x.2 q
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.stalkwise : ∀ {P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    AlgebraicGeometry.HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
      fun {x S} {x_1} {x_2} φ =>
      ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)
-- Mathlib.Algebra.Ring.Defs
mul_one_add : ∀ {α : Type u} [inst : Add α] [inst_1 : MulOneClass α] [LeftDistribClass α] (a b : α), a * (1 + b) = a + a * b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?!_snd : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} {v : β k}, (t.getThenInsertIfNew?! k v).2 = Std.DTreeMap.Internal.Impl.insertIfNew! k v t
-- Aesop.Forward.Match
/-- Add a hyp or pattern substitution to the match. `subst` is the substitution
that results from matching a hypothesis against slot `m.level + 1`, or from the
pattern. `isPatSubst` is `true` if the substitution resulted from a pattern
substitution. `forwardDeps` are the forward dependencies of slot
`m.level + 1`.  -/
Aesop.Match.addHypOrPatSubst : Aesop.Substitution → Bool → Array Aesop.PremiseIndex → Aesop.Match → Aesop.Match
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.cast.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 : Std.Sat.AIG α}
  (s s_1 : aig1.BinaryRefVec len), s = s_1 → ∀ (h : aig1.decls.size ≤ aig2.decls.size), s.cast h = s_1.cast h
-- Mathlib.Order.WithBot
WithBot.instPartialOrder.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α],
  WithBot.instPartialOrder = { toPreorder := WithBot.instPreorder, le_antisymm := ⋯ }
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Pass.mk : Mathlib.TacticAnalysis.Config → Option (Lean.Option Bool) → Mathlib.TacticAnalysis.Pass
-- Mathlib.Topology.MetricSpace.Thickening
Metric.ediam_cthickening_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} (ε : NNReal),
  Metric.ediam (Metric.cthickening (↑ε) s) ≤ Metric.ediam s + 2 * ↑ε
-- Mathlib.Data.Bool.Basic
Bool.left_le_or : ∀ (x y : Bool), x ≤ (x || y)
-- Mathlib.RingTheory.Smooth.IntegralClosure
/-- Let `S` be an `R`-algebra and `f : S[X]` be a monic polynomial with `R`-integral coefficients.
Suppose `y` in `B = S[X]/f` is `R`-integral, then `f' * y` is the image of some `g : S[X]` with
`R`-integral coefficients.  -/
exists_derivative_mul_eq_and_isIntegral_coeff : ∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {φ : Polynomial S →ₐ[R] B},
  Function.Surjective ⇑φ →
    ∀ {f : Polynomial S},
      f.Monic →
        (∀ (i : ℕ), IsIntegral R (f.coeff i)) →
          RingHom.ker φ.toRingHom = Ideal.span {f} →
            ∀ {y : B}, IsIntegral R y → ∃ g, φ (Polynomial.derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)
-- Mathlib.Topology.Algebra.Monoid.Defs
Continuous.const_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M}, Continuous f → ∀ (b : M), Continuous fun x => b + f x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.tensorObj_obj : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F₁ F₂ : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj F₁ F₂).obj j =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F₁.obj j) (F₂.obj j)
-- Mathlib.Computability.Partrec
Computable.vector_cons : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Computable₂ List.Vector.cons
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a subtraction commutative monoid if `β`
is a subtraction commutative monoid.  -/
FunLike.subtractionCommMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : Neg F] →
                [inst_5 : Sub F] →
                  [inst_6 : SMul ℤ F] →
                    [inst_7 : SubtractionCommMonoid β] →
                      [IsZeroApply F α β] →
                        [IsAddApply F α β] →
                          [IsNegApply F α β] →
                            [IsSubApply F α β] → [IsSMulApply ℕ F α β] → [IsSMulApply ℤ F α β] → SubtractionCommMonoid F
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- A subgroup is *regular at ∞* if its periods and strict periods coincide.  -/
Subgroup.IsRegularAtInfty : {R : Type u_1} → [inst : Ring R] → Subgroup (GL (Fin 2) R) → Prop
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.triangle_aux₁_assoc : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.LocalizedMonoidal L W ε} (i₁ : X₁ ≅ Y₁) (i₂ : X₂ ≅ Y₂) (i₃ : X₃ ≅ Y₃)
  {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom i₁.hom i₂.hom)
        i₃.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom i₁.inv
            (CategoryTheory.MonoidalCategoryStruct.tensorHom i₂.inv i₃.inv))
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom h
-- Mathlib.Algebra.Module.PUnit
PUnit.instVAddCommClass : ∀ {R : Type u_1} {S : Type u_2}, VAddCommClass R S PUnit.{u_3 + 1}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproduct.bicone_fst : ∀ {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.Limits.BinaryBiproduct.bicone X Y).fst = CategoryTheory.Limits.biprod.fst
-- Mathlib.Analysis.Normed.Lp.Finsupp
/-- The L^1 metric on `ι`-many copies of a metric space `X`  -/
Finsupp.instPseudoMetricSpaceWithLpOfNNReal : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : Zero X] → {p : NNReal} → [Fact (1 ≤ p)] → [PseudoMetricSpace X] → PseudoMetricSpace (WithLp (↑p) (ι →₀ X))
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.laplacian_apply_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℂ F]
  (f : TemperedDistribution E F) (u : SchwartzMap E ℂ), (Laplacian.laplacian f) u = f (Laplacian.laplacian u)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.centralizer_univ : ∀ {R : Type u_1} [inst : NonUnitalSemiring R], NonUnitalSubsemiring.centralizer Set.univ = NonUnitalSubsemiring.center R
-- Mathlib.Analysis.Calculus.FDeriv.Defs
fderivWithin_def : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_6} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (s : Set E) (x : E),
  fderivWithin 𝕜 f s x =
    if HasFDerivWithinAt f 0 s x then 0 else if h : DifferentiableWithinAt 𝕜 f s x then Classical.choose h else 0
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
/-- The vertices of `s` whose density in `t` is `ε` less than expected.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.badVertices : {α : Type u_1} → (G : SimpleGraph α) → [DecidableRel G.Adj] → ℝ → Finset α → Finset α → Finset α
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.mem_subgroupOfPrimitiveMapToOne_iff : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) [inst_1 : NeZero n] [Nontrivial R]
  (p : ℕ) [hp : Fact (Nat.Prime p)],
  χ ∈ DirichletCharacter.subgroupOfPrimitiveMapToOne R n p ↔ χ.primitiveCharacter ↑p = 1
-- Mathlib.Algebra.Ring.GeomSum
Nat.sub_one_dvd_pow_sub_one : ∀ (x n : ℕ), x - 1 ∣ x ^ n - 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.cpop.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVUnOp.cpop = 1
-- Mathlib.Data.Finset.Insert
Finset.Nonempty.exists_cons_eq : ∀ {α : Type u_3} {s : Finset α}, s.Nonempty → ∃ t a, ∃ (ha : a ∉ t), Finset.cons a t ha = s
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.zero_le_toSignedMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ],
  0 ≤ μ.toSignedMeasure
-- Init.Data.Array.Lemmas
Array.size_pos_of_mem : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs → 0 < xs.size
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_zero : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
-- Init.Data.Rat.Lemmas
Rat.mk_eq_divInt : ∀ {num : ℤ} {den : ℕ} {nz : den ≠ 0} {c : num.natAbs.Coprime den},
  { num := num, den := den, den_nz := nz, reduced := c } = Rat.divInt num ↑den
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls.match_1.splitter : (motive : Lean.Expr → Sort u_1) →
  (origParam : Lean.Expr) →
    ((origFVar : Lean.FVarId) → motive (Lean.Expr.fvar origFVar)) →
      ((x : Lean.Expr) → (∀ (origFVar : Lean.FVarId), x = Lean.Expr.fvar origFVar → False) → motive x) →
        motive origParam
-- Init.Data.SInt.Lemmas
Int32.toInt.inj : ∀ {x y : Int32}, x.toInt = y.toInt → x = y
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.aux_inj_roots_of_min_poly : ∀ (F : Type u_3) (E : Type u_4) (K : Type u_5) [inst : Field F] [inst_1 : Ring E] [inst_2 : CommRing K]
  [inst_3 : IsDomain K] [inst_4 : Algebra F E] [inst_5 : Algebra F K] [inst_6 : FiniteDimensional F E],
  Function.Injective (minpoly.rootsOfMinPolyPiType F E K)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rco.length_iter : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α] {r : Std.Rco α},
  r.iter.length = r.size
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.iUnion_connectedComponentSupp : ∀ {V : Type u} (G : SimpleGraph V), ⋃ c, c.supp = Set.univ
-- Mathlib.Topology.Irreducible
/-- A maximal irreducible set that contains a given point.  -/
irreducibleComponent : {X : Type u_1} → [TopologicalSpace X] → X → Set X
-- Std.Data.DHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise panics.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DHashMap.getEntry! : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [Inhabited ((a : α) × β a)] → Std.DHashMap α β → α → (a : α) × β a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a ha acc => f a ⋯ acc
-- Std.Data.ExtDHashMap.Lemmas
_private.Std.Data.ExtDHashMap.Lemmas.0.Std.ExtDHashMap.union_mk : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m₁ m₂ : Std.DHashMap α β}, (Std.ExtDHashMap.mk m₁).union (Std.ExtDHashMap.mk m₂) = Std.ExtDHashMap.mk (m₁ ∪ m₂)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
/-- The ascending chain condition on principal ideals in a domain is sufficient to prove that
the domain is `WfDvdMonoid`.  -/
WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt : ∀ {α : Type u_1} [inst : CommSemiring α] [IsDomain α],
  ({I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2) → WfDvdMonoid α
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressReport.mk.inj : ∀ {kind : String} {message? : Option String} {cancellable : Bool} {percentage? : Option ℕ} {kind_1 : String}
  {message?_1 : Option String} {cancellable_1 : Bool} {percentage?_1 : Option ℕ},
  { kind := kind, message? := message?, cancellable := cancellable, percentage? := percentage? } =
      { kind := kind_1, message? := message?_1, cancellable := cancellable_1, percentage? := percentage?_1 } →
    kind = kind_1 ∧ message? = message?_1 ∧ cancellable = cancellable_1 ∧ percentage? = percentage?_1