mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.foldr : {α : Type u} → {cmp : α → α → Ordering} → {δ : Type w} → (α → δ → δ) → δ → Std.TreeSet.Raw α cmp → δ
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.getOp : Lean.Meta.Grind.AC.ACM Lean.Expr
-- Init.Data.List.Basic
List.length.eq_def : ∀ {α : Type u_1} (x : List α),
  x.length =
    match x with
    | [] => 0
    | head :: as => as.length + 1
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_X : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).X i =
    CategoryTheory.Limits.pullback f (CategoryTheory.CategoryStruct.comp (𝒰.f i) g)
-- Mathlib.RingTheory.Extension.Generators
/-- The assignment of each variable in `I` to a value in `P' = R'[X']`.  -/
Algebra.Generators.Hom.val : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {P : Algebra.Generators R S ι} →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst_3 : CommRing R'] →
                      [inst_4 : CommRing S'] →
                        [inst_5 : Algebra R' S'] →
                          {P' : Algebra.Generators R' S' ι'} → [inst_6 : Algebra S S'] → P.Hom P' → ι → P'.Ring
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.run : Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.s.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (i : ℕ) → motive i.succ),
  (match 0 with
    | 0 => h_1 ()
    | i.succ => h_2 i) =
    h_1 ()
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Epi S.v₂₃.τ₁
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_descCochain : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n),
  (CochainComplex.mappingCone.inl φ).comp (CochainComplex.mappingCone.descCochain φ α β h) ⋯ = α
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_le_of_le : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ}, ‖a₁‖ ≤ r₁ → ‖a₂‖ ≤ r₂ → ‖a₁ / a₂‖ ≤ r₁ + r₂
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ext_get? : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtTreeSet α cmp},
  (∀ (k : α), t₁.get? k = t₂.get? k) → t₁ = t₂
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?ₘ'.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGT?ₘ' k t =
    Std.DTreeMap.Internal.Impl.explore (fun k' => (compare k k').then Ordering.gt) none
      (fun x x_1 =>
        match x, x_1 with
        | x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_1 => some ⟨k', v⟩
        | base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 r => r.head?.or base
        | base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3 => base)
      t
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertManyIfNewUnit_ind : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ α]
  {motive : Std.HashMap.Raw α Unit → Prop} (m : Std.HashMap.Raw α Unit) (l : ρ),
  motive m →
    (∀ (m : Std.HashMap.Raw α Unit) (a : α), motive m → motive (m.insertIfNew a ())) → motive (m.insertManyIfNewUnit l)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.piecewise_apply : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [inst : (x : α) → Decidable (x ∈ s)]
  [inst_1 : (y : β) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t),
  ↑(e.piecewise e' s t H H') = s.piecewise ↑e ↑e'
-- Init.Data.Nat.Lemmas
/-- Dependent version of `decidableExistsLT`.  -/
Nat.decidableExistsLT' : {k : ℕ} →
  {p : (m : ℕ) → m < k → Prop} → [I : (m : ℕ) → (h : m < k) → Decidable (p m h)] → Decidable (∃ m, ∃ (h : m < k), p m h)
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toPlus P) F) (J.plusCompIso F P).hom =
    J.toPlus (P.comp F)
