mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instCompactSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [IsNonarchimedeanLocalField K], CompactSpace ↥(ValuativeRel.valuation K).integer
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.filterMap!_equiv_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : (a : α) → β a → Bool},
  t.WF →
    (Std.DTreeMap.Internal.Impl.filterMap! (fun k => Option.guard fun v => f k v) t).Equiv
      (Std.DTreeMap.Internal.Impl.filter! f t)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.le_total : ∀ {d : ℕ} (a b : ℤ√↑d), a ≤ b ∨ b ≤ a
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instIsCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsCancelMulZero α], IsCancelMulZero αᵒᵈ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
/-- Verify that the constructed limit cone is indeed a limit.  -/
CategoryTheory.Limits.pullbackConeOfRightIsoIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.IsIso g] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.pullbackConeOfRightIso f g)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instBot : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → Bot (ConvexCone R M)
-- Mathlib.Order.SymmDiff
symmDiff_eq_right : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] {a b : α}, symmDiff a b = b ↔ a = ⊥
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.hasFiniteIntegral_comp_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} ⦃f : γ → E⦄,
  MeasureTheory.AEStronglyMeasurable f ((η.comp κ) a) →
    (MeasureTheory.HasFiniteIntegral f ((η.comp κ) a) ↔
      (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral f (η x)) ∧
        MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : γ), ‖f y‖ ∂η x) (κ a))
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodAssoc_apply_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P]
  (x : P), (AddEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inr (AddMonoid.Coprod.inr x)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ofList_singleton : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α}
  {v : β}, Std.ExtHashMap.ofList [(k, v)] = ∅.insert k v
-- Init.Data.Prod
/-- Composing a `Prod.map` with another `Prod.map` is equal to
a single `Prod.map` of composed functions, fully applied.
 -/
