mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.exists_subordinateOrthonormalBasisIndex_eq : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)
  (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) {i : ι},
  V i ≠ ⊥ → ∃ a, DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV' = i
-- Mathlib.RingTheory.FiniteType
RingHom.Finite.finiteType : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B}, f.Finite → f.FiniteType
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero : {α : Type u_3} → [self : LinearOrderedCommGroupWithZero α] → LinearOrderedCommMonoidWithZero α
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.isKProjective_shift_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) (n : ℤ),
  ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).IsKProjective ↔ K.IsKProjective
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- An effective equivalence relation is an equivalence relation `p₁, p₂ : R ⟶ A` together with a
morphism `π : A ⟶ B` such that the resulting square is both a pullback square and a pushout
square.  -/
CategoryTheory.EffectiveEquivalenceRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R A : C} → (R ⟶ A) → (R ⟶ A) → Type (max u_1 v_1)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_add : ∀ (x y : ℝ), ↑(x + y) = ↑x + ↑y
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- The direct sum of two `C^n` vector bundles over the same base is a `C^n` vector bundle.  -/
Bundle.Prod.contMDiffVectorBundle : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B] (F₁ : Type u_11)
  [inst_6 : NormedAddCommGroup F₁] [inst_7 : NormedSpace 𝕜 F₁] (E₁ : B → Type u_12)
  [inst_8 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_9 : (x : B) → AddCommMonoid (E₁ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₁ x)] (F₂ : Type u_13) [inst_11 : NormedAddCommGroup F₂] [inst_12 : NormedSpace 𝕜 F₂]
  (E₂ : B → Type u_14) [inst_13 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_14 : (x : B) → AddCommMonoid (E₂ x)]
  [inst_15 : (x : B) → Module 𝕜 (E₂ x)] [inst_16 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_17 : (x : B) → TopologicalSpace (E₂ x)] [inst_18 : FiberBundle F₁ E₁] [inst_19 : FiberBundle F₂ E₂]
  [inst_20 : VectorBundle 𝕜 F₁ E₁] [inst_21 : VectorBundle 𝕜 F₂ E₂] [ContMDiffVectorBundle n F₁ E₁ IB]
  [ContMDiffVectorBundle n F₂ E₂ IB], ContMDiffVectorBundle n (F₁ × F₂) (fun x => E₁ x × E₂ x) IB
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DHashMap.Raw.Const.get? (m₁ ∩ m₂) k = none
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_toList_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.toList.Perm t₂.toList → t₁.Equiv t₂
-- Mathlib.RingTheory.Regular.Free
instFreeQuotientIdealSpanSingletonSetQuotSMulTop : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  (x : R), Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- The perfect closure of `R` in `A` are the elements `x : A` such that `x ^ p ^ n`
is in `R` for some `n`, where `p` is the exponential characteristic of `R`.  -/
Subalgebra.perfectClosure : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → (p : ℕ) → [ExpChar A p] → Subalgebra R A
-- Mathlib.Data.Int.ModEq
Int.modEq_sub_modulus_mul_iff : ∀ {n a b c : ℤ}, a ≡ b - n * c [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.comp₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8} {γ : ι → Type u_9}
  {mβ : (i : ι) → MeasurableSpace (β i)} {mγ : (i : ι) → MeasurableSpace (γ i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    ∀ (g : (i : ι) → β i → γ i),
      (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
        (∀ (i : ι), AEMeasurable (g i) (MeasureTheory.Measure.map (f i) (μ.bind ⇑κ))) →
          ProbabilityTheory.Kernel.iIndepFun (fun i => g i ∘ f i) κ μ
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- `descPochhammer R n` is the polynomial `X * (X - 1) * ... * (X - n + 1)`,
with coefficients in the ring `R`.
 -/
descPochhammer : (R : Type u) → [inst : Ring R] → ℕ → Polynomial R
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β} {fallback : α},
      (t.insert k v).minKeyD fallback = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivWithinAt_pi' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}
  {Φ' : E →L[𝕜] (i : ι) → F' i},
  HasFDerivWithinAt Φ Φ' s x ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => Φ x i) (ContinuousLinearMap.proj i ∘SL Φ') s x
-- Init.Control.Lawful.Basic
Functor.map_unit : ∀ {f : Type u_1 → Type u_2} [inst : Functor f] [LawfulFunctor f] {a : f PUnit.{u_1 + 1}},
  (fun x => PUnit.unit) <$> a = a
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filterGen≤_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monad.Algebra
/-- To construct an isomorphism of coalgebras, it suffices to give an isomorphism of the carriers which
commutes with the structure morphisms.
 -/
CategoryTheory.Comonad.Coalgebra.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} →
      {A B : G.Coalgebra} →
        (h : A.A ≅ B.A) →
          autoParam
              (CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a)
              CategoryTheory.Comonad.Coalgebra.isoMk._auto_1 →
            (A ≅ B)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.instCartesianMonoidalCategory.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddMon.instCartesianMonoidalCategory =
    { toMonoidalCategory := CategoryTheory.AddMon.monMonoidal,
      isTerminalTensorUnit :=
        CategoryTheory.Limits.IsTerminal.ofUniqueHom
          (fun M => { hom := CategoryTheory.SemiCartesianMonoidalCategory.toUnit M.X, isAddMonHom_hom := ⋯ }) ⋯,
      fst := fun M N => { hom := CategoryTheory.SemiCartesianMonoidalCategory.fst M.X N.X, isAddMonHom_hom := ⋯ },
      snd := fun M N => { hom := CategoryTheory.SemiCartesianMonoidalCategory.snd M.X N.X, isAddMonHom_hom := ⋯ },
      fst_def := ⋯, snd_def := ⋯,
      tensorProductIsBinaryProduct := fun M N =>
        CategoryTheory.Limits.BinaryFan.IsLimit.mk
          (CategoryTheory.Limits.BinaryFan.mk
            { hom := CategoryTheory.SemiCartesianMonoidalCategory.fst M.X N.X, isAddMonHom_hom := ⋯ }
            { hom := CategoryTheory.SemiCartesianMonoidalCategory.snd M.X N.X, isAddMonHom_hom := ⋯ })
          (fun {T} f g => { hom := CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom, isAddMonHom_hom := ⋯ }) ⋯
          ⋯ ⋯ }
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_right_inj_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) [Invertible A] {x y : Matrix n m α}, A * x = A * y ↔ x = y
-- Init.Data.Vector.Lemmas
Vector.getElem?_append_right : ∀ {α : Type u_1} {n m i : ℕ} {xs : Vector α n} {ys : Vector α m}, n ≤ i → (xs ++ ys)[i]? = ys[i - n]?
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_diff_le_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).size ≤ m₁.size
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coe_linearMapAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] (b : B),
  ⇑(Bundle.Trivialization.linearMapAt R e b) = fun y => if b ∈ e.baseSet then (↑e ⟨b, y⟩).2 else 0
