mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_eq_pi_div_two : ∀ {x : ℝ}, Real.arcsin x = Real.pi / 2 ↔ 1 ≤ x
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- `∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j + g j) * (∏ j > i, f j)`.  -/
Finset.prod_add_ordered : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : LinearOrder ι] (s : Finset ι) (f g : ι → R),
  ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
-- Mathlib.Algebra.Homology.QuasiIso
QuasiIso.quasiIsoAt : ∀ {ι : Type u_1} {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {c : ComplexShape ι} {K L : HomologicalComplex C c} {f : K ⟶ L}
  {inst_2 : ∀ (i : ι), K.HasHomology i} {inst_3 : ∀ (i : ι), L.HasHomology i} [self : QuasiIso f] (i : ι),
  QuasiIsoAt f i
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.constAlter₀ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β}
  {h : 0 < m.buckets.size} {a : α} {f : Option β → Option β},
  m.WF → (↑(Std.DHashMap.Internal.Raw₀.Const.alter ⟨m, h⟩ a f)).WF
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_const_smul_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {G : Type u_6} [inst_1 : Group G] [inst_2 : MulAction G β] [ContinuousConstSMul G β] (c : G),
  MeasureTheory.AEStronglyMeasurable (fun x => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_zero : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B], FractionalIdeal.dual A K 0 = 0