Prod.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ)
  (g : β → ε) (g' : δ → ζ) (x : α × γ), Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesEntry.eager : Lean.Meta.Grind.CasesEntry → Bool
-- Lean.Meta.Canonicalizer
/-- Mapping from `Expr` to hash.  -/
Lean.Meta.Canonicalizer.State.cache : Lean.Meta.Canonicalizer.State → Std.HashMap.Raw Lean.Meta.Canonicalizer.ExprVisited UInt64
-- Lean.Elab.PreDefinition.Structural.Eqns
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.findBRecOnLHS.go : {α : Type} → Lean.Expr → (Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.GroupTheory.Finiteness
Monoid.fg_of_surjective : ∀ {M : Type u_1} [inst : Monoid M] {M' : Type u_3} [inst_1 : Monoid M'] [Monoid.FG M] (f : M →* M'),
  Function.Surjective ⇑f → Monoid.FG M'
-- Mathlib.Algebra.BrauerGroup.Defs
instCoeSortCSAType : {K : Type u} → [inst : Field K] → CoeSort (CSA K) (Type v)
-- Init.Core
Nat.succ.injEq : ∀ (u v : ℕ), (u.succ = v.succ) = (u = v)
-- Mathlib.Algebra.Opposites
AddOpposite.op_one : ∀ {α : Type u_1} [inst : One α], AddOpposite.op 1 = 1
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M), b.flag 0 = ⊥
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.Binary.parseLit.go : UInt64 → UInt64 → Std.Internal.Parsec.ByteArray.Parser ℤ
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `t n` is a monotone sequence of sets in `𝔖`
such that each `s ∈ 𝔖` is included in some `t n`
and `V n` is an antitone basis of entourages of `β`,
then `UniformOnFun.gen 𝔖 (t n) (V n)` is an antitone basis of entourages of `α →ᵤ[𝔖] β`.  -/
UniformOnFun.hasAntitoneBasis_uniformity : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} [inst_1 : Preorder ι]
  [IsDirectedOrder ι] {t : ι → Set α} {V : ι → Set (β × β)},
  (∀ (n : ι), t n ∈ 𝔖) →
    Monotone t →
      (∀ s ∈ 𝔖, ∃ n, s ⊆ t n) →
        (uniformity β).HasAntitoneBasis V →
          (uniformity (UniformOnFun α β 𝔖)).HasAntitoneBasis fun n => UniformOnFun.gen 𝔖 (t n) (V n)
-- Batteries.Data.Array.Merge
Array.merge.go.eq_def : ∀ {α : Type u_1} (lt : α → α → Bool) (xs ys acc : Array α) (i j : ℕ),
  Array.merge.go lt xs ys acc i j =
    if hi : i ≥ xs.size then
      acc ++
        ↑(have a := ys;
          a.toSubarray j)
    else
      if hj : j ≥ ys.size then
        acc ++
          ↑(have a := xs;
            a.toSubarray i)
      else
        have x := xs[i];
        have y := ys[j];
        if lt x y = true then Array.merge.go lt xs ys (acc.push x) (i + 1) j
        else Array.merge.go lt xs ys (acc.push y) i (j + 1)
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.instAddAction.eq_1 : ∀ {α : Type u_1} {f : α → α},
  IterateAddAct.instAddAction = { vadd := fun n x => f^[n.val] x, add_vadd := ⋯, zero_vadd := ⋯ }
-- Std.Data.DTreeMap.Internal.Queries
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.DTreeMap.Internal.Impl.Equiv : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop
-- Init.Data.String.Basic
String.Internal.offsetOfPosImpl : String → String.Pos.Raw → ℕ
-- Init.Meta.Defs
/-- Converts a runtime value into surface syntax that denotes it.

Instances do not need to guarantee that the resulting syntax will always re-elaborate into an
equivalent value. For example, the syntax may omit implicit arguments that can usually be found
automatically.
 -/
Lean.Quote : Type → optParam Lean.SyntaxNodeKind `term → Type
-- Mathlib.SetTheory.ZFC.PSet
/-- The empty pre-set  -/
PSet.empty : PSet.{u_1}
-- Mathlib.Data.Option.NAry
/-- Symmetric statement to `Option.map_map₂_antidistrib_left`.  -/
Option.map₂_map_left_anticomm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {α' : Type u_5}
  {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f (g a) b = g' (f' b a)) → Option.map₂ f (Option.map g a) b = Option.map g' (Option.map₂ f' b a)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The additive equivalence `K ⟶ L⟦n⟧ ≃+ Cocycle K L n`.  -/
CochainComplex.HomComplex.Cocycle.equivHomShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          (K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) ≃+ CochainComplex.HomComplex.Cocycle K L n
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.transitivity₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.EquivalenceRelation p₁ p₂),
  CategoryTheory.CategoryStruct.comp self.t p₁ = CategoryTheory.CategoryStruct.comp self.c.fst p₁
-- Init.Data.Nat.Lemmas
Nat.sub_le_iff_le_add : ∀ {a b c : ℕ}, a - b ≤ c ↔ a ≤ c + b
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.option : ∀ {R : Type u_1} [inst : Ring R] {I : Type u_3} {e : I → R} [inst_1 : Fintype I],
  OrthogonalIdempotents e → CompleteOrthogonalIdempotents fun x => x.elim (1 - ∑ i, e i) e
-- Mathlib.Analysis.SpecialFunctions.Sqrt
Real.hasDerivAt_sqrt : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt (fun x => √x) (1 / (2 * √x)) x
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.liftStar_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y),
  (CategoryTheory.WithInitial.liftStar F M hM).inv = CategoryTheory.CategoryStruct.id Z
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f],
  CategoryTheory.inv (CategoryTheory.inv f) = f
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If an equalizer of `f` and `g` exists, we can access the inclusion
`equalizer f g ⟶ X` by saying `equalizer.ι f g`.  -/
CategoryTheory.Limits.equalizer.ι : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f g : X ⟶ Y) → [inst_1 : CategoryTheory.Limits.HasEqualizer f g] → CategoryTheory.Limits.equalizer f g ⟶ X
-- Mathlib.RingTheory.Ideal.Colon
Submodule.annihilator_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M},
  Module.annihilator R (M ⧸ N) = N.colon Set.univ
-- Init.Data.BitVec.Lemmas
BitVec.lt_of_le_ne : ∀ {n : ℕ} {x y : BitVec n}, x ≤ y → ¬x = y → x < y
-- Mathlib.Data.Part
Part.Dom.toOption : ∀ {α : Type u_1} {o : Part α} [inst : Decidable o.Dom] (h : o.Dom), o.toOption = some (o.get h)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedCommGroup.toCommGroup : {E : Type u_8} → [self : SeminormedCommGroup E] → CommGroup E
-- Mathlib.Data.Fintype.CardEmbedding
_private.Mathlib.Data.Fintype.CardEmbedding.0.«term|_|» : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEvalRingHom_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R),
  Polynomial.evalEvalRingHom x = Polynomial.eval₂RingHom (Polynomial.evalRingHom x)
-- Mathlib.Tactic.Linter.FindDeprecations
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.mk.inj : ∀ {module decl : Lean.Name} {rgStart rgStop : Lean.Position} {since : String} {module_1 decl_1 : Lean.Name}
  {rgStart_1 rgStop_1 : Lean.Position} {since_1 : String},
  { module := module, decl := decl, rgStart := rgStart, rgStop := rgStop, since := since } =
      { module := module_1, decl := decl_1, rgStart := rgStart_1, rgStop := rgStop_1, since := since_1 } →
    module = module_1 ∧ decl = decl_1 ∧ rgStart = rgStart_1 ∧ rgStop = rgStop_1 ∧ since = since_1
-- Std.Http.Internal.Char
/-- Checks whether `c` is an ASCII alphanumeric character.
 -/
Std.Http.Internal.Char.isAsciiAlphaNumChar : Char → Bool
-- Init.Data.BitVec.Lemmas
BitVec.mul_neg : ∀ {w : ℕ} (x y : BitVec w), x * -y = -(x * y)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_closure : ∀ {G : Type u_2} [inst : Group G] (s : Set Gᵐᵒᵖ), (Subgroup.closure s).unop = Subgroup.closure (MulOpposite.op ⁻¹' s)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- For `L : C ⥤ D`, taking the Grothendieck construction of `CostructuredArrow.functor L`
precomposed with another functor `R : E ⥤ D` results in a category which is equivalent to
the comma category `Comma L R`.  -/
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (L : CategoryTheory.Functor C D) →
              (R : CategoryTheory.Functor E D) →
                CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)) ≌
                  CategoryTheory.Comma L R
-- Mathlib.CategoryTheory.Iso
CategoryTheory.asIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.asIso f).hom = f
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {D : Type u_1} [inst_3 : CategoryTheory.Category.{v_1, u_1} D],
  ((CategoryTheory.Functor.whiskeringLeft (HomotopyCategory C (ComplexShape.up ℤ)) (DerivedCategory C) D).obj
      DerivedCategory.Qh).Full
-- Mathlib.Data.PFun
_private.Mathlib.Data.PFun.0.PFun.fix.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : β ⊕ α → Sort u_3) (b : β)
  (h_1 : (b_1 : β) → Sum.inl b = Sum.inl b_1 → motive (Sum.inl b_1))
  (h_2 : (a' : α) → Sum.inl b = Sum.inr a' → motive (Sum.inr a')),
  (match e : Sum.inl b with
    | Sum.inl b_1 => h_1 b_1 e
    | Sum.inr a' => h_2 a' e) =
    h_1 b ⋯
-- Mathlib.Order.Bounds.Image
MonotoneOn.mem_upperBounds_image_self : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α} {a : α},
  MonotoneOn f t → a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- If each costructured arrow category on `G` has a terminal object, we have a constructed right
adjoint to `G`.
 -/
CategoryTheory.adjunctionOfCostructuredArrowTerminals : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          [inst_2 : ∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] →
            G ⊣ CategoryTheory.rightAdjointOfCostructuredArrowTerminals G
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.IsSymmetric.coe_toSelfAdjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric), ↑↑hT.toSelfAdjoint = T
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.inter_sdiff_assoc`.

---

See also `Set.sdiff_inter_right_comm`.  -/
Set.inter_diff_assoc : ∀ {α : Type u_1} (a b c : Set α), (a ∩ b) \ c = a ∩ (b \ c)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PullbackCone.unop_inr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g), c.unop.inr = c.snd.unop
-- Mathlib.Topology.Constructions
CofiniteTopology.instInhabited : {X : Type u} → [Inhabited X] → Inhabited (CofiniteTopology X)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.IsComonHom.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.ComonObj M] [inst_3 : CategoryTheory.ComonObj N] {f : M ⟶ N},
  autoParam (CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit)
      CategoryTheory.IsComonHom.hom_counit._autoParam →
    autoParam
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.comul =
          CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
            (CategoryTheory.MonoidalCategoryStruct.tensorHom f f))
        CategoryTheory.IsComonHom.hom_comul._autoParam →
      CategoryTheory.IsComonHom f
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) (X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ)
  {X_1 Y : Fin (n + 1)} (f : X_1 ⟶ Y),
  ((CategoryTheory.ComposableArrows.opEquivalence C n).functor.obj X).map f =
    ((Opposite.unop X).map (⋯.functor.map (CategoryTheory.homOfLE ⋯))).op
