mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.semiring : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [AddMonoid M] → Semiring (AddMonoidAlgebra R M)
-- Init.Grind.Config
/-- When `true`, it reverts all hypotheses during the preprocessing step,
and then reintroduces them while simplifying and applying eager `cases`.
 -/
Lean.Grind.Config.revert : Lean.Grind.Config → Bool
-- Init.Data.List.Find
/-- `p` does not hold for elements with indices less than `xs.findIdx p`.  -/
List.not_of_lt_findIdx : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ} (h : i < List.findIdx p xs), p xs[i] = false
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.instIsOrderedAddCancelMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : Preorder β] [IsOrderedCancelAddMonoid β], IsOrderedCancelAddMonoid (α × β)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_id_set_eq_sInter : ∀ {α : Type u_2} (s : Finset (Set α)), s.inf id = ⋂₀ ↑s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.DHashMap.Raw.ofList l).getKey! k' = k
-- Mathlib.RingTheory.PowerBasis
PowerBasis.adjoin_eq_top_of_gen_mem_adjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {B : PowerBasis R S}
  {x : S}, B.gen ∈ R[x] → R[x] = ⊤
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
/-- Let `K₁` and `K₂` be two number fields and assume that `K₁/ℚ` is Galois. If `discr K₁` and
`discr K₂` are coprime, then they are linear disjoint over `ℚ`.
 -/
NumberField.linearDisjoint_of_isGalois_isCoprime_discr : ∀ (L : Type u_3) [inst : Field L] [inst_1 : NumberField L] (K₁ K₂ : IntermediateField ℚ L) [IsGalois ℚ ↥K₁],
  IsCoprime (NumberField.discr ↥K₁) (NumberField.discr ↥K₂) → K₁.LinearDisjoint ↥K₂
-- Init.Data.Array.Attach
Array.flatMap_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Array β} {g : α → Array β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Array.flatMap f xs = Array.flatMap g xs.unattach
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.IsInitial.isPrincipal_opow`. -/
Ordinal.IsInitial.principal_opow : ∀ {o : Ordinal.{u_1}}, o.IsInitial → Ordinal.omega0 ≤ o → Ordinal.IsPrincipal (fun x1 x2 => x1 ^ x2) o
-- Mathlib.Data.Fintype.Vector
Sym.instFinite : ∀ {α : Type u_1} [Finite α] {n : ℕ}, Finite (Sym α n)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.spine_δ₀ : ∀ (X : SSet) {m : ℕ} (x : X.obj (Opposite.op { len := m + 1 })),
  X.spine m ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x) =
    (X.spine (m + 1) x).interval 1 m ⋯
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- A quotient of a finite-dimensional space is also finite-dimensional.  -/
FiniteDimensional.finiteDimensional_quotient : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] (S : Submodule K V), FiniteDimensional K (V ⧸ S)
-- Mathlib.Algebra.Lie.Basic
/-- A bijective morphism of Lie algebras yields an equivalence of Lie algebras.  -/
LieEquiv.ofBijective : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieRing L₂] →
            [inst_3 : LieAlgebra R L₁] →
              [inst_4 : LieAlgebra R L₂] → (f : L₁ →ₗ⁅R⁆ L₂) → Function.Bijective ⇑f → L₁ ≃ₗ⁅R⁆ L₂
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instToStringSyntheticMVarKind : ToString Lean.Elab.Term.SyntheticMVarKind
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- **Alias** of the forward direction of `OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq'`. -/
OpenPartialHomeomorph.IsImage.symm_preimage_eq' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y},
  e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsLoop.ncard_one : ∀ {α : Type u_1} {e : Set α} {H : Hypergraph α}, H.IsLoop e → e.ncard = 1
-- Init.Data.Function
Function.Injective.eq_iff : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ {a b : α}, f a = f b ↔ a = b
-- Lean.Meta.ArgsPacker
/-- Given a telescope of FVars of type `tᵢ`, iterates `PSigma` to produce the type
`t₁ ⊗' t₂ …`.
 -/
Lean.Meta.ArgsPacker.Unary.packType : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.Disjoint
Complementeds.coe_injective : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], Function.Injective Subtype.val
-- Mathlib.GroupTheory.Coset.Basic
orbit_addSubgroup_eq_rightCoset : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α), AddAction.orbit (↥s) a = AddOpposite.op a +ᵥ ↑s
-- Init.Data.SInt.Bitwise
Int8.toInt32_xor : ∀ (a b : Int8), (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
-- Mathlib.Logic.Embedding.Set
/-- Restrict the codomain of an embedding.  -/
Function.Embedding.codRestrict : {α : Sort u_1} → {β : Type u_2} → (p : Set β) → (f : α ↪ β) → (∀ (a : α), f a ∈ p) → α ↪ ↑p
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.mk.injEq : ∀ {α : Type u_6} [T : TopologicalSpace α] (σ : Type u_5) (F : Ctop α σ) (eq : F.toTopsp = T) (σ_1 : Type u_5)
  (F_1 : Ctop α σ_1) (eq_1 : F_1.toTopsp = T),
  ({ σ := σ, F := F, eq := eq } = { σ := σ_1, F := F_1, eq := eq_1 }) = (σ = σ_1 ∧ F ≍ F_1)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.edges_bypass_sublist_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.edges.Sublist p.edges
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `add_apply`. -/
SlashInvariantForm.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Presentation.tensor_var : ∀ {A : Type u} [inst : CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module A M₁] [inst_4 : Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂)
  (x : (pres₁.tensor pres₂.toRelations).G),
  (pres₁.tensor pres₂).var x =
    match x with
    | (g₁, g₂) => pres₁.var g₁ ⊗ₜ[A] pres₂.var g₂
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.instModulePolynomial : {R : Type u_1} → [inst : Semiring R] → Module (Polynomial R) (LaurentPolynomial R)
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.instAddMonoid : {α : Type u_3} →
  [inst : UniformSpace α] → [inst_1 : AddGroup α] → [IsUniformAddGroup α] → AddMonoid (UniformSpace.Completion α)
-- Mathlib.Data.Set.Basic
/-- There is exactly one set of a type that is empty.  -/
Set.uniqueEmpty : {α : Type u} → [IsEmpty α] → Unique (Set α)
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- The complex consisting of only the faces present in both of its arguments.  -/
Geometry.SimplicialComplex.instMin : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] → [inst_3 : Module 𝕜 E] → Min (Geometry.SimplicialComplex 𝕜 E)
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- **Alias** of the reverse direction of `Submodule.linearDisjoint_op`.

