mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDivInvMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivInvMonoid α],
  OrderDual.instDivInvMonoid =
    { toMonoid := OrderDual.instMonoid, toInv := OrderDual.instInv, toDiv := OrderDual.instDiv, toZPow := ZPow.ofPow,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {outWidth w : ℕ} →
          aig.RefVec w → outWidth = w * w → Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget aig outWidth
-- Mathlib.Analysis.Normed.Group.Bounded
tendsto_norm_cobounded_atTop' : ∀ {E : Type u_2} [inst : SeminormedGroup E], Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R], (Perfection.teichmuller p I) 0 = 0
-- Mathlib.Probability.Martingale.Convergence
/-- Part b of the **L¹ martingale convergence theorem**: if `f` is a uniformly integrable martingale
strongly adapted to the filtration `ℱ`, then for all `n`, `f n` is almost everywhere equal to the
conditional expectation of its limiting process w.r.t. `ℱ n`.  -/
MeasureTheory.Martingale.ae_eq_condExp_limitProcess : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.UniformIntegrable f 1 μ → ∀ (n : ℕ), f n =ᵐ[μ] μ[MeasureTheory.Filtration.limitProcess f ℱ μ | ↑ℱ n]
-- Mathlib.Data.Sum.Basic
Sum.elim_update_left : ∀ {α : Type u} {β : Type v} {γ : Sort u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → γ) (g : β → γ)
  (a : α) (x : γ), Sum.elim (Function.update f a x) g = Function.update (Sum.elim f g) (Sum.inl a) x
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Node.atom.inj : ∀ {a a_1 : Mathlib.Tactic.Widget.StringDiagram.AtomNode},
  Mathlib.Tactic.Widget.StringDiagram.Node.atom a = Mathlib.Tactic.Widget.StringDiagram.Node.atom a_1 → a = a_1
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edgeSet_replaceVertex_of_not_adj : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V],
  ¬G.Adj s t → (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s
-- Mathlib.GroupTheory.Torsion
/-- The torsion submonoid of a torsion monoid is `⊤`.  -/
IsMulTorsion.torsion_eq_top : ∀ {G : Type u_1} [inst : CommMonoid G], IsMulTorsion G → CommMonoid.torsion G = ⊤
-- Mathlib.LinearAlgebra.Pi
LinearMap.update_apply : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)] [inst_5 : DecidableEq ι]
  (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i j : ι) (b : M₂ →ₗ[R] φ i),
  (Function.update f i b j) c = Function.update (fun i => (f i) c) i (b c) j
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mk.inj : ∀ {R : Type u_14} {S : Type u_15} {inst : Semiring R} {inst_1 : Semiring S} {σ : R →+* S} {M : Type u_16}
  {M₂ : Type u_17} {inst_2 : AddCommMonoid M} {inst_3 : AddCommMonoid M₂} {inst_4 : Module R M} {inst_5 : Module S M₂}
  {toAddHom : M →ₙ+ M₂} {map_smul' : ∀ (m : R) (x : M), toAddHom.toFun (m • x) = σ m • toAddHom.toFun x}
  {toAddHom_1 : M →ₙ+ M₂} {map_smul'_1 : ∀ (m : R) (x : M), toAddHom_1.toFun (m • x) = σ m • toAddHom_1.toFun x},
  { toAddHom := toAddHom, map_smul' := map_smul' } = { toAddHom := toAddHom_1, map_smul' := map_smul'_1 } →
    toAddHom = toAddHom_1
-- Mathlib.Data.QPF.Univariate.Basic
QPF.instInhabitedCofixOfAP : {F : Type u → Type u} → [q : QPF F] → [Inhabited (QPF.P F).A] → Inhabited (QPF.Cofix F)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightKind : Type
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instSupSet : {E : Type u_3} → [inst : AddGroup E] → SupSet (NonarchAddGroupSeminorm E)
-- Lean.Elab.PreDefinition.TerminationHint
/-- True if any form of termination hint is present.  -/
Lean.Elab.TerminationHints.isNotNone : Lean.Elab.TerminationHints → Bool
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.disjoint_hull_right_of_convex : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {C : ConvexCone 𝕜 M} {s : Set M},
  Convex 𝕜 s → (Disjoint C (ConvexCone.hull 𝕜 s) ↔ Disjoint (↑C) s)
-- Mathlib.Algebra.Group.NatPowAssoc
Int.cast_npow : ∀ (R : Type u_2) [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (n : ℤ) (m : ℕ), ↑(n ^ m) = ↑n ^ m
-- Aesop.Percent
Aesop.Percent.mk.sizeOf_spec : ∀ (toFloat : Float), sizeOf { toFloat := toFloat } = 1 + sizeOf toFloat
-- Mathlib.CategoryTheory.Idempotents.Basic
/-- A category is idempotent complete iff for all idempotent endomorphisms,
the equalizer of the identity and this idempotent exists.  -/
CategoryTheory.Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.IsIdempotentComplete C ↔
    ∀ (X : C) (p : X ⟶ X),
      CategoryTheory.CategoryStruct.comp p p = p →
        CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.id X) p
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The special case of the first cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_δ_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)},
  CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ i.castSucc) = CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ i.succ)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.startsWith_char_eq_false_iff_get : ∀ {c : Char} {s : String.Slice}, s.startsWith c = false ↔ ∀ (h : s.startPos ≠ s.endPos), s.startPos.get h ≠ c
