mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.AssocList
Batteries.AssocList.find?_eq_findEntry? : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (l : Batteries.AssocList α β),
  Batteries.AssocList.find? a l = Option.map (fun x => x.2) (Batteries.AssocList.findEntry? a l)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLTHSubIntOfNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ), t.IsLE ((t.truncLT n).obj X) (n - 1)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U U_1 : Submodule 𝕜 E) (e_U : U = U_1) [inst_3 : U.HasOrthogonalProjection], U.starProjection = U_1.starProjection
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.absolutelyContinuous_compProd_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν]
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] [∀ (x : α), NeZero (κ x)],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) ↔
    μ.AbsolutelyContinuous ν ∧ (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.addSubgroup_congr : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (S S' : AddSubgroup G),
  S = S' → (IsAddQuotientCoveringMap f ↥S ↔ IsAddQuotientCoveringMap f ↥S')
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁ : a ∈ t.insert k v},
  (t.insert k v).get a h₁ = if h₂ : cmp k a = Ordering.eq then cast ⋯ v else t.get a ⋯
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The **Law of Quadratic Reciprocity for the Jacobi symbol**, version with `qrSign`  -/
jacobiSym.quadratic_reciprocity' : ∀ {a b : ℕ}, Odd a → Odd b → jacobiSym (↑a) b = qrSign b a * jacobiSym (↑b) a
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.tsum_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α]
  [T3Space α] {f : β × γ → α},
  Summable f → (∀ (b : β), Summable fun c => f (b, c)) → ∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain_single : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : DecidableEq ι] [inst_1 : DecidableEq κ]
  [inst_2 : (i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (k : κ) (x : β (h k)),
  (DFinsupp.comapDomain h hh fun₀ | h k => x) = fun₀ | k => x
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
CompleteLinearOrder.toConditionallyCompleteLinearOrderBot : {α : Type u_5} → [h : CompleteLinearOrder α] → ConditionallyCompleteLinearOrderBot α
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalOneₐ_liftAlgHom : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) {R : Type u_6} {A : Type u_7} [inst_1 : CommRing R]
  [inst_2 : CommRing A] [inst_3 : Algebra R A] [inst_4 : Algebra R S] (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) (x : A),
  (AdicCompletion.evalOneₐ I) ((AdicCompletion.liftAlgHom I f ⋯) x) = (Ideal.Quotient.factorₐ R ⋯) ((f 1) x)
-- Mathlib.Condensed.Discrete.Colimit
/-- `lanPresheafIso` is natural in `S`.  -/
LightCondensed.lanPresheafNatIso : {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} →
  ((S : LightProfinite) →
      CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) →
    (LightCondensed.lanPresheaf F ≅ F)
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.Clause.relabel.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β) (c : Std.Sat.CNF.Clause α),
  Std.Sat.CNF.Clause.relabel r c =
    List.map
      (fun x =>
        match x with
        | (i, n) => (r i, n))
      c
-- Mathlib.Lean.Meta.DiscrTree
/-- Check if a `keys : Array DiscTree.Key` is "specific",
i.e. something other than `[*]` or `[=, *, *, *]`.
 -/
