mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_le : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L)
  {n : ℕ},
  n ≤ LieAlgebra.IsKilling.chainLength α β → LieAlgebra.rootSpace H (-(n • ⇑α) + ⇑(LieModule.chainTop (⇑α) β)) ≠ ⊥
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The functoriality of `coind₁`.  -/
ContRepresentation.coind₁Map : {R : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : TopologicalSpace V] →
            [inst_3 : IsTopologicalAddGroup V] →
              [inst_4 : Module R V] →
                [inst_5 : AddCommGroup W] →
                  [inst_6 : TopologicalSpace W] →
                    [inst_7 : IsTopologicalAddGroup W] →
                      [inst_8 : Module R W] →
                        {G : Type u_7} →
                          [inst_9 : Group G] →
                            [inst_10 : TopologicalSpace G] →
                              [inst_11 : TopologicalSpace R] →
                                [inst_12 : ContinuousSMul R V] →
                                  [inst_13 : ContinuousSMul R W] →
                                    [inst_14 : IsTopologicalGroup G] →
                                      {π₁ : ContRepresentation R G V} →
                                        {π₂ : ContRepresentation R G W} →
                                          ContIntertwiningMap π₁ π₂ → ContIntertwiningMap π₁.coind₁ π₂.coind₁
-- Mathlib.Order.Closure
LowerAdjoint.closure_union_closure_left : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe) (x y : α),
  l.toFun (↑(l.toFun ↑x) ∪ ↑y) = l.toFun (↑x ∪ ↑y)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticMap.associated_tmul : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : AddCommGroup N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁] [inst_9 : Module R N₁]
  [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : IsScalarTower R A N₁] [inst_14 : Module R M₂] [inst_15 : Module R N₂] [inst_16 : Invertible 2]
  [inst_17 : Invertible 2] (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂),
  QuadraticMap.associated (Q₁.tmul Q₂) = (QuadraticMap.associated Q₁).tmul (QuadraticMap.associated Q₂)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Purity.impure.sizeOf_spec : sizeOf Lean.Compiler.LCNF.Purity.impure = 1
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x y : α),
  ⇑e ⁻¹' Set.Ioc (e x) (e y) = Set.Ioc x y
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of measure `μ` on set `{ω | X ω = x}`.

It is `μ` restricted to `{ω | X ω = x}` and scaled by the inverse of `μ {ω | X ω = x}`
(to make it a probability measure): `(μ {ω | X ω = x})⁻¹ • μ.restrict {ω | X ω = x}`.  -/
ProbabilityTheory.«term__[_|_In_]» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.eq_zero_of_sum_eq_zero : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {s : Finset ι} {w : ι → k} {p : ι → V},
  AffineIndependent k p → ∑ i ∈ s, w i = 0 → ∑ i ∈ s, w i • p i = 0 → ∀ i ∈ s, w i = 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (h : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) {Z : C} (h_1 : h₂.right.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.left.φH (CategoryTheory.CategoryStruct.comp h₂.iso.hom h_1) =
    CategoryTheory.CategoryStruct.comp h₁.iso.hom (CategoryTheory.CategoryStruct.comp h.right.φH h_1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The underlying set of a `SubMulAction`.  -/
SubMulAction.carrier : {R : Type u} → {M : Type v} → [inst : SMul R M] → SubMulAction R M → Set M
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- [Stacks Tag 00Z7](https://stacks.math.columbia.edu/tag/00Z7) -/
CategoryTheory.GrothendieckTopology.isGLB_sInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (s : Set (CategoryTheory.GrothendieckTopology C)),
  IsGLB s (sInf s)
-- Mathlib.Algebra.Group.Basic
inv_pow_sub : ∀ {G : Type u_3} [inst : Group G] (a : G) {m n : ℕ}, n ≤ m → a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instOne : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] →
                [inst_5 : Module R V] → {π₁ : ContRepresentation R G V} → One (ContIntertwiningMap π₁ π₁)
-- Aesop.Forward.State
Aesop.PatSubstSource.hyp.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId),
  (Aesop.PatSubstSource.hyp fvarId = Aesop.PatSubstSource.hyp fvarId_1) = (fvarId = fvarId_1)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_min!_eq_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {hc : t.min! ∈ t}, t.get t.min! hc = t.min ⋯
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translate_iterate : ∀ (x : ℝ) (n : ℕ),
  (⇑↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x)))^[n] =
    ⇑↑(CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x)))
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_eq_Ioc_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc a b = Set.Ioc a b ↔ ¬a ≤ b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Std.Do.PostCond
Std.Do.ExceptConds.const.eq_3 : ∀ (p : Prop) (ε : Type u) (s : Std.Do.PostShape),
  Std.Do.ExceptConds.const p = (fun _ε => ⌜p⌝, Std.Do.ExceptConds.const p)
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.PullbacksPreservedBy.preservesPairwisePullbacks_of_mem : ∀ {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} {J : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor C D}
  [self : J.PullbacksPreservedBy F] ⦃X : C⦄ ⦃R : CategoryTheory.Presieve X⦄,
  R ∈ J.coverings X → F.PreservesPairwisePullbacks R
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {𝕜 : Type u_2} [inst_2 : RCLike 𝕜]
  [inst_3 : NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ E] (a : 𝕜) (f : ℂ → E) (c : ℂ) (R : ℝ),
  ∮ (z : ℂ) in C(c, R), a • f z = a • ∮ (z : ℂ) in C(c, R), f z
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A quadratic map on a module.