-- Mathlib.Data.List.Defs
/-- The head of a list, or the default element of the type is the list is `nil`.  -/
List.headI : {α : Type u_1} → [Inhabited α] → List α → α
-- Mathlib.Data.Finset.Defs
Finset.coe_injective : ∀ {α : Type u_4}, Function.Injective SetLike.coe
-- Init.Data.Order.Classes
Std.IsLinearPreorder.mk : ∀ {α : Type u} [inst : LE α] [toIsPreorder : Std.IsPreorder α], (∀ (a b : α), a ≤ b ∨ b ≤ a) → Std.IsLinearPreorder α
-- Init.Data.List.Lemmas
List.replicate_beq_replicate : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {n : ℕ}, (List.replicate n a == List.replicate n b) = (n == 0 || a == b)
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `R` be a nonarchimedean ring. If functions `f : α → R` and `g : β → R` are summable, then
so is `fun i : α × β ↦ f i.1 * g i.2`.  -/
Summable.mul_of_nonarchimedean : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : UniformSpace R] [IsUniformAddGroup R]
  [NonarchimedeanRing R] {f : α → R} {g : β → R}, Summable f → Summable g → Summable fun i => f i.1 * g i.2
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Replacing the third point by one on the same line does not change twice the oriented angle.  -/
Collinear.two_zsmul_oangle_eq_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₃' : P},
  Collinear ℝ {p₃, p₂, p₃'} →
    p₃ ≠ p₂ → p₃' ≠ p₂ → 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₁ p₂ p₃'
-- Mathlib.GroupTheory.ResiduallyFinite
/-- An additive group `G` is residually finite if the intersection of all finite index normal
additive subgroups is trivial.  -/
AddGroup.ResiduallyFinite : (G : Type u_1) → [AddGroup G] → Prop
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_of_not_le : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, ¬Ideal.map (algebraMap R S) p ≤ P → p.ramificationIdx' P = 0
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : I → C} (f : (i : I) → X i ⟶ S)
  (hf : CategoryTheory.Sieve.ofArrows X f ∈ J S) {E : A} (x : (i : I) → E ⟶ P.obj (Opposite.op (X i)))
  (hx :
    ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
      CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j) →
        CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op))
  (i : I), CategoryTheory.CategoryStruct.comp (hP.amalgamateOfArrows f hf x hx) (P.map (f i).op) = x i
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.continuous_restrictScalars : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5}
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : (i : ι) → Module 𝕜' (E i)]
  [inst_12 : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F],
  Continuous (ContinuousMultilinearMap.restrictScalars 𝕜')
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.cons : Mathlib.Tactic.BicategoryLike.Mor₂ →
  Mathlib.Tactic.BicategoryLike.WhiskerRight →
    Mathlib.Tactic.BicategoryLike.HorizontalComp → Mathlib.Tactic.BicategoryLike.HorizontalComp
-- Mathlib.CategoryTheory.Localization.Adjunction
/-- Auxiliary definition of the unit morphism for the adjunction `Adjunction.localization`  -/
CategoryTheory.Adjunction.Localization.ε : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                {G : CategoryTheory.Functor C₁ C₂} →
                  {F : CategoryTheory.Functor C₂ C₁} →
                    (G ⊣ F) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          [L₁.IsLocalization W₁] →
                            (L₂ : CategoryTheory.Functor C₂ D₂) →
                              (G' : CategoryTheory.Functor D₁ D₂) →
                                (F' : CategoryTheory.Functor D₂ D₁) →
                                  [CategoryTheory.CatCommSq G L₁ L₂ G'] →
                                    [CategoryTheory.CatCommSq F L₂ L₁ F'] → CategoryTheory.Functor.id D₁ ⟶ G'.comp F'
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
              (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
                (𝒰.f k))
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f k))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))
-- Init.Data.List.Lemmas
List.map_eq_flatMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, List.map f l = List.flatMap (fun x => [f x]) l
-- Mathlib.Topology.Defs.Filter
/-- A set `s` is compact if for every nontrivial filter `f` that contains `s`,
there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`.  -/
IsCompact : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if the root of its equivalence class.  -/
Lean.Meta.Grind.isRoot : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.Pseudofunctor B C} (θ : G ⟶ H) {a : B} {a' : C} (f : a' ⟶ G.obj a) {Z : a' ⟶ H.obj a}
  (h :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.id (H.obj a))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.id a)).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapId a).hom)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapId a).hom (θ.app a)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor (θ.app a)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor (θ.app a)).inv) h))
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality**, `ℝ≥0` version with real conjugate exponents.  -/
NNReal.young_inequality_real : ∀ (a b : NNReal) {p q : ℝ}, p.HolderConjugate q → a * b ≤ a ^ p / p.toNNReal + b ^ q / q.toNNReal
-- Mathlib.Data.Num.Lemmas
PosNum.succ.eq_3 : ∀ (n : PosNum), n.bit0.succ = n.bit1
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict_sub : ∀ {R : Type u_10} {R₂ : Type u_11} {M : Type u_12} {M₂ : Type u_13} [inst : Ring R] [inst_1 : Ring R₂] {σ₁₂ : R →+* R₂}
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {p : Submodule R M}
  {q : Submodule R₂ M₂} {f g : M →ₛₗ[σ₁₂] M₂} (hf : Set.MapsTo ⇑f ↑p ↑q) (hg : Set.MapsTo ⇑g ↑p ↑q)
  (hfg : optParam (Set.MapsTo ⇑(f - g) ↑p ↑q) ⋯), f.restrict hf - g.restrict hg = (f - g).restrict hfg
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pullbackMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : X ⟶ S}
  [inst_3 : CategoryTheory.Limits.HasPullbacksAlong f] {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'}
  [inst_4 : CategoryTheory.Limits.HasPullbacksAlong g'] {i₂ : Y ⟶ Y'},
  P i₁ →
    P i₂ →
      ∀ (e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g'),
        P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State.mk.injEq : ∀ (fvars : Array Lean.Expr) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances)
  (expectedType? : Option Lean.Expr) (fvars_1 : Array Lean.Expr) (lctx_1 : Lean.LocalContext)
  (localInsts_1 : Lean.LocalInstances) (expectedType?_1 : Option Lean.Expr),
  ({ fvars := fvars, lctx := lctx, localInsts := localInsts, expectedType? := expectedType? } =
      { fvars := fvars_1, lctx := lctx_1, localInsts := localInsts_1, expectedType? := expectedType?_1 }) =
    (fvars = fvars_1 ∧ lctx = lctx_1 ∧ localInsts = localInsts_1 ∧ expectedType? = expectedType?_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.instSubsingletonIsPointwiseLeftKanExtensionAt : ∀ {C : Type u_1} {D : Type u_2} {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_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D),
  Subsingleton (E.IsPointwiseLeftKanExtensionAt Y)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.star_mul_self_of_mem : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ spinGroup Q → star x * x = 1
-- Mathlib.Data.Finset.Card
/-- Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t`
are equal.

The difference with `Finset.card_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.card_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains.

The difference with `Finset.card_equiv` is that bijectivity is only required to hold on the domains,
rather than on the entire types.  -/
Finset.card_nbij' : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : α → β) (j : β → α),
  Set.MapsTo i ↑s ↑t → Set.MapsTo j ↑t ↑s → Set.LeftInvOn j i ↑s → Set.RightInvOn j i ↑t → s.card = t.card
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} {x y : M₁.Hom M₂}, x.app = y.app → x = y
-- Mathlib.Computability.Encoding
_private.Mathlib.Computability.Encoding.0.Computability.decodePosNum.match_1.splitter : (motive : List Bool → Sort u_1) →
  (x : List Bool) →
    ((l : List Bool) → motive (false :: l)) →
      ((l : List Bool) → motive (true :: l)) →
        ((x : List Bool) →
            (∀ (l : List Bool), x = false :: l → False) → (∀ (l : List Bool), x = true :: l → False) → motive x) →
          motive x
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex'_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq fst snd f g), sq.shortComplex'.f = CategoryTheory.Limits.biprod.lift fst snd
-- Mathlib.Computability.Language
instDecidableEqSymbol : {T : Type u_4} → {N : Type u_5} → [DecidableEq T] → [DecidableEq N] → DecidableEq (Symbol T N)
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
homeomorphSphereProd_symm_apply_coe : ∀ (E : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (r : ℝ) (hr : 0 < r)
  (x : ↑(Metric.sphere 0 r) × ↑(Set.Ioi 0)), ↑((homeomorphSphereProd E r hr).symm x) = ↑x.2 • ↑x.1
-- Lean.Parser.Module
Lean.Parser.parseCommand : Lean.Parser.InputContext →
  Lean.Parser.ParserModuleContext →
    Lean.Parser.ModuleParserState → Lean.MessageLog → Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog
-- Mathlib.Logic.Function.FiberPartition
Function.Fiber.map_eq_image : ∀ {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f) (x : ↑↑a), f ↑x = Function.Fiber.image f a
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.epi_of_epi_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z}
  [CategoryTheory.Epi h], CategoryTheory.CategoryStruct.comp f g = h → CategoryTheory.Epi g
-- Mathlib.GroupTheory.SpecificGroups.Alternating
two_mul_card_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α],
  2 * Fintype.card ↥(alternatingGroup α) = Fintype.card (Equiv.Perm α)
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_of_subsingleton : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] [Subsingleton U] (f : U →ₗ[𝕜] V), f.normDet = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If `C` has a terminal object and `G` preserves terminal objects, then `D` has a terminal object
also.
Note this property is somewhat unique to (co)limits of the empty diagram: for general `J`, if `C`
has limits of shape `J` and `G` preserves them, then `D` does not necessarily have limits of shape
`J`.
 -/
CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G], CategoryTheory.Limits.HasTerminal D
-- Mathlib.Algebra.Order.Field.Basic
exists_add_lt_and_pos_of_lt : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < a → ∃ c, b + c < a ∧ 0 < c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedSymbolTag : Inhabited Lean.Lsp.SymbolTag
-- Lean.Elab.PreDefinition.Structural.Eqns
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.getStructuralRecArgPosImp? : Lean.Name → Lean.CoreM (Option ℕ)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- A strong epimorphism that is a monomorphism is an isomorphism.  -/
CategoryTheory.isIso_of_mono_of_strongEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Mono f]
  [CategoryTheory.StrongEpi f], CategoryTheory.IsIso f
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
equivTangentBundleProd.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  (M' : Type u_7) [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'],
  equivTangentBundleProd I M I' M' =
    { toFun := fun p => (⟨p.proj.1, p.snd.1⟩, ⟨p.proj.2, p.snd.2⟩),
      invFun := fun p => ⟨(p.1.proj, p.2.proj), (p.1.snd, p.2.snd)⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_unop : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [T2Space 𝔸] (x : 𝔸ᵐᵒᵖ),
  NormedSpace.exp (MulOpposite.unop x) = MulOpposite.unop (NormedSpace.exp x)