Lean.Meta.DiscrTree.keysSpecific : Array Lean.Meta.DiscrTree.Key → Bool
-- Mathlib.Topology.Order.LowerUpperTopology
sInfHom.continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] [inst_2 : TopologicalSpace α]
  [Topology.IsLower α] [inst_4 : TopologicalSpace β] [Topology.IsLower β] (f : sInfHom α β), Continuous ⇑f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Complex.cos` is complex analytic.  -/
Complex.analyticAt_cos : ∀ {x : ℂ}, AnalyticAt ℂ Complex.cos x
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.ofLift.eq_1 : ∀ {G : Type u} [inst : Group G] (X : Type u) (of : X → G)
  (lift : {H : Type u} → [inst_1 : Group H] → (X → H) ≃ (G →* H))
  (lift_of : ∀ {H : Type u} [inst_1 : Group H] (f : X → H) (a : X), (lift f) (of a) = f a),
  FreeGroupBasis.ofLift X of lift lift_of = { repr := ((FreeGroup.lift of).toMulEquiv (lift FreeGroup.of) ⋯ ⋯).symm }
-- Mathlib.Data.Fin.Tuple.Basic
Fin.repeat_apply : ∀ {m n : ℕ} {α : Sort u_1} (a : Fin n → α) (i : Fin (m * n)), Fin.repeat m a i = a i.modNat
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivAddCircle_apply_mk : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜),
  (AddCircle.equivAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {f : A →ₗc[R] B} (h : f.toFun 1 = 1) (h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y),
  ⇑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = ⇑f
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.giMapComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f),
  Subsemigroup.giMapComap hf = ⋯.toGaloisInsertion ⋯
-- Mathlib.Tactic.Translate.Core
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.applyReplacementFun.visitLet : Mathlib.Tactic.Translate.TranslateData →
  Lean.Expr →
    optParam (Array Lean.Expr) #[] → optParam Lean.LocalContext { } → Mathlib.Tactic.Translate.ReplacementM Lean.Expr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isSome_maxKey?_modify_eq_isSome : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey?.isSome = t.maxKey?.isSome
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
CategoryTheory.Limits.instHasCokernelMapObjFunctorTypeSigmaConst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (R : C)
  [inst_2 : CategoryTheory.Limits.HasCoproducts C] {α β : Type w} (f : α ⟶ β),
  CategoryTheory.Limits.HasCokernel ((CategoryTheory.Limits.sigmaConst.obj R).map f)
-- Mathlib.LinearAlgebra.Orientation
/-- If the index type has cardinality equal to the finite dimension, an orientation equals the
negation of another orientation if and only if they are not equal.  -/
Orientation.ne_iff_eq_neg : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [FiniteDimensional R M]
  (x₁ x₂ : Orientation R M ι), Fintype.card ι = Module.finrank R M → (x₁ ≠ x₂ ↔ x₁ = -x₂)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_pi_sub : ∀ (x : ℝ), Real.tan (Real.pi - x) = -Real.tan x
-- Init.Data.Iterators.Basic
/-- This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
with `Iter.finitelyManySkips`.
 -/
Std.Iter.TerminationMeasures.Productive.rel_of_skip : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it it' : Std.Iter β},
  it.IsPlausibleStep (Std.IterStep.skip it') → { it := it'.toIterM }.Rel { it := it.toIterM }
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdx : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
  [IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ] [inst_9 : Algebra S Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_11 : Algebra Rₚ Sₚ] (P : Ideal S)
  [hPp : P.LiesOver p] [inst_12 : Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [P.IsPrime],
  (Ideal.map (algebraMap S Sₚ) P).ramificationIdx Rₚ = P.ramificationIdx R
-- Mathlib.Logic.Equiv.Set
Equiv.eq_preimage_iff_image_eq : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (t : Set β), s = ⇑e ⁻¹' t ↔ ⇑e '' s = t
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.DHashMap α β)
  (e_m : m = m_1) (a : α) (h : a ∈ m), m.get a h = m_1.get a ⋯
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_const_mul_right_iff : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S] {f : α → E}
  {l : Filter α} {g : α → S} {c : S}, c ≠ 0 → ((f =O[l] fun x => c * g x) ↔ f =O[l] g)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The trivial monoid algebra is the base ring.  -/
MonoidAlgebra.uniqueAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Monoid M] → [Subsingleton M] → MonoidAlgebra A M ≃ₐ[R] A
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_top_right : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.relIndex ⊤ = H.index
-- Mathlib.Algebra.Ring.Parity
odd_sub_one : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Odd (a - 1) ↔ Even a
-- Mathlib.Algebra.Algebra.Hom
RingHom.equivNatAlgHom_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Semiring R] [inst_1 : Semiring S] (self : R →ₐ[ℕ] S),
  (RingHom.equivNatAlgHom R S).symm self = self.toRingHom
-- Mathlib.Combinatorics.Colex
Finset.Colex.IsInitSeg.exists_initSeg : ∀ {α : Type u_1} [inst : LinearOrder α] {𝒜 : Finset (Finset α)} {r : ℕ} [inst_1 : Fintype α],
  Finset.Colex.IsInitSeg 𝒜 r → 𝒜.Nonempty → ∃ s, s.card = r ∧ 𝒜 = Finset.Colex.initSeg s
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {g₁ g₂ : FrameHom β γ} {f : FrameHom α β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Init.Data.SInt.Lemmas
Int16.maxValue_le_iff : ∀ {a : Int16}, Int16.maxValue ≤ a ↔ a = Int16.maxValue
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsCardinalAccessibleCategory : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular],
  CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ) κ
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
_private.Mathlib.Algebra.Order.Monoid.Unbundled.WithTop.0.WithTop.addMonoid.match_1.eq_2 : ∀ {α : Type u_1} (motive : WithTop α → ℕ → Sort u_2) (h_1 : (a : α) → (n : ℕ) → motive (some a) n)
  (h_2 : Unit → motive none 0) (h_3 : (_n : ℕ) → motive none _n.succ),
  (match none, 0 with
    | some a, n => h_1 a n
    | none, 0 => h_2 ()
    | none, _n.succ => h_3 _n) =
    h_2 ()
-- Init.Data.UInt.Basic
/-- Converts word-sized unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
USize.toUInt8 : USize → UInt8
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.vecMul_injective_iff_isUnit : ∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] {A : Matrix m m K},
  (Function.Injective fun v => Matrix.vecMul v A) ↔ IsUnit A
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyLemma.mk : Mathlib.Tactic.ClickSuggestions.Premise → Mathlib.Tactic.ClickSuggestions.ApplyLemma
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go : {α : Type u} → {β : Type v} → [Ord α] → α → Option (α × β) → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Returns `some uniqueId` if `proof` was marked using `markTheoremInstanceProof`  -/
Lean.Meta.Grind.EMatch.isTheoremInstanceProof? : Lean.Expr → Option Lean.Name
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntry!ₘ_eq_getEntry! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited ((a : α) × β a)] {k : α} {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.getEntry!ₘ k = Std.Internal.List.getEntry! k t.toListModel
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffOn_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {s : Set E}, ContDiffOn 𝕜 n id s
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.Pi.map_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} (f : J → C)
  [inst_1 : CategoryTheory.Limits.HasProduct f] {D : Type t} [inst_2 : CategoryTheory.Category.{r, t} D]
  {FD : D → D → Type u_1} {DD : D → Type (max w r)} [inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)]
  [inst_4 : CategoryTheory.ConcreteCategory D FD] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F]
  [CategoryTheory.Limits.HasProduct fun j => F.obj (f j)]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget D)]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun b => F.obj (f b))
      (CategoryTheory.forget D)]
  (x y : CategoryTheory.ToType (F.obj (∏ᶜ f))),
  (∀ (i : J),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.Pi.π f i))) x =
        (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.Pi.π f i))) y) →
    x = y
-- Mathlib.Algebra.CharP.MixedCharZero
/-- In a local ring `R`, split any predicate over `R` into the three cases:
- *prime power* characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
 -/
split_by_characteristic_localRing : ∀ (R : Type u_1) [inst : CommRing R] {P : Prop} [IsLocalRing R],
  (∀ (p : ℕ), IsPrimePow p → CharP R p → P) →
    (∀ (a : Algebra ℚ R), P) → (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → P
-- Mathlib.Algebra.Group.Action.Defs
vadd_zero_vadd : ∀ {α : Type u_5} {M : Type u_9} (N : Type u_10) [inst : AddMonoid N] [inst_1 : VAdd M N] [inst_2 : AddAction N α]
  [inst_3 : VAdd M α] [VAddAssocClass M N α] (x : M) (y : α), (x +ᵥ 0) +ᵥ y = x +ᵥ y
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Injective.summable_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : γ → β}, Function.Injective g → (∀ x ∉ Set.range g, f x = 0) → (Summable (f ∘ g) ↔ Summable f)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Construct the expression for `η ▷ f`.  -/
Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker : Mathlib.Tactic.BicategoryLike.Mor₂ →
  Mathlib.Tactic.BicategoryLike.WhiskerRight →
    Mathlib.Tactic.BicategoryLike.Atom₁ → Mathlib.Tactic.BicategoryLike.WhiskerRight
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_iSup_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] {a : α} {f : ι → LowerSet α}, a ∈ ⨆ i, f i ↔ ∃ i, a ∈ f i
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- If `i < j` are in `Fin (n + 3)`, this is the isomorphism between `Δ[n]`
and the face of `Δ[n + 2]` corresponding to `{i, j}ᶜ`.  -/
SSet.stdSimplex.facePairComplIso : {n : ℕ} → (i j : Fin (n + 3)) → i < j → (SSet.stdSimplex.obj { len := n } ≅ (SSet.stdSimplex.face {i, j}ᶜ).toSSet)
-- Mathlib.Topology.Algebra.Affine
Filter.Tendsto.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] {α : Type u_6} {l : Filter α} {f₁ f₂ : α → P}
  {g : α → R} {p₁ p₂ : P} {c : R},
  Filter.Tendsto f₁ l (nhds p₁) →
    Filter.Tendsto f₂ l (nhds p₂) →
      Filter.Tendsto g l (nhds c) →
        Filter.Tendsto (fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) l (nhds ((AffineMap.lineMap p₁ p₂) c))
-- Lean.Message
Lean.MessageDataContext.mk.inj : ∀ {env : Lean.Environment} {mctx : Lean.MetavarContext} {lctx : Lean.LocalContext} {opts : Lean.Options}
  {env_1 : Lean.Environment} {mctx_1 : Lean.MetavarContext} {lctx_1 : Lean.LocalContext} {opts_1 : Lean.Options},
  { env := env, mctx := mctx, lctx := lctx, opts := opts } =
      { env := env_1, mctx := mctx_1, lctx := lctx_1, opts := opts_1 } →
    env = env_1 ∧ mctx = mctx_1 ∧ lctx = lctx_1 ∧ opts = opts_1
-- Mathlib.Algebra.Ring.SumsOfSquares
NonUnitalSubsemiring.closure_isSquare : ∀ {T : Type u_2} [inst : NonUnitalCommSemiring T],
  NonUnitalSubsemiring.closure {x | IsSquare x} = NonUnitalSubsemiring.sumSq T
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_sub : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddGroup R] (a b : QuaternionAlgebra R c₁ c₂ c₃), (a - b).imK = a.imK - b.imK
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_intCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocDiv hp (a - ↑m * p) b = toIocDiv hp a b + m
-- Mathlib.Order.WithBot
WithBot.unbotA.eq_1 : ∀ {α : Type u_1} [inst : Nonempty α], WithBot.unbotA = WithBot.unbotD (Classical.arbitrary α)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution_univ : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] [inst_2 : Fintype G] (A : Finset G) (a : G),
  A.convolution Finset.univ a = A.card
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS_zero : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), complEDS b c d k 0 = 0
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandInfo.toElabInfo : Lean.Elab.CommandInfo → Lean.Elab.ElabInfo
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyonedaForget_inv_app_app_hom_apply : ∀ (X : CommMonCatᵒᵖ) (X_1 : CommMonCat) (f : Opposite.unop X ⟶ X_1),
  (CategoryTheory.ConcreteCategory.hom ((CommMonCat.coyonedaForget.inv.app X).app X_1)) f = CommMonCat.Hom.hom f
-- Lean.SubExpr
Lean.SubExpr.Pos.pushNaryFn : ℕ → Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Aesop.ElabM
Aesop.ElabM.run : {α : Type} → Aesop.ElabM.Context → Aesop.ElabM α → Lean.Elab.TermElabM α
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNormedStarGroup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NormedAddCommGroup β] [inst_2 : StarAddMonoid β]
  [inst_3 : NormedStarGroup β], NormedStarGroup (ZeroAtInftyContinuousMap α β)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The seminorms on the space `𝓓^{n}_{K}(E, F)` given by the sup norm of the iterated derivatives.
In the scope `Distributions.Seminorm`, we denote them by `N[𝕜; F]_{K, n, i}`
(or `N[𝕜]_{K, n, i}`), or simply by `N[𝕜; F]_{K, i}` (or `N[𝕜; F]_{K, i}`) when `n = ∞`.  -/
Distributions.«termN[_]_{_,_}» : Lean.ParserDescr
-- Mathlib.Topology.Sheaves.Points
/-- When `X` is a topological space, this is the obvious conservative family of
points on the site `(Opens X, Opens.grothendieckTopology X)`.  -/
Opens.pointsGrothendieckTopology : (X : Type u) → [inst : TopologicalSpace X] → CategoryTheory.ObjectProperty (Opens.grothendieckTopology X).Point
-- Init.Data.String.Termination
String.Pos.ne_startPos_of_prev?_eq_some : ∀ {s : String} {p q : s.Pos}, p.prev? = some q → p ≠ s.startPos
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- At a continuous linear equivalence `e : E ≃L[𝕜] F` between Banach spaces, the operation of
inversion is `C^n`, for all `n`.  -/
contDiffAt_map_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  [CompleteSpace E] (e : E ≃L[𝕜] F), ContDiffAt 𝕜 n ContinuousLinearMap.inverse ↑e
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.isIso_unit_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R)
  (i : L.comp R ≅ CategoryTheory.Functor.id C), CategoryTheory.IsIso adj.unit
-- Mathlib.Algebra.Regular.Basic
/-- If an element `b` becomes left-regular after multiplying it on the left by a left-regular
element, then `b` is left-regular.  -/
IsLeftRegular.of_mul : ∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsLeftRegular (a * b) → IsLeftRegular b
-- Mathlib.Data.Set.Function
Set.BijOn.exists : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {p : β → Prop},
  Set.BijOn f s t → ((∃ b ∈ t, p b) ↔ ∃ a ∈ s, p (f a))
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioo_pred_left_eq_Ioc_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Set.Ioo (Order.pred a) b = Set.Ico a b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insertIfNew k v).maxKey?.isSome = true
-- Mathlib.Data.List.Basic
List.instAssociativeAppend_mathlib : ∀ {α : Type u}, Std.Associative Append.append
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.instSequentialSpaceCarrierToTopCat : ∀ (X : LightCondSet), SequentialSpace ↑X.toTopCat
-- Lean.Compiler.LCNF.Types
/-- Return true iff `type` is `Prop` or `As → Prop`.
 -/
Lean.Compiler.LCNF.isPropFormerType : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.add_isLittleO : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v w : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → w =o[l] v → Asymptotics.IsEquivalent l (u + w) v
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.finsuppCocone.eq_1 : ∀ (R : Type w) [inst : CommRing R] (M ι : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ModuleCat.finsuppCocone R M ι =
    CategoryTheory.Limits.Cofan.mk (ModuleCat.of R (ι →₀ M)) fun i => ModuleCat.ofHom (Finsupp.lsingle i)
-- Lean.Elab.Do.Legacy
/-- Given
- `a` is true if the code block has a `Code.action _` exit point
- `r` is true if the code block has a `Code.return _ _` exit point
- `bc` is true if the code block has a `Code.break _` or `Code.continue _` exit point

generate Kind. See comment at the beginning of the `ToTerm` namespace.  -/
Lean.Elab.Term.Do.ToTerm.mkNestedKind : Bool → Bool → Bool → Lean.Elab.Term.Do.ToTerm.Kind