For a more familiar constructor when `R` is a ring, see `QuadraticMap.ofPolar`.  -/
QuadraticMap : (R : Type u) →
  (M : Type v) →
    (N : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] → [Module R M] → [inst_3 : AddCommMonoid N] → [Module R N] → Type (max v w)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_comp : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (g f : CentroidHom α), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coeMultisetPNatNat : Coe (Multiset ℕ+) (Multiset ℕ)
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `NonUnitalRing` across an `Equiv`  -/
Equiv.nonUnitalRing : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NonUnitalRing β] → NonUnitalRing α
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.isQuotientMap_of_isColimit_cofork : ∀ {X Y : TopCat} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Cofork f g) (hc : CategoryTheory.Limits.IsColimit c),
  Topology.IsQuotientMap ⇑(CategoryTheory.ConcreteCategory.hom c.π)
-- Mathlib.Algebra.Group.Units.Basic
Units.mul_inv_eq_iff_eq_mul : ∀ {α : Type u} [inst : Monoid α] (b : αˣ) {a c : α}, a * ↑b⁻¹ = c ↔ a = c * ↑b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsert_snd : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.containsThenInsert k v t ⋯).2.impl = (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.pow_subset : ∀ {G : Type u_2} [inst : Group G] {s : Set G} {H : Subgroup G} {n : ℕ}, s ⊆ ↑H → s ^ n ⊆ ↑H
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
ContinuousLinearEquiv.uniformConvergenceCLMCongrSL_symm_apply : ∀ {𝕜 : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} {𝕜₄ : Type u_9} {E : Type u_10} {F : Type u_11} {G : Type u_12}
  {H : Type u_13} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
  [inst_20 : RingHomInvPair σ₁₂ σ₂₁] [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_23 : RingHomInvPair σ₄₃ σ₃₄] [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F)
  (e₄₃ : H ≃SL[σ₄₃] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) (h : ⋯), ⋯
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- The length of an object of `SimplexCategoryGenRel`.  -/
SimplexCategoryGenRel.len : SimplexCategoryGenRel → ℕ
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.comp_apply : ∀ {X Y T : CommGrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInf_nonneg : ∀ {X : Type u_1} {F : Set X} [inst : UniformSpace X] (T : X → X), F.Nonempty → 0 ≤ Dynamics.coverEntropyInf T F
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.distribMulAction : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] →
      [inst_1 : SeminormedAddCommGroup V₂] →
        {R : Type u_5} →
          [inst_2 : MonoidWithZero R] →
            [inst_3 : DistribMulAction R V₂] →
              [inst_4 : PseudoMetricSpace R] → [IsBoundedSMul R V₂] → DistribMulAction R (NormedAddGroupHom V₁ V₂)
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsMinOn.lineDerivWithin_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E},
  IsMinOn f s a → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → lineDerivWithin ℝ f s a b = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mul_inv_rev_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : C) [inst_3 : CategoryTheory.GrpObj G] {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
      (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv)
      (CategoryTheory.CategoryStruct.comp (β_ G G).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h))
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.sigmaMk_mk : ∀ {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) (i : ι) (x : ↥(f i)),
  (AlgebraicGeometry.sigmaMk f) ⟨i, x⟩ = (CategoryTheory.Limits.Sigma.ι f i) x