-- Lean.Meta.Basic
Lean.Meta.DefEqCacheKey.configKey : Lean.Meta.DefEqCacheKey → UInt64
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.coe_mk : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target)
  (h₃ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.source)
  (h₄ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.target),
  ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂, open_source := h₃, open_target := h₄ } =
    ↑e
-- Lean.Util.ShareCommon
Lean.ShareCommon.PShareCommonT.withShareCommon : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → α → Lean.ShareCommon.PShareCommonT m α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_diff!_eq_false_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.contains k (m₁.diff! m₂) = false
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_of_equivalence : ∀ {C : Type u_1} {D : Type u_2} {D' : Type u_3} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} D']
  [inst_3 : CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D')
  (F : CategoryTheory.Functor C H) (E : D ≌ D') (eL : L.comp E.functor ≅ L') (Y : D) (Y' : D')
  (e : E.functor.obj Y ≅ Y') [L.HasPointwiseLeftKanExtensionAt F Y], L'.HasPointwiseLeftKanExtensionAt F Y'
-- Init.Data.SInt.Bitwise
Int64.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : Int64}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.Data.Sigma.Basic
Sigma.subtype_ext_iff : ∀ {α : Type u_1} {β : Type u_7} {p : α → β → Prop} {x₀ x₁ : (a : α) × Subtype (p a)},
  x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ ↑x₀.snd = ↑x₁.snd
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → (Std.ExtDHashMap.ofList l).size = l.length
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (CategoryTheory.CategoryStruct.comp X.toSpecΓ h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.germ ⊤ x trivial)) h
-- Init.Data.Vector.Count
Vector.count_cast : ∀ {α : Type u_1} [inst : BEq α] {n a : ℕ} {h : n = a} {a_1 : α} {xs : Vector α n},
  Vector.count a_1 (Vector.cast h xs) = Vector.count a_1 xs
