mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Gcd
Nat.gcd_right_eq_iff : ∀ {m n n' : ℕ}, m.gcd n = m.gcd n' ↔ ∀ (k : ℕ), k ∣ m → (k ∣ n ↔ k ∣ n')
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (G : CategoryTheory.StrictlyUnitaryPseudofunctor C D) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  ((F.comp G).mapComp f g).inv =
    CategoryTheory.CategoryStruct.comp (G.mapComp (F.map f) (F.map g)).inv (G.map₂ (F.mapComp f g).inv)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
SSet.Homotopy.h₀ : ∀ {X Y : SSet} {f g : X ⟶ Y} (H : SSet.Homotopy f g), CategoryTheory.CategoryStruct.comp SSet.ι₀ H.h = f
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.to_rightInvOn : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ {g : β → α} {t : Set β}, Set.RightInvOn g f t → LipschitzWith K (t.domRestrict g)
-- Init.Omega.Constraint
/-- Check if a constraint is unsatisfiable.  -/
Lean.Omega.Constraint.isImpossible : Lean.Omega.Constraint → Bool
-- Mathlib.Logic.Relator
/-- The binary relations `R : α → β → Prop` and `S : γ → δ → Prop` induce a binary
relation on functions `LiftFun : (α → γ) → (β → δ) → Prop`.  -/
Relator.LiftFun : {α : Sort u₁} →
  {β : Sort u₂} → {γ : Sort v₁} → {δ : Sort v₂} → (α → β → Prop) → (γ → δ → Prop) → (α → γ) → (β → δ) → Prop
-- Std.Data.ExtDTreeMap.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.
If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`,
then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.ExtDTreeMap.containsThenInsertIfNew : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → β a → Bool × Std.ExtDTreeMap α β cmp
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans X Y)
  (θ : CategoryTheory.Lax.StrongTrans Y Z) {a b : B} (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.comp η θ).naturality f =
    CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f) ≪≫
      CategoryTheory.Bicategory.whiskerLeftIso (η.app a) (θ.naturality f) ≪≫
        (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).symm ≪≫
          CategoryTheory.Bicategory.whiskerRightIso (η.naturality f) (θ.app b) ≪≫
            CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.asIdeal_le_asIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : PrimeSpectrum R), x.asIdeal ≤ y.asIdeal ↔ x ≤ y
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Any two types with unique elements are measurably equivalent.  -/
MeasurableEquiv.ofUniqueOfUnique : (α : Type u_6) →
  (β : Type u_7) → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → [Unique α] → [Unique β] → α ≃ᵐ β
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.pap.injEq : ∀ (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg) (c_1 : Lean.IR.FunId) (ys_1 : Array Lean.IR.Arg),
  (Lean.IR.Expr.pap c ys = Lean.IR.Expr.pap c_1 ys_1) = (c = c_1 ∧ ys = ys_1)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDocInfo.inj : ∀ {i i_1 : Lean.Elab.DocInfo}, Lean.Elab.Info.ofDocInfo i = Lean.Elab.Info.ofDocInfo i_1 → i = i_1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology C n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.map (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.resMap g φ) ψ) n) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.map f φ n)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.map g ψ n) h)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.subst_into_smul : ∀ {α : Type u_1} [inst : AddCommMonoid α] (l : ℕ) (r : α) (tl : ℕ) (tr t : α),
  l = tl → r = tr → Mathlib.Tactic.Abel.smul tl tr = t → Mathlib.Tactic.Abel.smul l r = t
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat) (f : ↑(X.presheaf.obj (Opposite.op ⊤))),
  (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) f ≠ 0 ↔ x ∈ X.toRingedSpace.basicOpen f
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_disjUnion : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (f : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) {π₁ π₂ : BoxIntegral.TaggedPrepartition I}
  (h : Disjoint π₁.iUnion π₂.iUnion),
  BoxIntegral.integralSum f vol (π₁.disjUnion π₂ h) =
    BoxIntegral.integralSum f vol π₁ + BoxIntegral.integralSum f vol π₂
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_div_cancel₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b : G₀}, a ≠ 0 → a / (a / b) = b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)
-- Mathlib.CategoryTheory.Endomorphism
/-- Endomorphisms of an object in a category. Arguments order in multiplication agrees with
`Function.comp`, not with `CategoryTheory.CategoryStruct.comp`.  -/
CategoryTheory.End : {C : Type u} → [CategoryTheory.CategoryStruct.{v, u} C] → C → Type v
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt.eq_1 : ∀ (p : ℕ) (z : ℤ), padicValInt p z = padicValNat p z.natAbs
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instNonUnitalRing : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] → [inst_1 : Monoid G] → [MulSemiringAction G k] → NonUnitalRing (SkewMonoidAlgebra k G)
-- Mathlib.Topology.UniformSpace.Basic
/-- **Alias** of the reverse direction of `uniformContinuousOn_iff_restrict`. -/
UniformContinuousOn.of_restrict : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  UniformContinuous (s.domRestrict f) → UniformContinuousOn f s
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- Auxiliary lemma for the degenerate case of `dist_orthogonalProjection_eq_iff_angle_eq` where
`p` lies in `s₁`.  -/
_private.Mathlib.Geometry.Euclidean.Angle.Bisector.0.EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq_aux₁ : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} [inst_4 : s₁.direction.HasOrthogonalProjection]
  [inst_5 : s₂.direction.HasOrthogonalProjection] (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂),
  p ∈ s₁ →
    (dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) = dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p) ↔
      EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₁) p) =
        EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₂) p))
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_T_eval_one : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ),
  ↑(∏ l ∈ Finset.range k, (2 * l + 1)) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n)) =
    ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2))
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.zero_nsmul : ∀ {α : Type u_1} {t : FirstOrder.Language.presburger.Term α}, 0 • t = 0
-- Init.Data.List.Sort.Lemmas
List.zipIdxLE_trans : ∀ {α : Type u_1} {le : α → α → Bool},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    ∀ (a b c : α × ℕ), List.zipIdxLE le a b = true → List.zipIdxLE le b c = true → List.zipIdxLE le a c = true
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.intCast_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddGroupWithOne (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)]
  [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (n : ℤ) (i : ι), ↑n = ⟦⟨i, ↑n⟩⟧
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.rightFun_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (p : F × G) in nhds (φ.prodFun φ.pt), φ.rightFun (φ.implicitFunction p.1 p.2) = p.2
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : A.IsTriangulated],
  (A.triangulatedLocalizerMorphism B).functor.IsTriangulated
-- Init.Grind.Ring.Basic
Lean.Grind.CommSemiring.mk : {α : Type u} → [toSemiring : Lean.Grind.Semiring α] → (∀ (a b : α), a * b = b * a) → Lean.Grind.CommSemiring α
-- Mathlib.NumberTheory.MahlerMeasure
_private.Mathlib.NumberTheory.MahlerMeasure.0.Polynomial.boxPoly.eq_1 : ∀ (n : ℕ) (B₁ B₂ : Fin (n + 1) → ℝ),
  Polynomial.boxPoly n B₁ B₂ = {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), B₁ i ≤ ↑(p.coeff ↑i) ∧ ↑(p.coeff ↑i) ≤ B₂ i}
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFractionRel.symm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {z₁ z₂ : W.RightFraction X Y},
  CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂ → CategoryTheory.MorphismProperty.RightFractionRel z₂ z₁
-- Mathlib.Data.Finset.Option
Finset.eraseNone_insertNone : ∀ {α : Type u_1} (s : Finset α), Finset.eraseNone (Finset.insertNone s) = s
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.support_mul_subset : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R}, (x * y).support ⊆ x.support + y.support
-- Mathlib.Data.Multiset.AddSub
Multiset.instAdd : {α : Type u_1} → Add (Multiset α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.isEquivalent_sin : Asymptotics.IsEquivalent (nhds 0) Real.sin id
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.comap` as a `MonoidHom`.  -/
LocallyConstant.comapMonoidHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} → [inst_2 : MulOneClass Z] → C(X, Y) → LocallyConstant Y Z →* LocallyConstant X Z
-- Mathlib.Combinatorics.SetFamily.LYM
/-- The downward **local LYM inequality**. `𝒜` takes up less of `α^(r)` (the finsets of card `r`)
than `∂𝒜` takes up of `α^(r - 1)`.  -/
Finset.card_div_choose_le_card_shadow_div_choose : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] [inst_4 : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
  r ≠ 0 → Set.Sized r ↑𝒜 → ↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑𝒜.shadow.card / ↑((Fintype.card α).choose (r - 1))
-- Lean.Environment
Lean.EnvExtensionState : Type
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roo_eq_add : ∀ {m n : ℤ} {i : ℕ}, i < (n - (m + 1)).toNat → (m<...n).toArray[i]! = m + 1 + ↑i
-- Mathlib.Computability.DFA
DFA.acceptsFrom_union : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2) (s1 : σ1) (s2 : σ2),
  (M1.union M2).acceptsFrom (s1, s2) = M1.acceptsFrom s1 + M2.acceptsFrom s2