-- Mathlib.Algebra.Group.Center
IsMulCentral.right_comm : ∀ {M : Type u_1} {c : M} [inst : Mul M], IsMulCentral c → ∀ (a b : M), a * b * c = a * c * b
-- Mathlib.Algebra.Homology.QuasiIso
CochainComplex.quasiIsoAt₀_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℕ} (f : K ⟶ L) [inst_2 : HomologicalComplex.HasHomology K 0]
  [inst_3 : HomologicalComplex.HasHomology L 0] [inst_4 : (HomologicalComplex.sc' K 0 0 1).HasHomology]
  [inst_5 : (HomologicalComplex.sc' L 0 0 1).HasHomology],
  QuasiIsoAt f 0 ↔
    CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map f)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] {A : Type u_2} [inst_2 : NonUnitalRing A]
  [inst_3 : StarRing A] [inst_4 : Module ℝ A] (φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A)
  (f : ContinuousMapZero X ℝ), φ.realContinuousMapZeroOfNNReal f = φ f.toNNReal - φ (-f).toNNReal
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Finite.mk : ∀ {α : Type u_1} {M : Matroid α}, M.E.Finite → M.Finite
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.map : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] {e : M}, IsIdempotentElem e → ∀ (f : F), IsIdempotentElem (f e)
-- Mathlib.RingTheory.Localization.Module
Module.Basis.localizationLocalization_span : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {A : Type u_3} [inst_4 : CommSemiring A] [inst_5 : Algebra R A]
  (Aₛ : Type u_4) [inst_6 : CommSemiring Aₛ] [inst_7 : Algebra A Aₛ] [inst_8 : Algebra Rₛ Aₛ] [inst_9 : Algebra R Aₛ]
  [inst_10 : IsScalarTower R Rₛ Aₛ] [inst_11 : IsScalarTower R A Aₛ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Module.Basis ι R A),
  Submodule.span R (Set.range ⇑(Module.Basis.localizationLocalization Rₛ S Aₛ b)) =
    (↑(IsScalarTower.toAlgHom R A Aₛ)).range
-- Init.Data.Option.Lemmas
Option.eq_some_iff_get_eq : ∀ {α : Type u_1} {o : Option α} {a : α}, o = some a ↔ ∃ (h : o.isSome = true), o.get h = a
-- Mathlib.Algebra.Order.Ring.WithTop
_private.Mathlib.Algebra.Order.Ring.WithTop.0.WithTop.instMonoidWithZero.match_1.eq_3 : ∀ {α : Type u_1} (motive : WithTop α → ℕ → Sort u_2) (_n : ℕ) (h_1 : (a : α) → (n : ℕ) → motive (some a) n)
  (h_2 : Unit → motive none 0) (h_3 : (_n : ℕ) → motive none _n.succ),
  (match none, _n.succ with
    | some a, n => h_1 a n
    | none, 0 => h_2 ()
    | none, _n.succ => h_3 _n) =
    h_3 _n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {combined w : ℕ} (n n_1 : ℕ)
  (e_n : n = n_1) (inner inner_1 : aig.RefVec w),
  inner = inner_1 →
    ∀ (h : combined = w * n),
      { w := w, n := n, inner := inner, h := h } = { w := w, n := n_1, inner := inner_1, h := ⋯ }
-- Mathlib.Data.Quot
Quot.map_surjective : ∀ {α : Sort u_1} {β : Sort u_2} {ra : α → α → Prop} {rb : β → β → Prop} {f : α → β}
  (h : ∀ ⦃a b : α⦄, ra a b → rb (f a) (f b)), Function.Surjective f → Function.Surjective (Quot.map f h)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  [inst_2 : DecidableEq σ] [inst_3 : DecidableEq R] [inst_4 : DecidableEq M]
  (x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)),
  (DirectSum.coeAddMonoidHom fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x =
    DFinsupp.sum x fun x x_1 => ↑x_1
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.Q : (α : Type u) → [Lean.Grind.Semiring α] → Type u
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
Lean.Elab.Structural.RecArgInfo.mk.injEq : ∀ (fnName : Lean.Name) (fixedParamPerm : Lean.Elab.FixedParamPerm) (recArgPos : ℕ) (indicesPos : Array ℕ)
  (indGroupInst : Lean.Elab.Structural.IndGroupInst) (indIdx : ℕ) (fnName_1 : Lean.Name)
  (fixedParamPerm_1 : Lean.Elab.FixedParamPerm) (recArgPos_1 : ℕ) (indicesPos_1 : Array ℕ)
  (indGroupInst_1 : Lean.Elab.Structural.IndGroupInst) (indIdx_1 : ℕ),
  ({ fnName := fnName, fixedParamPerm := fixedParamPerm, recArgPos := recArgPos, indicesPos := indicesPos,
        indGroupInst := indGroupInst, indIdx := indIdx } =
      { fnName := fnName_1, fixedParamPerm := fixedParamPerm_1, recArgPos := recArgPos_1, indicesPos := indicesPos_1,
        indGroupInst := indGroupInst_1, indIdx := indIdx_1 }) =
    (fnName = fnName_1 ∧
      fixedParamPerm = fixedParamPerm_1 ∧
        recArgPos = recArgPos_1 ∧ indicesPos = indicesPos_1 ∧ indGroupInst = indGroupInst_1 ∧ indIdx = indIdx_1)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.ofNat_le_lift_iff : ∀ {a : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n ≤ Cardinal.lift.{v, u} a ↔ OfNat.ofNat n ≤ a
-- Mathlib.Algebra.Field.Defs
/-- A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  -/
DivisionRing : Type u_2 → Type u_2
-- Mathlib.Algebra.Group.ULift
ULift.addMonoid.eq_1 : ∀ {α : Type u} [inst : AddMonoid α], ULift.addMonoid = Function.Injective.addMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Set.UnionLift
Set.iUnionLift_of_mem : ∀ {α : Type u_1} {ι : Sort u_3} {β : Sort u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  {hT : T ⊆ Set.iUnion S} (x : ↑T) {i : ι} (hx : ↑x ∈ S i), Set.iUnionLift S f hf T hT x = f i ⟨↑x, hx⟩
-- Mathlib.NumberTheory.Cyclotomic.Basic
isCyclotomicExtension_iff : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  IsCyclotomicExtension S A B ↔
    (∀ {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n) ∧
      ∀ (x : B), x ∈ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- If `B` is a faithfully flat `A`-algebra, the induced map on the prime spectrum is
surjective.  -/
PrimeSpectrum.comap_surjective_of_faithfullyFlat : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B], Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
-- Mathlib.Data.Set.List
Set.range_list_getD : ∀ {α : Type u_1} (l : List α) (d : α), (Set.range fun n => l[n]?.getD d) = insert d {x | x ∈ l}
-- Init.System.IO
/-- Creates a new task that waits for all the tasks in the list `tasks` to complete, and then runs the
`EIO ε` action `f` on their results. This new task has priority `prio`.

Running the resulting `BaseIO` action causes the task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped.
 -/
EIO.mapTasks : {α : Type u_1} →
  {ε β : Type} →
    (List α → EIO ε β) →
      List (Task α) → optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task (Except ε β))
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.coe_bipartiteAbove : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Finset β) (a : α) [inst : DecidablePred (r a)],
  ↑(Finset.bipartiteAbove r t a) = {b | b ∈ t ∧ r a b}
-- Mathlib.Data.Finset.Card
Set.LeftInvOn.eq_1 : ∀ {α : Type u} {β : Type v} (g : β → α) (f : α → β) (s : Set α), Set.LeftInvOn g f s = ∀ ⦃x : α⦄, x ∈ s → g (f x) = x
-- Mathlib.Order.SupClosed
infClosed_univ : ∀ {α : Type u_3} [inst : SemilatticeInf α], InfClosed Set.univ
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_algebraMap : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_3} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜₁ E] {S : Type u_5} [inst_4 : CommSemiring S] [inst_5 : Module S E] [inst_6 : SMulCommClass 𝕜₁ S E]
  [inst_7 : SMul S 𝕜₁] [inst_8 : IsScalarTower S 𝕜₁ E] [inst_9 : ContinuousConstSMul S E]
  [inst_10 : IsTopologicalAddGroup E] (c : S), ((algebraMap S (E →WOT[𝕜₁] E)) c).toCLM = (algebraMap S (E →L[𝕜₁] E)) c