-- Init.Data.Range.Polymorphic.PRange
Std.Roo.mk.inj : ∀ {α : Type u} {lower upper lower_1 upper_1 : α},
  ((lower<...upper) = lower_1<...upper_1) → lower = lower_1 ∧ upper = upper_1
-- Mathlib.AlgebraicGeometry.Sites.Affine
/-- Construct an object of affine `P`-schemes over `S` by giving a morphism `Spec R ⟶ S`.  -/
AlgebraicGeometry.Scheme.affineOverMk : {S : AlgebraicGeometry.Scheme} →
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    {R : CommRingCat} → (f : AlgebraicGeometry.Spec R ⟶ S) → P f → P.CostructuredArrow ⊤ AlgebraicGeometry.Scheme.Spec S
-- Lean.Level
Lean.Level.collectMVars : Lean.Level → optParam Lean.LMVarIdSet ∅ → Lean.LMVarIdSet
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.instUnitizationNormedAddCommGroup : (𝕜 : Type u_1) →
  (A : Type u_2) →
    [inst : NormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] → [NormedSpace 𝕜 A] → NormedAddCommGroup (WithLp 1 (Unitization 𝕜 A))
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- A `NormedAddTorsor V P` is a torsor of an additive seminormed group
action by a `SeminormedAddCommGroup V` on points `P`. We bundle the pseudometric space
structure and require the distance to be the same as results from the
norm (which in fact implies the distance yields a pseudometric space, but
bundling just the distance and using an instance for the pseudometric space
results in type class problems).  -/
NormedAddTorsor : (V : outParam (Type u_1)) → (P : Type u_2) → [SeminormedAddCommGroup V] → [PseudoMetricSpace P] → Type (max u_1 u_2)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.Subset.ndinter_eq_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ⊆ t → s.ndinter t = s
-- Lean.Declaration
/-- List of all (including this one) declarations in the same mutual block.
Note that this information is not used by the kernel, and is only used
to save the information provided by the user when using mutual blocks.
Recall that the Lean kernel does not support recursive definitions and they
are compiled using recursors and `WellFounded.fix`.
 -/