-- Mathlib.Topology.Sheaves.Functors
TopCat.Sheaf.pushforward_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) {F F' : TopCat.Sheaf C X}
  (α : F ⟶ F'), ((TopCat.Sheaf.pushforward C f).map α).hom = (TopCat.Presheaf.pushforward C f).map α.hom
-- Mathlib.Data.Set.Basic
Set.mem_of_subset_of_mem : ∀ {α : Type u} {s₁ s₂ : Set α} {a : α}, s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂
-- Init.Data.Range.Basic
_private.Init.Data.Range.Basic.0.Std.Legacy.Range.forIn'.loop.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_C : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (r : R), m.degree (MvPolynomial.C r) = 0
-- Mathlib.Order.TypeTags
WithBot.eq_1 : ∀ (α : Type u_2), WithBot α = Option α
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y Y' : C}
  (e : F.RepresentableBy Y) (e' : F.RepresentableBy Y'),
  (e.uniqueUpToIso e').hom =
    CategoryTheory.Yoneda.fullyFaithful.preimage
      (CategoryTheory.NatIso.ofComponents
          (fun Z =>
            { hom := TypeCat.ofHom (⇑e'.homEquiv.symm ∘ ⇑e.homEquiv),
              inv := TypeCat.ofHom (⇑e.homEquiv.symm ∘ ⇑e'.homEquiv), hom_inv_id := ⋯, inv_hom_id := ⋯ })
          ⋯).hom
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.add_zsmul_modEq : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a : G} (z : ℤ), a + z • p ≡ a [PMOD p]
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.node : {α : Type u} → Array (Lean.PersistentArrayNode α) → Lean.PersistentArrayNode α
-- Mathlib.Tactic.FBinop
/-- Store macro expansion information to make sure that "go to definition" behaves
similarly to notation defined without using `fbinop%`.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.macroExpansion : Lean.Name → Lean.Syntax → Lean.Syntax → FBinopElab.Tree✝ → FBinopElab.Tree✝
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.union : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Order.IsSuccLimit o →
    Profinite.NobelingProof.contained C o →
      Profinite.NobelingProof.GoodProducts.range C = ⋃ e, Profinite.NobelingProof.GoodProducts.smaller C ↑e
-- Mathlib.Topology.ContinuousMap.SecondCountableSpace
ContinuousMap.instSeparableSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SecondCountableTopology X]
  [LocallyCompactSpace X] [SecondCountableTopology Y], TopologicalSpace.SeparableSpace C(X, Y)
-- Mathlib.Data.Multiset.Filter
Multiset.countP_eq_card_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α),
  Multiset.countP p s = (Multiset.filter p s).card
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.sub : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → μ.Integrable g → μ.Integrable (f - g)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.mk : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : MetricSpace A] [inst_8 : Algebra R A]
  [toContinuousFunctionalCalculus : ContinuousFunctionalCalculus R A p],
  (∀ (a : A) (ha : p a), Isometry ⇑(cfcHom ha)) → IsometricContinuousFunctionalCalculus R A p
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.sigma_apply : ∀ {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [inst : TopologicalSpace A]
  [inst_1 : (i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) (ig : (i : I) × X i),
  (ContinuousMap.sigma f) ig = (f ig.fst) ig.snd
-- Mathlib.Data.Sum.Order
/-- The linear sum of two orders  -/
Sum.Lex.«term_⊕ₗ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cocone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (e : J ≌ K)
  (w : e.functor.comp G ≅ F),
  (P.coconePointsIsoOfEquivalence Q e w).hom =
    P.desc ((CategoryTheory.Limits.Cocone.equivalenceOfReindexing e w).functor.obj t)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_inf : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Opens α} {x : α}, x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.analyticAt_relation_mul_id_pow_six : ∀ (L : PeriodPair), AnalyticAt ℂ (PeriodPair.relation✝ L * id ^ 6) 0
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.precomposing_map_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) {X Y : a ⟶ b} (η : X ⟶ Y) (x : b ⟶ c),
  ((CategoryTheory.Bicategory.precomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerRight η x
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- In a completely regular T0 topological space, the inverse of `diracProbaEquiv` is continuous.  -/
MeasureTheory.continuous_diracProbaEquivSymm : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [inst_3 : T0Space X] [CompletelyRegularSpace X], Continuous ⇑MeasureTheory.diracProbaEquiv.symm
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreCategory : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Groupoid (CategoryTheory.Core C)
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDerivWithin_smul_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {𝕜' : Type u_2} [inst_5 : NormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F} {N : WithTop ℕ∞},
  ContDiffOn 𝕜 N f s →
    ContDiffOn 𝕜 N g s →
      UniqueDiffOn 𝕜 s →
        ∀ {x : E},
          x ∈ s →
            ∀ {n : ℕ},
              ↑n ≤ N →
                ‖iteratedFDerivWithin 𝕜 n (fun y => f y • g y) s x‖ ≤
                  ∑ i ∈ Finset.range (n + 1),
                    ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_3.eq_3 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3)
  (x :
    Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
      Opposite.unop (Opposite.op CategoryTheory.WithInitial.star))
  (x_1 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star)
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
          motive (Opposite.op (CategoryTheory.WithInitial.of x)) (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
          motive (Opposite.op (CategoryTheory.WithInitial.of a)) (Opposite.op CategoryTheory.WithInitial.star) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
      (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
        motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star) x x_2),
  (match Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_1 with
    | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_2 a x x_2
    | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_3 x x_2) =
    h_3 x x_1
-- Aesop.Search.SearchM
Aesop.setMaxRuleApplicationDepthReached : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Unit
-- Mathlib.Data.Set.Sups
/-- The point-wise supremum `a ⊔ b` of `a, b : α`.  -/
«term_⊻_» : Lean.TrailingParserDescr
-- Mathlib.Data.Nat.Prime.Basic
Nat.exists_dvd_of_not_prime2 : ∀ {n : ℕ}, 2 ≤ n → ¬Nat.Prime n → ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n
-- Mathlib.Data.Int.Fib.Basic
Int.fib_neg_two : Int.fib (-2) = -1
-- Std.Data.Iterators.Consumers.Monadic.Set
/-- Traverses the given iterator and stores the emitted values in a `TreeSet`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toTreeSet`.
 -/
Std.IterM.Total.toTreeSet : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.Iterators.Finite α m] →
          [Std.IteratorLoop α m m] → Std.IterM.Total m β → (cmp : β → β → Ordering) → m (Std.TreeSet β cmp)
-- Init.Data.Array.Lemmas
Array.replicate_zero : ∀ {α : Type u_1} {a : α}, Array.replicate 0 a = #[]
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.GetElem?.match_1.splitter : (elem : outParam (Type u_1)) →
  (motive : Option elem → Sort u_2) →
    (x : Option elem) → ((e : elem) → motive (some e)) → (Unit → motive none) → motive x
-- Init.Sym.Simp.SimprocDSL
/-- No discharge. Only unconditional rewrites will apply.  -/
Lean.Parser.Sym.Simp.dischNone : Lean.ParserDescr
-- Mathlib.Topology.Category.CompactlyGenerated
/-- Construct a homeomorphism from an isomorphism.  -/
CompactlyGenerated.homeoOfIso : {X Y : CompactlyGenerated} → (X ≅ Y) → ↑X.toTop ≃ₜ ↑Y.toTop
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) {x : ↥X} (hx : x ∈ f.domain),
  f.fromSpecStalkOfMem hx = CategoryTheory.CategoryStruct.comp (f.domain.fromSpecStalkOfMem x hx) f.hom
-- Mathlib.Algebra.Ring.Defs
Distrib.toMul : {R : Type u_1} → [self : Distrib R] → Mul R
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.getUnusedNames.go.eq_def : ∀ (suggestions : Array Lean.Name) (i : ℕ) (acc : Array Lean.Name) (lctx : Lean.LocalContext),
  Aesop.getUnusedNames.go✝ suggestions i acc lctx =
    if h : i < suggestions.size then
      have name := lctx.getUnusedName suggestions[i];
      have lctx := lctx.addDecl (Aesop.getUnusedNames.dummyLDecl✝ name);
      Aesop.getUnusedNames.go✝ suggestions (i + 1) (acc.push name) lctx
    else (acc, lctx)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.bounded.inj : ∀ {α : Type} {ch ch_1 : Std.CloseableChannel.Bounded✝ α},
  Std.CloseableChannel.Flavors.bounded✝ ch = Std.CloseableChannel.Flavors.bounded✝ ch_1 → ch = ch_1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.subtype_comp_codRestrict : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f : F)
  (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  (NonUnitalStarSubalgebraClass.subtype S).comp (NonUnitalStarAlgHom.codRestrict f S hf) = ↑f
-- Mathlib.Data.ULift
ULift.up_injective : ∀ {α : Type u}, Function.Injective ULift.up
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- `evaluation_coevaluation'` field of `ExactPairing Y X` in a braided category  -/
_private.Mathlib.CategoryTheory.Monoidal.Rigid.Braided.0.CategoryTheory.BraidedCategory.evaluation_coevaluation_braided' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : C} [inst_3 : CategoryTheory.ExactPairing X Y],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (η_ X Y) (β_ Y X).inv) Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y
          (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (ε_ X Y)))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv
-- Lean.Meta.InferType
/-- Returns `true` iff the type of `e` is a `Sort _`.
 -/
Lean.Meta.isType : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_sub : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : AddGroup α] (M N : Matrix (m × o) (n × o) α),
  (M - N).blockDiag = M.blockDiag - N.blockDiag
-- Aesop.Tree.Data
Aesop.GoalState.isProvenByRuleApplication : Aesop.GoalState → Bool
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.WF.combine : ∀ {α : Type u_1} {le : α → α → Bool} {s : Batteries.PairingHeapImp.Heap α} {a : α},
  Batteries.PairingHeapImp.Heap.NodeWF le a s →
    Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.combine le s)
-- Mathlib.GroupTheory.CommutingProbability
commProb.eq_1 : ∀ (M : Type u_1) [inst : Mul M], commProb M = ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card M) ^ 2
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.toLin'_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {V : Type u_1}
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] (b : Module.Basis n R V) (M : GL n R) (v : V),
  ((Matrix.GeneralLinearGroup.toLin' b) M).toLinearEquiv v = (Fintype.linearCombination R ⇑b) ((↑M).mulVec ⇑(b.repr v))
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] (P : CategoryTheory.MorphismProperty D)
  (F : CategoryTheory.Functor C D) (X : D) {X_1 Y : P.CostructuredArrow ⊤ F X} (f : X_1 ⟶ Y),
  (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P F X).map f =
    CategoryTheory.MorphismProperty.Over.homMk (F.map f.left) ⋯ ⋯
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.mk.inj : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} {inst : Zero I₂} {r : I₁ × I₂ × I₃ → J}
  {π : I₁ × I₃ → J} {p₁₂ : I₁ × I₂ → I₁} {hp₁₂ : ∀ (i : I₁ × I₂ × I₃), π (p₁₂ (i.1, i.2.1), i.2.2) = r i}
  {p₂₃ : I₂ × I₃ → I₃} {hp₂₃ : ∀ (i : I₁ × I₂ × I₃), π (i.1, p₂₃ i.2) = r i} {h₁ : ∀ (i₁ : I₁), p₁₂ (i₁, 0) = i₁}
  {h₃ : ∀ (i₃ : I₃), p₂₃ (0, i₃) = i₃} {p₁₂_1 : I₁ × I₂ → I₁}
  {hp₁₂_1 : ∀ (i : I₁ × I₂ × I₃), π (p₁₂_1 (i.1, i.2.1), i.2.2) = r i} {p₂₃_1 : I₂ × I₃ → I₃}
  {hp₂₃_1 : ∀ (i : I₁ × I₂ × I₃), π (i.1, p₂₃_1 i.2) = r i} {h₁_1 : ∀ (i₁ : I₁), p₁₂_1 (i₁, 0) = i₁}
  {h₃_1 : ∀ (i₃ : I₃), p₂₃_1 (0, i₃) = i₃},
  { p₁₂ := p₁₂, hp₁₂ := hp₁₂, p₂₃ := p₂₃, hp₂₃ := hp₂₃, h₁ := h₁, h₃ := h₃ } =
      { p₁₂ := p₁₂_1, hp₁₂ := hp₁₂_1, p₂₃ := p₂₃_1, hp₂₃ := hp₂₃_1, h₁ := h₁_1, h₃ := h₃_1 } →
    p₁₂ = p₁₂_1 ∧ p₂₃ = p₂₃_1