-- Mathlib.Order.CompleteBooleanAlgebra
iInf₂_codisjoint_iff : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : Order.Coframe α] {a : α} {f : (i : ι) → κ i → α},
  Codisjoint (⨅ i, ⨅ j, f i j) a ↔ ∀ (i : ι) (j : κ i), Codisjoint (f i j) a
-- Mathlib.CategoryTheory.Category.Cat
/-- The type of 1-morphisms in the bicategory of categories `Cat`.
This is a structure around `Functor` to prevent defeq-abuse
 -/
CategoryTheory.Cat.Hom : CategoryTheory.Cat → CategoryTheory.Cat → Type (max u v)
-- Mathlib.Data.Num.Basic
/-- The successor of a `Num` as a `Num`.  -/
Num.succ : Num → Num
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearEquiv.coe_toContinuousLinearEquiv_symm : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F]
  [inst_13 : FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F), ↑(↑e.toContinuousLinearEquiv).symm = ↑e.symm
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin : ∀ (R : Type uR) {S : Type uS} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] (s : Set S)
  (t : Set A),
  Algebra.adjoin R (⇑(algebraMap S A) '' s ∪ t) =
    Subalgebra.restrictScalars R (Algebra.adjoin (↥(Algebra.adjoin R s)) t)
-- Mathlib.Tactic.Translate.Core
/-- Copy the instance attribute in a `to_additive`