-- Mathlib.Logic.Basic
Decidable.ne_or_eq : ∀ {α : Sort u_1} (x y : α) [Decidable (x = y)], x ≠ y ∨ x = y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey a ⋯
-- Mathlib.Order.Heyting.Basic
Prod.instGeneralizedHeytingAlgebra : {α : Type u_2} →
  {β : Type u_3} → [GeneralizedHeytingAlgebra α] → [GeneralizedHeytingAlgebra β] → GeneralizedHeytingAlgebra (α × β)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  (apex : C) (l : apex ⟶ c) (r : apex ⟶ c') (wl : Wₗ l) (wr : Wᵣ r) (apex_1 : C) (l_1 : apex_1 ⟶ c) (r_1 : apex_1 ⟶ c')
  (wl_1 : Wₗ l_1) (wr_1 : Wᵣ r_1),
  ({ apex := apex, l := l, r := r, wl := wl, wr := wr } =
      { apex := apex_1, l := l_1, r := r_1, wl := wl_1, wr := wr_1 }) =
    (apex = apex_1 ∧ l ≍ l_1 ∧ r ≍ r_1)
-- Mathlib.Data.Nat.Factorial.BigOperators
Nat.ascFactorial_eq_prod_range : ∀ (n k : ℕ), n.ascFactorial k = ∏ i ∈ Finset.range k, (n + i)
-- Std.Tactic.Do.Syntax
/-- `mpure` moves a pure hypothesis from the stateful context into the pure context.
```lean
example (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
  mintro Hφ
  mpure Hφ
  mexact (ψ Hφ)
```
 -/