Lean.DefinitionVal.all : Lean.DefinitionVal → List Lean.Name
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.smul : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  IsAlgebraic R a → ∀ (r : R), IsAlgebraic R (r • a)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.nil : {V : Type u} → [inst : Quiver V] → {a : V} → Quiver.Path a a
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_div : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A B : SpecialLinearGroup R V), ↑(A / B) = ↑A / ↑B
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- Any measurable set in a countably generated measurable space can be expressed as a union of
atoms.  -/
MeasurableSpace.exists_eq_iUnion_countablyGeneratedAtom : ∀ {α : Type u_1} {mα : MeasurableSpace α} [inst : MeasurableSpace.CountablyGenerated α] {s : Set α},
  MeasurableSet s → ∃ q, s = ⋃ p, if q p then MeasurableSpace.countablyGeneratedAtom α p else ∅
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat : Type
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipWith_eq_zipWithTR.go : ∀ (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : α → β → γ) (as : List α) (bs : List β) (acc : Array γ),
  List.zipWithTR.go✝ f as bs acc = acc.toList ++ List.zipWith f as bs
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.mk.inj : ∀ {R : Type r} {inst : CommRing R} {W' : WeierstrassCurve.Projective R}
  {point : WeierstrassCurve.Projective.PointClass R} {nonsingular : W'.NonsingularLift point}
  {point_1 : WeierstrassCurve.Projective.PointClass R} {nonsingular_1 : W'.NonsingularLift point_1},
  { point := point, nonsingular := nonsingular } = { point := point_1, nonsingular := nonsingular_1 } → point = point_1
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- An idempotent operator is symmetric if and only if its range is
pairwise orthogonal to its kernel.  -/
LinearMap.IsIdempotentElem.isSymmetric_iff_isOrtho_range_ker : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, IsIdempotentElem T → (T.IsSymmetric ↔ T.range ⟂ T.ker)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_iff_keys_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α Unit cmp}, t₁.Equiv t₂ ↔ t₁.keys.Perm t₂.keys
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- The triangle (polygon) inequality for sequences of points; `Finset.range` version.  -/
dist_le_range_sum_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (f : ℕ → α) (n : ℕ),
  dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, dist (f i) (f (i + 1))
-- Init.Data.Array.Monadic
Array.forM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] [LawfulMonad m] {xs ys : Array α}
  {f : α → m PUnit.{u_1 + 1}},
  forM (xs ++ ys) f = do
    forM xs f
    forM ys f
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.del.match_1.splitter : (motive : RBTree.RBColor → Sort u_1) →
  (x : RBTree.RBColor) → (Unit → motive RBTree.RBColor.black) → (Unit → motive RBTree.RBColor.red) → motive x
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.max_zero_right : ∀ (a : Ordinal.{u_1}), max a 0 = a
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.symm : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  {S' : Type u_7} [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'],
  Algebra.IsPushout R S R' S' → Algebra.IsPushout R R' S S'
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.mapMultilinear_apply : ∀ {ι : Type u_1} (R : Type u_4) [inst : CommSemiring R] (s : ι → Type u_7) [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (t : ι → Type u_11) [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i),
  (PiTensorProduct.mapMultilinear R s t) f = PiTensorProduct.map f
-- Init.Notation
/-- The equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. -/
«term_=_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.prodLeftIsoPullback_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  {Z_1 : C} (h : Y.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst Y.hom Z.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.fst) h
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.det_of_mem_unitary : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  {A : Matrix n n α}, A ∈ Matrix.unitaryGroup n α → A.det ∈ unitary α
-- Std.Data.DTreeMap.Internal.Operations
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew? : {α : Type u} →
  {β : Type v} →
    [Ord α] →
      (t : Std.DTreeMap.Internal.Impl α fun x => β) →
        α → β → t.Balanced → Option β × Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.Algebra.Category.Grp.AB
instAB4AddCommGrpCat : CategoryTheory.AB4 AddCommGrpCat
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.homMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  {X Y : P.FullSubcategory}, Function.Surjective CategoryTheory.ObjectProperty.homMk
-- Mathlib.Topology.Algebra.Affine
ContinuousAt.lineMap : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : Ring R]
  [inst_6 : Module R V] [inst_7 : TopologicalSpace R] [ContinuousSMul R V] {X : Type u_6} [inst_9 : TopologicalSpace X]
  {f₁ f₂ : X → P} {g : X → R} {x : X},
  ContinuousAt f₁ x →
    ContinuousAt f₂ x → ContinuousAt g x → ContinuousAt (fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) x
-- Lean.Util.CollectMVars
Lean.CollectMVars.State.result : Lean.CollectMVars.State → Array Lean.MVarId
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.le_infDegree_mul : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : Semiring R] [inst_1 : SemilatticeInf T] [inst_2 : OrderTop T]
  [inst_3 : AddZeroClass A] [inst_4 : Add T] [AddLeftMono T] [AddRightMono T] (D : A →ₙ+ T)
  (f g : AddMonoidAlgebra R A),
  AddMonoidAlgebra.infDegree (⇑D) f + AddMonoidAlgebra.infDegree (⇑D) g ≤ AddMonoidAlgebra.infDegree (⇑D) (f * g)