[todo] it seems not to work when the `to_additive` is added as an attribute later.  -/
Mathlib.Tactic.Translate.copyInstanceAttribute : Lean.Name → Lean.Name → Lean.CoreM Unit
-- Init.Data.Int.Lemmas
Int.beq'_eq_beq : ∀ (a b : ℤ), a.beq' b = (a == b)
-- Mathlib.Data.Finset.Insert
Finset.prodPiInsert.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (f : α → Type u_3) {a : α} (x : f a × ((i : α) → i ∈ s → f i))
  (i : α) (hi : i ∈ insert a s), Finset.prodPiInsert f x i hi = if h : i = a then cast ⋯ x.1 else x.2 i ⋯
-- Mathlib.Data.Fin.VecNotation
PiFin.toExpr : {α : Type u} → [Lean.ToLevel] → [Lean.ToExpr α] → (n : ℕ) → Lean.ToExpr (Fin n → α)
-- Mathlib.Algebra.Lie.Graded
DirectSum.instLieRingSubtypeMemSubmodule : {ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid ι] →
          [inst_2 : CommRing R] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] →
                (ℒ : ι → Submodule R L) → [GradedLieAlgebra ℒ] → LieRing (DirectSum ι fun i => ↥(ℒ i))
-- Init.Data.Vector.Lemmas
Vector.getElem_eq_iff : ∀ {α : Type u_1} {n : ℕ} {x : α} {xs : Vector α n} {i : ℕ} {h : i < n}, xs[i] = x ↔ xs[i]? = some x
-- Mathlib.Order.CompleteLattice.Basic
iSup₂_mono : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {f g : (i : ι) → κ i → α},
  (∀ (i : ι) (j : κ i), f i j ≤ g i j) → ⨆ i, ⨆ j, f i j ≤ ⨆ i, ⨆ j, g i j
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.ofNat_ctorIdx : ∀ (x : Std.Time.Weekday), Std.Time.Weekday.ofNat x.ctorIdx = x
-- Init.Data.List.Attach
List.foldl_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : List (Subtype P)} {f : β → α → β} {x : β},
  List.foldl f x xs.unattach =
    List.foldl
      (fun s x =>
        match x with
        | ⟨x, h⟩ => binderNameHint s f (binderNameHint x (f s) (binderNameHint h () (f s (wfParam x)))))
      x xs
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
Std.IterM.append.eq_1 : ∀ {m : Type w → Type w'} {β α₁ α₂ : Type w} [inst : Std.Iterator α₁ m β] [inst_1 : Std.Iterator α₂ m β]
  (it₁ : Std.IterM m β) (it₂ : Std.IterM m β),
  it₁.append it₂ = { internalState := Std.Iterators.Types.Append.fst it₁ it₂ }
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- This is another convenient method to verify that a cotrident is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts.  -/
CategoryTheory.Limits.Cotrident.IsColimit.mk' : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            (t : CategoryTheory.Limits.Cotrident f) →
              ((s : CategoryTheory.Limits.Cotrident f) →
                  { l //
                    CategoryTheory.CategoryStruct.comp t.π l = s.π ∧
                      ∀
                        {m :
                          ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj
                              CategoryTheory.Limits.WalkingParallelFamily.one ⟶
                            ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj
                                  s.pt).obj
                              CategoryTheory.Limits.WalkingParallelFamily.one},
                        CategoryTheory.CategoryStruct.comp t.π m = s.π → m = l }) →
                CategoryTheory.Limits.IsColimit t