---

Linear disjointness is preserved by taking multiplicative opposite.  -/
Submodule.LinearDisjoint.of_op : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  (Submodule.equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (Submodule.equivOpposite.symm (MulOpposite.op M)) →
    M.LinearDisjoint N
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.mk.sizeOf_spec : ∀ (support : Finset ℕ) (prodPrimes : ℕ) (prodPrimes_squarefree : Squarefree prodPrimes) (weights : ℕ → ℝ)
  (weights_nonneg : ∀ (n : ℕ), 0 ≤ weights n) (totalMass : ℝ) (nu : ArithmeticFunction ℝ)
  (nu_mult : nu.IsMultiplicative) (nu_pos_of_prime : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → 0 < nu p)
  (nu_lt_one_of_prime : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → nu p < 1),
  sizeOf
      { support := support, prodPrimes := prodPrimes, prodPrimes_squarefree := prodPrimes_squarefree,
        weights := weights, weights_nonneg := weights_nonneg, totalMass := totalMass, nu := nu, nu_mult := nu_mult,
        nu_pos_of_prime := nu_pos_of_prime, nu_lt_one_of_prime := nu_lt_one_of_prime } =
    1 + sizeOf support + sizeOf prodPrimes + sizeOf totalMass + sizeOf nu + sizeOf nu_mult
-- Mathlib.CategoryTheory.Shift.Pullback
/-- The natural transformation `τ`, seen as a natural transformation from `PullbackShift.functor F φ`
to `PullbackShift.functor G φ`. Then a `CommShift B` instance on `τ` will define a `CommShift A`
instance on `PullbackShift.natTrans τ φ`, and we won't have to juggle with two `CommShift`
instances on `τ`.
 -/
CategoryTheory.PullbackShift.natTrans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) →
                {D : Type u_4} →
                  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] →
                    [inst_5 : CategoryTheory.HasShift D B] →
                      {F G : CategoryTheory.Functor C D} →
                        (F ⟶ G) → (CategoryTheory.PullbackShift.functor φ F ⟶ CategoryTheory.PullbackShift.functor φ G)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.splitAt.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → List α → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        (x_2 : List α) →
          ((x : ℕ) → (x_3 : List α) → motive [] x x_3) →
            ((x : α) → (xs : List α) → (n : ℕ) → (acc : List α) → motive (x :: xs) n.succ acc) →
              ((xs : List α) →
                  (x : ℕ) →
                    (acc : List α) →
                      (xs = [] → False) →
                        (∀ (x_4 : α) (xs_1 : List α) (n : ℕ), xs = x_4 :: xs_1 → x = n.succ → False) →
                          motive xs x acc) →
                motive x x_1 x_2