-- Init.Data.Order.Classes
Std.IsLinearOrder.mk : ∀ {α : Type u} [inst : LE α] [toIsPartialOrder : Std.IsPartialOrder α],
  (∀ (a b : α), a ≤ b ∨ b ≤ a) → Std.IsLinearOrder α
-- Mathlib.Tactic.NormNum.Core
/-- Run each registered `norm_num` extension on an expression, returning a `NormNum.Result`.  -/
Mathlib.Meta.NormNum.derive : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → optParam Bool false → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keys_filter!_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : α → Bool},
  t.WF → (Std.DTreeMap.Internal.Impl.filter! (fun k x => f k) t).keys = List.filter f t.keys
-- Mathlib.NumberTheory.LucasLehmer
mersenne_mod_eight : ∀ {n : ℕ}, 3 ≤ n → mersenne n % 8 = 7
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.equivOfUnique_symm_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → AddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)]
  [inst_3 : (i : ι) → TopologicalSpace (β i)] [inst_4 : Unique ι] (a : β default),
  (PiLp.equivOfUnique p 𝕜 β).symm a = WithLp.toLp p (uniqueElim a)
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.groupoidHasInvolutiveReverse : {C : Type u} → [inst : CategoryTheory.Groupoid C] → Quiver.HasInvolutiveReverse C
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instSubsingletonHomMkOfNatNat : ∀ (Δ : SimplexCategory), Subsingleton (Δ ⟶ { len := 0 })
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsuppIso_symm_apply : ∀ (R : Type u) [inst : Semiring R] (toFinsupp : AddMonoidAlgebra R ℕ),
  (Polynomial.toFinsuppIso R).symm toFinsupp = { toFinsupp := toFinsupp }
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves binary biproducts of `X` and `Y` if `F` maps every bilimit bicone over
`X` and `Y` to a bilimit bicone over `F.obj X` and `F.obj Y`.  -/
CategoryTheory.Limits.PreservesBinaryBiproduct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            C → C → (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.EquivalenceJ.inverse_map : ∀ {C₁ : Type u₁} {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₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) {f₁ f₂ : w.CostructuredArrowDownwards g} (φ : f₁ ⟶ f₂),
  (CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).map φ =
    CategoryTheory.StructuredArrow.homMk
      (CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right φ.left) ⋯) ⋯
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso X i).hom.left = ⋯.isoPushout.inv
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- A functorial version of `SimplicialObject.Augmented.rightOp`.  -/
CategoryTheory.simplicialToCosimplicialAugmented : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ
      (CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ)
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- The `Submonoid` generated by a set.  -/
Submonoid.closure : {M : Type u_1} → [inst : MulOneClass M] → Set M → Submonoid M
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.T_mul_apply_one : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), ↑(ModularGroup.T * g) 1 = ↑g 1
-- Std.Data.TreeMap.Basic
Std.TreeMap.instInhabited : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Inhabited (Std.TreeMap α β cmp)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_finprod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {f : ι → M → G},
  (∀ (i : ι), ContMDiff I' I n (f i)) →
    (LocallyFinite fun i => Function.mulSupport (f i)) → ContMDiff I' I n fun x => ∏ᶠ (i : ι), f i x
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The forgetful functor from pre-`1`-hypercovers to pre-`0`-hypercovers.  -/
CategoryTheory.PreOneHypercover.oneToZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.Functor (CategoryTheory.PreOneHypercover S) (CategoryTheory.PreZeroHypercover S)
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.leftInverse_l_u : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisInsertion l u), Function.LeftInverse l u
-- Mathlib.Analysis.Convex.Strict
StrictConvex.openSegment_subset : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : SMul 𝕜 E] {s : Set E} {x y : E},
  StrictConvex 𝕜 s → x ∈ s → y ∈ s → x ≠ y → openSegment 𝕜 x y ⊆ interior s