-- Lean.Elab.PreDefinition.Main
Lean.Elab.shouldUseStructural : Array Lean.Elab.PreDefinition → Bool
-- Mathlib.GroupTheory.Perm.ClosureSwap
/-- A transitive permutation group generated by transpositions must be the whole symmetric group  -/
closure_of_isSwap_of_isPretransitive : ∀ {α : Type u_2} [inst : DecidableEq α] [Finite α] {S : Set (Equiv.Perm α)},
  (∀ σ ∈ S, σ.IsSwap) → ∀ [MulAction.IsPretransitive (↥(Subgroup.closure S)) α], Subgroup.closure S = ⊤
-- Lean.Elab.Binders
/-- Elaborate as a nondependent `let` (a `have`).  -/
Lean.Elab.Term.LetConfig.nondep : Lean.Elab.Term.LetConfig → Bool
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.rightRel.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), QuotientAddGroup.rightRel s = AddAction.orbitRel (↥s) α
-- Mathlib.CategoryTheory.Category.TwoP
/-- Adding a first point is left adjoint to forgetting the first point.  -/
pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction : pointedToTwoPSnd ⊣ (CategoryTheory.forget₂ TwoP Bipointed).comp bipointedToPointedSnd
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.lt_card_lt_iff_apply_lt_of_monotone : ∀ {n : ℕ} {α : Type u_1} {j : Fin n} {f : Fin n → α} [inst : Preorder α] {a : α} [inst_1 : DecidableLT α],
  Monotone f → (↑j < {i | f i < a}.card ↔ f j < a)
-- Mathlib.Order.Lattice
sup_inf_self : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊔ a ⊓ b = a
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The functor from `Pointed` to `Bipointed` which adds a first point.  -/
pointedToBipointedSnd : CategoryTheory.Functor Pointed Bipointed
-- Lean.Parser.Term
/-- Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
e.g. because it has no constructors.
 -/
Lean.Parser.Term.nomatch : Lean.Parser.Parser
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.pure_one : ∀ (A : Type u_2) [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  (pure 1).IsIncreasingApproximateUnit
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokenType : Lean.FromJson Lean.Lsp.SemanticTokenType
-- Mathlib.Topology.Maps.Basic
/-- Assume `f` is a closed map. If there are points `y` arbitrarily close to `y₀` such that `p`
holds for at least some `x ∈ f ⁻¹' {y}`, then one can find `x₀ ∈ f ⁻¹' {y₀}` such that there
are points `x` arbitrarily close to `x₀` which satisfy `p`.  -/
IsClosedMap.frequently_nhds_fiber : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f →
    ∀ {p : X → Prop} (y₀ : Y),
      (∃ᶠ (y : Y) in nhds y₀, ∃ x ∈ f ⁻¹' {y}, p x) → ∃ x₀ ∈ f ⁻¹' {y₀}, ∃ᶠ (x : X) in nhds x₀, p x
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasNatValPattern : Lean.Meta.Match.Problem → Lean.MetaM Bool
-- Init.Prelude
/-- `a - b` computes the difference of `a` and `b`. See `HSub`.  -/
Sub.sub : {α : Type u} → [self : Sub α] → α → α → α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.rightHomologyIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.rightHomologyIso.hom (CategoryTheory.ShortComplex.homologyMap φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) S₂.rightHomologyIso.hom