-- Mathlib.Algebra.Homology.ExactSequence
/-- The isomorphism `S₁.sc _ i ≅ S₂.sc _ i` induced by an isomorphism `S₁ ≅ S₂`
in `ComposableArrows C n`.  -/
CategoryTheory.ComposableArrows.scMapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S₁ S₂ : CategoryTheory.ComposableArrows C n} →
          (S₁ ≅ S₂) →
            (h₁ : S₁.IsComplex) →
              (h₂ : S₂.IsComplex) →
                (i : ℕ) →
                  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.scMapIso._auto_1) →
                    S₁.sc h₁ i hi ≅ S₂.sc h₂ i hi
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_symm_add : ∀ (R : Type u_1) (p m n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  (iterateFrobeniusEquiv R p (m + n)).symm = (iterateFrobeniusEquiv R p n).symm.trans (iterateFrobeniusEquiv R p m).symm
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Makes the identity isomorphism from a proof two non-unital subsemirings of a multiplicative
monoid are equal.  -/
RingEquiv.nonUnitalSubsemiringCongr : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → {s t : NonUnitalSubsemiring R} → s = t → ↥s ≃+* ↥t
-- Init.Data.UInt.Lemmas
UInt32.add_left_neg : ∀ (a : UInt32), -a + a = 0
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.PlausibleStep.yield : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {it' : Std.IterM m β} {out : β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    ∀ (h : it.internalState.countdown ≠ 1),
      Std.Iterators.Types.Take.PlausibleStep it
        (Std.IterStep.yield
          { internalState := { countdown := it.internalState.countdown - 1, inner := it', finite := ⋯ } } out)
-- Aesop.Tree.Data
Aesop.Goal.modify : (Aesop.GoalData Aesop.Rapp Aesop.MVarCluster → Aesop.GoalData Aesop.Rapp Aesop.MVarCluster) → Aesop.Goal → Aesop.Goal
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int32.intCast_neg : ∀ (i : ℤ), ↑(-i) = -↑i
-- Mathlib.Data.List.Sigma
List.lookupAll_cons_eq : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a),
  List.lookupAll a (⟨a, b⟩ :: l) = b :: List.lookupAll a l
-- Init.Data.Vector.Basic
instDecidableEqVector : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → DecidableEq (Vector α n)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.quotientEquiv_symm : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) (x : S), P.quotientEquiv.symm x = (Ideal.Quotient.mk P.ker) (P.σ x)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instNontrivialSubalgebraOfNonempty : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [Nonempty σ] [Nontrivial R],
  Nontrivial (Subalgebra R (MvPowerSeries σ R))
-- Mathlib.Order.RelSeries
LTSeries.length_lt_card : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Fintype α] (s : LTSeries α), s.length < Fintype.card α
-- Init.Data.Vector.Lemmas
Vector.map_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {a a_1 : ℕ} {xs : Vector α (a + a_1)} {ys : Vector β a} {zs : Vector β a_1} {f : α → β},
  Vector.map f xs = ys ++ zs ↔ ∃ as bs, xs = as ++ bs ∧ Vector.map f as = ys ∧ Vector.map f bs = zs
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} [inst_1 : SizeOf C] (val : X.val ⟶ Y.val),
  sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.toQuadraticForm' : ∀ {n : Type u_2} [inst : Fintype n] {R : Type u_5} [inst_1 : CommRing R] [inst_2 : PartialOrder R] [inst_3 : StarRing R]
  [TrivialStar R] [inst_5 : DecidableEq n] {M : Matrix n n R}, M.PosDef → QuadraticMap.PosDef M.toQuadraticForm'
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.sum.eq_1 : ∀ {H : Type u} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'],
  ChartedSpace.sum =
    if h : Nonempty H then ChartedSpace.sumOfNonempty
    else
      have this := ⋯;
      have this_1 := ⋯;
      ChartedSpace.empty H (M ⊕ M')
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapSetEquiv_indep_iff : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) {E : Set β} (e : ↑M.E ≃ ↑E) {I : Set β},
  (M.mapSetEquiv e).Indep I ↔ M.Indep (Subtype.val '' ⇑e.symm '' Subtype.val ⁻¹' I) ∧ I ⊆ E
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.mk'_I : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n))
  (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E)
  (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ),
  (Topology.RelCWComplex.Subcomplex.mk' C E I closedCell_subset union).I n = I n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokens.mk : Option String → Array ℕ → Lean.Lsp.SemanticTokens
-- Aesop.Frontend.RuleExpr
_private.Aesop.Frontend.RuleExpr.0.Aesop.Frontend.RuleConfig.validateForAdditionalRules.getPhaseAndPriority : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → m (Aesop.PhaseName × Aesop.Frontend.Priority)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc : ∀ (X : SemiNormedGrp₁) (Y : SemiNormedGrp₁), AddMonoidHomClass { f // f.NormNoninc } X.carrier Y.carrier
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.subset_preimage_neighborSet : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (v : V) (f : G →g G'),
  G.neighborSet v ⊆ ⇑f ⁻¹' G'.neighborSet (f v)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_twoPow_of_le : ∀ {i w : ℕ}, w ≤ i → (BitVec.twoPow w i).toNat = 0
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_mem : ∀ {σ : Type u_1} {S : Type u_2} {subS : Type u_3} [inst : CommSemiring S] [inst_1 : SetLike subS S]
  [SubsemiringClass subS S] {p : MvPolynomial σ S} {s : subS},
  (∀ i ∈ p.support, MvPolynomial.coeff i p ∈ s) → ∀ {v : σ → S}, (∀ (i : σ), v i ∈ s) → (MvPolynomial.eval v) p ∈ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The scalar multiplication for a Jacobian point representative on a Weierstrass curve.  -/
WeierstrassCurve.Jacobian.instSMulForallFinOfNatNat : {R : Type r} → [CommRing R] → SMul R (Fin 3 → R)
-- Mathlib.Computability.Primrec.Basic
Primrec₂.option_some_iff : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, (Primrec₂ fun a b => some (f a b)) ↔ Primrec₂ f
-- Init.Data.UInt.Lemmas
USize.toUInt8_toUInt64 : ∀ (n : USize), n.toUInt64.toUInt8 = n.toUInt8
-- Mathlib.Algebra.Group.Action.Equidecomp
/-- The inverse function of an equidecomposition as an equidecomposition.  -/
Equidecomp.symm : {X : Type u_1} → {G : Type u_2} → [inst : Group G] → [inst_1 : MulAction G X] → Equidecomp X G → Equidecomp X G
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_left : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) (adj₂ : F ⊣₂ G) (X₁ : CategoryTheory.Arrow C₁)
  [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] [inst_4 : CategoryTheory.Limits.HasPushouts C₃]
  (X₃ : CategoryTheory.Arrow C₃),
  ((CategoryTheory.Functor.LeibnizAdjunction.adj F G adj₂ X₁).counit.app X₃).left =
    CategoryTheory.Limits.pushout.desc
      (adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.id ((G.obj (Opposite.op X₁.right)).obj X₃.left)))
      (adj₂.homEquiv.symm
        (CategoryTheory.Limits.pullback.fst ((G.obj (Opposite.op X₁.left)).map X₃.hom)
          ((G.map X₁.hom.op).app X₃.right)))
      ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.shrink_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (i : ↑E.presieve₀.uncurry), E.shrink.f i = (↑i).snd
-- Mathlib.Analysis.LocallyConvex.WeakSpace
/-- If `e` is a linear isomorphism between two locally convex spaces, and `e` induces (via
precomposition) an isomorphism between their continuous duals, then `e` commutes with the closure
on convex sets.

The hypotheses hold automatically for `e := toWeakSpace 𝕜 E`, see `Convex.toWeakSpace_closure`.  -/
LinearEquiv.image_closure_of_convex' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : Module ℝ E] [IsScalarTower ℝ 𝕜 E] [inst_7 : Module ℝ F]
  [IsScalarTower ℝ 𝕜 F] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] [inst_13 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F]
  [LocallyConvexSpace ℝ F] {s : Set E},
  Convex ℝ s →
    ∀ (e : E ≃ₗ[𝕜] F) (e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E),
      (∀ (f : StrongDual 𝕜 F), ↑(e_dual f) = e.dualMap ↑f) → ⇑e '' closure s = closure (⇑e '' s)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.State.mk : {σ : Type} → σ → Lean.NameSet → Bool → Lean.ScopedEnvExtension.State σ
-- Init.Omega.IntList
Lean.Omega.IntList.sum.eq_1 : ∀ (xs : Lean.Omega.IntList), xs.sum = List.foldr (fun x1 x2 => x1 + x2) 0 xs
-- Mathlib.Data.Vector.Defs
/-- Elimination rule for `Vector`.  -/
List.Vector.elim : {α : Type u_5} →
  {C : {n : ℕ} → List.Vector α n → Sort u} → ((l : List α) → C ⟨l, ⋯⟩) → {n : ℕ} → (v : List.Vector α n) → C v
-- Mathlib.Tactic.Translate.Core
/-- An optional flag stating that the translated declaration already exists.
If this flag is wrong about whether the translated declaration exists, we raise a linter error.
Note: the linter will never raise an error for inductive types and structures.  -/
Mathlib.Tactic.Translate.Config.existing : Mathlib.Tactic.Translate.Config → Bool
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TermElabM.run' : {α : Type} →
  Lean.Elab.TermElabM α → optParam Lean.Elab.Term.Context { } → optParam Lean.Elab.Term.State { } → Lean.MetaM α
-- Mathlib.Analysis.InnerProductSpace.PiL2
Matrix.toLpLin.eq_1 : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  (p q : ENNReal),
  Matrix.toLpLin p q =
    Matrix.toLin'.trans ((WithLp.linearEquiv p R (n → R)).symm.arrowCongr (WithLp.linearEquiv q R (m → R)).symm)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.nonsing_inv_nonsing_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  IsUnit A.det → A⁻¹⁻¹ = A
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_of_one_le : ∀ {x : ℝ}, 1 ≤ x → Real.arccos x = 0
-- Lean.Parser.Basic
Lean.Parser.tokenWithAntiquot : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.lt_pred_iff : ∀ {α : Type u_1} {a b : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  Order.IsPredLimit b → (b < Order.pred a ↔ b < a)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.dvd_of_factorization_pos : ∀ {n p : ℕ}, n.factorization p ≠ 0 → p ∣ n
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.coe_mk' : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R}
  (ha : ↑sa = s), ↑(NonUnitalSubring.mk' s sm sa hm ha) = s
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.pre_pre : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] {L : Type u₃} [inst_5 : CategoryTheory.Category.{v₃, u₃} L]
  (D : CategoryTheory.Functor L K) [h : CategoryTheory.Limits.HasColimit (D.comp (E.comp F))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre (E.comp F) D)
      (CategoryTheory.Limits.colimit.pre F E) =
    CategoryTheory.Limits.colimit.pre F (D.comp E)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight.sizeOf_spec : ∀ (e : Lean.Expr) (f g : Mathlib.Tactic.BicategoryLike.Mor₁) (η : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (h : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e f g η h) =
    1 + sizeOf e + sizeOf f + sizeOf g + sizeOf η + sizeOf h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Init.Data.ByteArray.Basic
/-- Appends two byte arrays using fast array primitives instead of converting them into lists and back.

In compiled code, this function replaces calls to `ByteArray.append`.
 -/
ByteArray.fastAppend : ByteArray → ByteArray → ByteArray