-- Std.Time.Duration
/-- Subtracts a `Week.Offset` from a `Duration`
 -/
Std.Time.Duration.subWeeks : Std.Time.Duration → Std.Time.Week.Offset → Std.Time.Duration
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.toFullSubcategory_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : P.FullSubcategory}
  (Q : HomotopicalAlgebra.Precylinder X.obj) (hQ : P Q.I),
  (Q.toFullSubcategory hQ).i₀ = CategoryTheory.ObjectProperty.homMk Q.i₀
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_roc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = List.drop (lo + 1) (List.take (hi + 1) xs.toList)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.replaceEntry.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (x : List ((a : α) × β a)),
  Std.Internal.List.replaceEntry k v x =
    match x with
    | [] => []
    | ⟨k', v'⟩ :: l => bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: Std.Internal.List.replaceEntry k v l
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.H1Cotangent.map_defaultHom_surjective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  Function.Surjective ⇑(Algebra.Extension.H1Cotangent.map (Algebra.Extension.defaultHom R S P))
-- Mathlib.Data.Set.Lattice.Image
Set.image_iInter₂_subset : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α) (f : α → β),
  f '' ⋂ i, ⋂ j, s i j ⊆ ⋂ i, ⋂ j, f '' s i j
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instHasColimitOverSchemeTopMorphismProperty : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J]
  (F : CategoryTheory.Functor J (P.Over ⊤ S))
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f).left]
  [(F.comp
        ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp
          ((CategoryTheory.Over.forget S).comp AlgebraicGeometry.Scheme.forget))).IsLocallyDirected]
  [Quiver.IsThin J] [Small.{u, u_1} J], CategoryTheory.Limits.HasColimit F