Lean.Parser.Tactic.mpure : Lean.ParserDescr
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.mk.sizeOf_spec : ∀ {α : Type w} [inst : SizeOf α] (array : Array α) (pos : ℕ),
  sizeOf { array := array, pos := pos } = 1 + sizeOf array + sizeOf pos
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_lcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α), normalize (lcm a b) = lcm a b
-- Aesop.BuiltinRules.Split
Aesop.BuiltinRules.splitHypotheses : Aesop.RuleTac
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.forall : ∀ {p : Complex.UnitDisc → Prop},
  (∀ (z : Complex.UnitDisc), p z) ↔ ∀ (z : ℂ) (hz : ‖z‖ < 1), p (Complex.UnitDisc.mk z hz)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- `support` and `vanishingIdeal` forms a Galois connection.
This is the global version of `PrimeSpectrum.gc`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.gc : ∀ {X : AlgebraicGeometry.Scheme},
  GaloisConnection (fun x => x.support) fun x => AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal x
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank_diagonal : ∀ {m : Type um} {R : Type uR} [inst : Field R] [inst_1 : DecidableEq m] (w : m → R),
  (Matrix.diagonal w).cRank = Cardinal.lift.{uR, um} (Cardinal.mk { i // w i ≠ 0 })
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprPasswdInfo : Repr Std.Internal.UV.System.PasswdInfo
-- Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
/-- Third (main) version, with pointwise equicontinuity and range in a compact subset, but
without closedness. The closure is then compact.  -/
BoundedContinuousFunction.arzela_ascoli : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [CompactSpace α] [inst_2 : PseudoMetricSpace β] [T2Space β]
  (s : Set β),
  IsCompact s →
    ∀ (A : Set (BoundedContinuousFunction α β)),
      (∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) →
        (Equicontinuous fun x => ⇑↑x) → IsCompact (closure A)
-- Mathlib.GroupTheory.Rank
AddGroup.rank_congr : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddGroup.FG G]
  [inst_3 : AddGroup.FG H] (e : G ≃+ H), AddGroup.rank G = AddGroup.rank H
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The maps from the induced topology as homs in `TopModuleCat R`.  -/
TopModuleCat.fromInduced : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M : ModuleCat R} →
        {I : Type u_1} →
          {X : I → TopModuleCat R} → (f : (i : I) → M ⟶ (X i).toModuleCat) → (i : I) → TopModuleCat.induced f ⟶ X i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : HomologicalComplex.opcycles (groupHomology.inhomogeneousChains A) 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.opcyclesIso₀ A).inv h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ A).inv
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles (groupHomology.inhomogeneousChains A) 0) h)