-- Mathlib.Topology.Sets.Opens
/-- The underlying set of a bundled `TopologicalSpace.Opens` object.  -/
TopologicalSpace.Opens.carrier : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.Opens α → Set α
-- Mathlib.Data.Finset.Basic
Finset.erase_union_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), a ∈ s → s.erase a ∪ {a} = s
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.balance'_aux : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3 →
        2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3 → Ordnode.Valid' o₁ (l.balance' x r) o₂
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_right_comm : ∀ (x y z : ℕ), x ^^^ y ^^^ z = x ^^^ z ^^^ y
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.ciInf_le_ciSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrder α] [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x1 ≥ x2) f →
    BddBelow (Set.range f) → Directed (fun x1 x2 => x1 ≤ x2) f → BddAbove (Set.range f) → ⨅ i, f i ≤ ⨆ i, f i
-- Lean.Data.Json.Basic
Lean.Json.bool.injEq : ∀ (b b_1 : Bool), (Lean.Json.bool b = Lean.Json.bool b_1) = (b = b_1)
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
Lean.Elab.Structural.instInhabitedRecArgInfo : Inhabited Lean.Elab.Structural.RecArgInfo
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.trans_transHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace Z'] (e : OpenPartialHomeomorph X Y)
  (e' : OpenPartialHomeomorph Y Z) (f'' : Z ≃ₜ Z'), (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')
-- Init.Data.List.Basic
/-- Auxiliary for `range'TR`: `range'TR.go n e = [e-n, ..., e-1] ++ acc`.  -/
List.range'TR.go : ℕ → ℕ → ℕ → List ℕ → List ℕ
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.restrict_pi_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (s : (i : ι) → Set (α i)),
  (MeasureTheory.Measure.pi μ).restrict (Set.univ.pi fun i => s i) =
    MeasureTheory.Measure.pi fun i => (μ i).restrict (s i)
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.isOrderedCancelAddMonoid : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommMonoid N] [inst_2 : PartialOrder N]
  [IsOrderedCancelAddMonoid N], IsOrderedCancelAddMonoid (Colex (α →₀ N))
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.zero : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarAddMonoid R], IsStarNormal 0
-- Mathlib.Geometry.Euclidean.SignedDist
Affine.Simplex.signedInfDist_apply_self : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  (s.signedInfDist i) (s.points i) = ‖s.points i -ᵥ ↑((s.faceOpposite i).orthogonalProjectionSpan (s.points i))‖
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicativeRight_apply_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : AddZeroClass H] (f : Additive G ≃+ H) (a : G),
  (AddEquiv.toMultiplicativeRight f) a = (AddMonoidHom.toMultiplicativeRight f.toAddMonoidHom) a
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq_cert : Int.Internal.Linear.Var → ℤ → Int.Internal.Linear.Poly → Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelp : Lean.FromJson Lean.Lsp.SignatureHelp
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.uniformBell_eq : ∀ (m n : ℕ), m.uniformBell n = ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
-- Init.Data.SInt.Lemmas
Int64.toUInt64_mul : ∀ (a b : Int64), (a * b).toUInt64 = a.toUInt64 * b.toUInt64
-- Mathlib.LinearAlgebra.Determinant
/-- If a linear map is invertible, so is its determinant.  -/
LinearMap.isUnit_det : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_7} [inst_1 : CommRing A] [inst_2 : Module A M] (f : M →ₗ[A] M),
  IsUnit f → IsUnit (LinearMap.det f)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressOptions : Lean.ToJson Lean.Lsp.WorkDoneProgressOptions
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.t0Space : ∀ (α : Type u_1) [inst : UniformSpace α], T0Space (UniformSpace.Completion α)
-- Mathlib.Topology.NhdsKer
IsOpen.nhdsKer_eq : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → nhdsKer s = s