-- Init.Prelude
/-- The underlying string.  -/
Substring.Raw.str : Substring.Raw → String
-- Lean.Meta.Tactic.NormCast
/-- The `norm_cast` extension data.  -/
Lean.Meta.NormCast.normCastExt : Lean.Meta.NormCast.NormCastExtension
-- Lean.Meta.Tactic.ExposeNames
/-- Returns a copy of the local context in which all declarations have clear, accessible names.  -/
_private.Lean.Meta.Tactic.ExposeNames.0.Lean.Meta.getLCtxWithExposedNames : Lean.MetaM Lean.LocalContext
-- Init.Core
List.cons.inj : ∀ {α : Type u} {head : α} {tail : List α} {head_1 : α} {tail_1 : List α},
  head :: tail = head_1 :: tail_1 → head = head_1 ∧ tail = tail_1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Empty.borelSpace : BorelSpace Empty
-- Mathlib.Topology.Algebra.Monoid
LocallyFinite.exists_finset_support : ∀ {ι : Type u_1} {X : Type u_5} [inst : TopologicalSpace X] {M : Type u_6} [inst_1 : Zero M] {f : ι → X → M},
  (LocallyFinite fun i => Function.support (f i)) →
    ∀ (x₀ : X), ∃ I, ∀ᶠ (x : X) in nhds x₀, (Function.support fun i => f i x) ⊆ ↑I
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.k_compHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {c₁ c₂ c₃ : R} (q : QuaternionAlgebra.Basis A c₁ c₂ c₃) (F : A →ₐ[R] B),
  (q.compHom F).k = F q.k
-- Mathlib.Tactic.Translate.ToDual
/-- The bundle of environment extensions for `to_dual`  -/
Mathlib.Tactic.ToDual.data : Mathlib.Tactic.Translate.TranslateData
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of January.
 -/
Std.Time.Month.Ordinal.january : Std.Time.Month.Ordinal
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instIsZeroApplyReal : ∀ {E : Type u_3} [inst : AddGroup E], IsZeroApply (AddGroupSeminorm E) E ℝ
-- Mathlib.Analysis.Fourier.ZMod
_private.Mathlib.Analysis.Fourier.ZMod.0.ZMod.auxDFT_smul : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (c : ℂ) (Φ : ZMod N → E),
  ZMod.auxDFT✝ (c • Φ) = c • ZMod.auxDFT✝ Φ
-- Mathlib.Topology.Instances.CantorSet
cantorToTernary_ne_one : ∀ {x : ℝ} {n : ℕ}, (cantorToTernary x).get n ≠ 1
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.inv_hom_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (e : A ≅ B) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Topology.NhdsWithin
clusterPt_principal_subtype_iff_frequently : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α},
  s ⊆ t →
    ∀ {J : Set ↑s} {a : ↑s},
      ClusterPt a (Filter.principal J) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) t, ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_mul_measure_univ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  (f : α → ENNReal), (⨍⁻ (a : α), f a ∂μ) * μ Set.univ = ∫⁻ (x : α), f x ∂μ
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `get!` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.Const.get!ₘ : {α : Type u} → {β : Type v} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => β) → α → [Inhabited β] → β
-- Init.Data.String.TakeDrop
/-- If `pat` matches a prefix of `s`, returns the position at the start of the remainder.
Returns `none` otherwise.

This function is generic over all currently supported patterns.
 -/
String.skipPrefix? : {ρ : Type} → (s : String) → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Option s.Pos
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.span_singleton_absNorm_le : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] (I : Ideal S),
  Ideal.span {↑(Ideal.absNorm I)} ≤ I
-- Mathlib.Algebra.GCDMonoid.Basic
/-- **Alias** of `instStrongNormalizationMonoid`. -/
NormalizationMonoid.ofUniqueUnits : {α : Type u_1} → [inst : CommMonoidWithZero α] → [Subsingleton αˣ] → StrongNormalizationMonoid α
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsStrictMinor.trans : ∀ {α : Type u_1} {M M' N : Matroid α}, N <m M → M <m M' → N <m M'
-- Mathlib.Algebra.Polynomial.Div
Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p q : Polynomial R},
  p ∣ q → q.natDegree ≤ p.natDegree → q.leadingCoeff ∣ p.leadingCoeff → Associated p q
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly : Type