-- Mathlib.NumberTheory.LSeries.Basic
/-- An alternate spelling of `term_def` for the case `f 0 = 0`.  -/
LSeries.term_def₀ : ∀ {f : ℕ → ℂ}, f 0 = 0 → ∀ (s : ℂ) (n : ℕ), LSeries.term f s n = f n * ↑n ^ (-s)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The lineality space of a face of a cone agrees with the lineality space of the cone.  -/
PointedCone.IsFaceOf.lineal_congr : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M}, F.IsFaceOf C → F.lineal = C.lineal
-- Lean.Declaration
Lean.RecursorVal.isUnsafe : Lean.RecursorVal → Bool
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.exists_seq_comp_tendsto : ∀ {α : Type u_1} {ι : Type u_3} {g : Filter ι} [g.IsCountablyGenerated] {u : ι → α} {f : Filter α}
  [f.IsCountablyGenerated],
  (f ⊓ Filter.map u g).NeBot → ∃ θ, Filter.Tendsto θ Filter.atTop g ∧ Filter.Tendsto (u ∘ θ) Filter.atTop f
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHomotopy_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G), CochainComplex.HomComplex.Cochain.ofHomotopy (Homotopy.refl φ) = 0
-- Mathlib.Data.Rat.Lemmas
Rat.ofNat_sub_den : ∀ (n : ℕ) (q : ℚ), (OfNat.ofNat n - q).den = q.den
-- Lean.Meta.Basic
/-- Determines whether two universe level expressions are definitionally equal to each other.
 -/
Lean.Meta.isLevelDefEq : Lean.Level → Lean.Level → Lean.MetaM Bool
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.ne_zero_of_mem_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x a : α}, x ∈ UniqueFactorizationMonoid.normalizedFactors a → x ≠ 0
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.mul_left : ∀ {α : Type u} {β : Type v} {l : Filter α} [inst : Mul β] {f₁ f₂ f₃ : α → β}, f₁ =ᶠ[l] f₂ → f₃ * f₁ =ᶠ[l] f₃ * f₂
-- Mathlib.Algebra.Group.Defs
DivisionCommMonoid.toDivisionMonoid : {G : Type u} → [self : DivisionCommMonoid G] → DivisionMonoid G
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.closedBall_zero' : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α), Metric.closedBall x 0 = closure {x}
-- Mathlib.Order.Hom.BoundedLattice
/-- Reinterpret a `BoundedLatticeHom` as a `BoundedOrderHom`.  -/
BoundedLatticeHom.toBoundedOrderHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] →
        [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedLatticeHom α β → BoundedOrderHom α β
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_asymm : ∀ {x y : PSet.{u_1}}, x ∈ y → y ∉ x
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomCompTriple.right_ids : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂},
  RingHomCompTriple σ₁₂ (RingHom.id R₂) σ₁₂