-- Aesop.Rule.Name
Aesop.instHashableScopeName.hash : Aesop.ScopeName → UInt64
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.geomSum.eq_2 : ∀ {α : Type u_1} [inst : CommRing α] (a b : α) (n : ℕ), geomSum✝ a b n.succ = a * geomSum✝ a b n + b ^ (n + 1)
-- Mathlib.MeasureTheory.Measure.SubFinite
MeasureTheory.Measure.withDensity_sub_of_le : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal}
  [MeasureTheory.IsFiniteMeasure (μ.withDensity g)],
  Measurable g → g ≤ᵐ[μ] f → μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
add_one_le_two_mul : ∀ {R : Type u} [inst : LE R] [inst_1 : NonAssocSemiring R] [AddLeftMono R] {a : R}, 1 ≤ a → a + 1 ≤ 2 * a
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (unit : CategoryTheory.Functor.id C ⟶ F.comp G)
  (counit : G.comp F ⟶ CategoryTheory.Functor.id D)
  (homEquiv_unit :
    autoParam
      (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y},
        (homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (unit.app X) (G.map f))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit._autoParam)
  (homEquiv_counit :
    autoParam
      (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y},
        (homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (counit.app Y))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit._autoParam)
  (homEquiv_1 : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (unit_1 : CategoryTheory.Functor.id C ⟶ F.comp G)
  (counit_1 : G.comp F ⟶ CategoryTheory.Functor.id D)
  (homEquiv_unit_1 :
    autoParam
      (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y},
        (homEquiv_1 X Y) f = CategoryTheory.CategoryStruct.comp (unit_1.app X) (G.map f))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit._autoParam)
  (homEquiv_counit_1 :
    autoParam
      (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y},
        (homEquiv_1 X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (counit_1.app Y))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit._autoParam),
  ({ homEquiv := homEquiv, unit := unit, counit := counit, homEquiv_unit := homEquiv_unit,
        homEquiv_counit := homEquiv_counit } =
      { homEquiv := homEquiv_1, unit := unit_1, counit := counit_1, homEquiv_unit := homEquiv_unit_1,
        homEquiv_counit := homEquiv_counit_1 }) =
    (homEquiv = homEquiv_1 ∧ unit = unit_1 ∧ counit = counit_1)
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unsafeRule.injEq : ∀ (r r_1 : Aesop.UnsafeRule),
  (Aesop.BaseRuleSetMember.unsafeRule r = Aesop.BaseRuleSetMember.unsafeRule r_1) = (r = r_1)
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.front : ∀ {l : List Char} {c : Char} {m r : List Char} {s : Substring.Raw}, Substring.Raw.ValidFor l (c :: m) r s → s.front = c
-- Mathlib.Algebra.Group.Opposite
Commute.op : ∀ {α : Type u_1} [inst : Mul α] {x y : α}, Commute x y → Commute (MulOpposite.op x) (MulOpposite.op y)
-- Init.Data.Vector.Attach
/-- Implementation of `pmap` using the zero-copy version of `attach`.  -/
Vector.pmapImpl : {α : Type u_1} →
  {β : Type u_2} → {n : ℕ} → {P : α → Prop} → ((a : α) → P a → β) → (xs : Vector α n) → (∀ a ∈ xs, P a) → Vector β n
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_dvd2 : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ) (d' : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_right_split ctx p₁ p₂ p₃ d k →
    Int.Internal.Linear.cooper_dvd_right_split_dvd2_cert p₂ p₃ d k d' p' = true →
      d' ∣ Int.Internal.Linear.Poly.denote' ctx p'
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.bot_toSubfield : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  ⊥.toSubfield = (algebraMap F E).fieldRange
-- Lean.Declaration
Lean.instBEqConstructorVal.beq : Lean.ConstructorVal → Lean.ConstructorVal → Bool
-- Mathlib.Algebra.Group.Indicator
Set.apply_mulIndicator_symmDiff : ∀ {α : Type u_1} {β : Type u_2} {G : Type u_6} [inst : Group G] {g : G → β},
  (∀ (x : G), g x⁻¹ = g x) →
    ∀ (s t : Set α) (f : α → G) (x : α),
      g ((symmDiff s t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Iic_add_one : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∏ i ≤ a + 1, f i = (∏ i ≤ a, f i) * f (a + 1)
-- Mathlib.Analysis.Polynomial.Fourier
Polynomial.toAddCircle_X_pow_eq_fourier : ∀ {n : ℕ}, Polynomial.toAddCircle (Polynomial.X ^ n) = fourier ↑n
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instBEqEMatchDiagNode.beq : Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.EMatchDiagNode → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_eraseKey_eq_of_beq_minKey!_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (k == Std.Internal.List.minKey! l) = false →
          Std.Internal.List.minKey! (Std.Internal.List.eraseKey k l) = Std.Internal.List.minKey! l
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instIntCastQuotient : {R : Type u_1} → [inst : AddGroupWithOne R] → [inst_1 : Mul R] → (c : RingCon R) → IntCast c.Quotient
-- Mathlib.Topology.Perfect
/-- If `x` is an accumulation point of a set `C` and `U` is a neighborhood of `x`,
then `x` is an accumulation point of `U ∩ C`.  -/
AccPt.nhds_inter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} {x : α} {U : Set α},
  AccPt x (Filter.principal C) → U ∈ nhds x → AccPt x (Filter.principal (U ∩ C))
-- Mathlib.Tactic.Core
/-- Returns the mathlib root directory.  -/
Mathlib.getMathlibDir : IO System.FilePath
-- Init.Tactics
/-- Experimental Sym-based drop-in for `mvcgen`; see `mvcgen` for documentation.  -/
Lean.Parser.Tactic.vcgenMacro : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrFiberwise_symm_apply : ∀ {α : Type u_9} {β : Type u_10} {γ₁ : α → Type u_11} {γ₂ : β → Type u_12} {f : α → β}
  (e : (b : β) → ((σ : { a // f a = b }) → γ₁ ↑σ) ≃ γ₂ b) (g : (b : β) → γ₂ b) (a : α),
  (Equiv.piCongrFiberwise e).symm g a = (e (f a)).symm (g (f a)) ⟨a, ⋯⟩
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.mk : {X Y : Bipointed} → (toFun : X.X → Y.X) → toFun X.toProd.1 = Y.toProd.1 → toFun X.toProd.2 = Y.toProd.2 → X.Hom Y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {k : α} {v : β k}, (cmp t.maxKey! (t.insertIfNew k v).maxKey!).isLE = true
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_eq_top : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂}, f.range = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- If the Lie span of a set is the whole Lie algebra, then two Lie derivations equal on this set
are equal on the whole Lie algebra.  -/
LieDerivation.ext_of_lieSpan_eq_top : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {D1 D2 : LieDerivation R L M} (s : Set L), LieSubalgebra.lieSpan R L s = ⊤ → Set.EqOn (⇑D1) (⇑D2) s → D1 = D2
-- Mathlib.Combinatorics.Configuration
Configuration.ofField.instMembershipProjectivizationForallFinOfNatNat : {K : Type u_3} → [inst : Field K] → Membership (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  [hi : Inhabited (β k')] {f : β k → β k},
  (m.modify k f).get! k' =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).get! else m.get! k'
-- Mathlib.Topology.Inseparable
not_specializes_iff_exists_closed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, ¬x ⤳ y ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.instIsCancelMulZeroOfIsCancelAdd : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [IsCancelAdd R] [IsCancelMulZero R],
  IsCancelMulZero (MvPolynomial σ R)
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.disjoint_of_mem_compression_of_notMem : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α], a ∈ UV.compression u v s → a ∉ s → Disjoint v a
-- Mathlib.Data.PFun
PFun.dom_of_mem_fix : ∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β}, b ∈ f.fix a → (f a).Dom
-- Batteries.Data.Vector.Lemmas
Vector.get_push_last : ∀ {α : Type u_1} {n : ℕ} (v : Vector α n) (a : α), (v.push a).get (Fin.last n) = a
-- Lean.CompactedRegion
_private.Lean.CompactedRegion.0.Lean.CompactedRegion.root : Lean.CompactedRegion → NonScalar
-- Lean.Elab.Tactic.Omega.Core
/-- The constraint.  -/
Lean.Elab.Tactic.Omega.Fact.constraint : Lean.Elab.Tactic.Omega.Fact → Lean.Omega.Constraint
-- Init.Data.UInt.Bitwise
USize.toUInt8_and : ∀ (a b : USize), (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
-- Mathlib.Data.Sum.Order
OrderIso.sumCongr_refl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β],
  (OrderIso.refl α).sumCongr (OrderIso.refl β) = OrderIso.refl (α ⊕ β)