mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiable.clm_prodMap : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_17}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄},
  MDiff g → MDiff f → MDiff fun x => (g x).prodMap (f x)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- An induction principle for closure membership for predicates with two arguments.  -/
Subsemigroup.closure_induction₂ : ∀ {M : Type u_1} [inst : Mul M] {s : Set M}
  {p : (x y : M) → x ∈ Subsemigroup.closure s → y ∈ Subsemigroup.closure s → Prop},
  (∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (x y z : M) (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s)
        (hz : z ∈ Subsemigroup.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
      (∀ (x y z : M) (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s)
          (hz : z ∈ Subsemigroup.closure s), p z x hz hx → p z y hz hy → p z (x * y) hz ⋯) →
        ∀ {x y : M} (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s), p x y hx hy
-- Mathlib.Control.Basic
/-- Attempts to perform the computation, but fails silently if it doesn't succeed.  -/
tryM : {F : Type → Type v} → [Alternative F] → {α : Type} → F α → F Unit
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Merge the contents of two heaps.  -/
Batteries.BinomialHeap.merge : {α : Type u} →
  {le : α → α → Bool} → Batteries.BinomialHeap α le → Batteries.BinomialHeap α le → Batteries.BinomialHeap α le
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_source' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  (e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_intCast_mul_add : ∀ {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) = m + toIocDiv hp a b
-- Mathlib.Algebra.Group.InjSurj
/-- A type has left-cancellative multiplication, if it admits an injective map that
preserves `*` to another type with left-cancellative multiplication.  -/
Function.Injective.isLeftCancelMul : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : Mul M₂] [IsLeftCancelMul M₂] (f : M₁ → M₂),
  Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → IsLeftCancelMul M₁
-- Mathlib.Topology.Instances.Matrix
summable_matrix_diagonal : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [inst_2 : DecidableEq n] {f : X → n → R},
  Summable (fun x => Matrix.diagonal (f x)) L ↔ Summable f L
-- Lean.Elab.Tactic.Grind.Basic
/-- Like `throwError`, but, if recovery is enabled, logs the error instead.
 -/
Lean.Elab.Tactic.Grind.throwOrLogError : Lean.MessageData → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.Topology.EMetricSpace.Defs
instEMetricSpaceOrderDual : {X : Type u_1} → [EMetricSpace X] → EMetricSpace Xᵒᵈ
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.ext_elem : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [Finite ι] {q₁ q₂ : P},
  (∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂) → q₁ = q₂
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- To check that `HD` is continuous, we check that it is Lipschitz. As `HD` is a max, we
prove separately inequalities controlling the two terms (relying too heavily on copy-paste...)  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.HD_lipschitz_aux1 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty X] [Nonempty Y]
  (f g : GromovHausdorff.Cb✝ X Y), ⨆ x, ⨅ y, f (Sum.inl x, Sum.inr y) ≤ (⨆ x, ⨅ y, g (Sum.inl x, Sum.inr y)) + dist f g
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.EIsoH.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂), X.EIsoH f n₀ n₁ n₂ hn₁ hn₂ = (X.homologyDataIdId f n₀ n₁ n₂ ⋯ ⋯).left.homologyIso
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.addSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M),
  ↑c = { carrier := {x | c x.1 x.2}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Algebra.Lie.Solvable
/-- Given a solvable Lie ideal `I` with derived series `I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥`, this is the
`k-1`th term in the derived series (and is therefore an Abelian ideal contained in `I`).

For a non-solvable ideal, this is the zero ideal, `⊥`.  -/
LieAlgebra.derivedAbelianOfIdeal : {R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieIdeal R L → LieIdeal R L
-- Mathlib.GroupTheory.Coset.Basic
leftAddCoset_rightAddCoset : ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α), AddOpposite.op b +ᵥ a +ᵥ s = a +ᵥ AddOpposite.op b +ᵥ s
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} {R : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X},
  CategoryTheory.Presieve.map F R f ↔
    ∃ Z, ∃ (h : F.obj Z = Y), ∃ g, R g ∧ F.map g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.proved.sizeOf_spec : ∀ (newRapps : Array Aesop.RappRef), sizeOf (Aesop.SafeRulesResult.proved newRapps) = 1 + sizeOf newRapps
-- Mathlib.LinearAlgebra.LinearPMap
LinearMap.toPMap_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ[σ] F)
  (p : Submodule R E) (x : ↥p), ↑(f.toPMap p) x = f ↑x
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Context.mk : Mathlib.Meta.FunProp.Config →
  Std.TreeSet Lean.Name Lean.Name.quickCmp →
    (Lean.Expr → Lean.MetaM (Option Lean.Expr)) → ℕ → Mathlib.Meta.FunProp.Context
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.of_forall_getElem?_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [LawfulBEq α],
  (∀ (k : α), m₁[k]? = m₂[k]?) → m₁.Equiv m₂
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
_private.Mathlib.AlgebraicGeometry.Morphisms.Flat.0.CategoryTheory.Pairwise.diagramMap.match_1.eq_3 : ∀ {ι : Type u_1} (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) (i j : ι)
  (h_1 :
    (i : ι) →
      motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.id_single i))
  (h_2 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
        (CategoryTheory.Pairwise.Hom.id_pair i j))
  (h_3 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.left i j))
  (h_4 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
        (CategoryTheory.Pairwise.Hom.right i j)),
  (match CategoryTheory.Pairwise.pair i j, CategoryTheory.Pairwise.single i, CategoryTheory.Pairwise.Hom.left i j with
    | .(CategoryTheory.Pairwise.single i), .(CategoryTheory.Pairwise.single i),
      CategoryTheory.Pairwise.Hom.id_single i => h_1 i
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.pair i j),
      CategoryTheory.Pairwise.Hom.id_pair i j => h_2 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single i), CategoryTheory.Pairwise.Hom.left i j =>
      h_3 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single j), CategoryTheory.Pairwise.Hom.right i j =>
      h_4 i j) =
    h_3 i j
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.integral_sesq_fourier_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℂ F] {G : Type u_5}
  [inst_9 : NormedAddCommGroup G] [inst_10 : NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E)
  (g : SchwartzMap V F) (M : E →L⋆[ℂ] F →L[ℂ] G),
  ∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransformInv.fourierInv g) x)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.le_stdPart_of_le : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ},
  0 ≤ ArchimedeanClass.mk x → f r ≤ x → r ≤ ArchimedeanClass.stdPart x
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionObj`, the action of `C` on `D`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊙ₗ_» : Lean.TrailingParserDescr
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.cmpEq.RootOrdered_congr : ∀ {α : Type u_1} {a b : α} {cmp : α → α → Ordering},
  RBTree.RBNode.cmpEq cmp a b →
    ∀ {t : RBTree.RBNode.Path α}, RBTree.RBNode.Path.RootOrdered cmp t a ↔ RBTree.RBNode.Path.RootOrdered cmp t b
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.trans : ∀ {a o o' : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}},
  a.IsFundamentalSequence o f →
    ∀ {g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}} (hg : o.IsFundamentalSequence o' g),
      a.IsFundamentalSequence o' fun i hi => f (g i hi) ⋯
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.HasLeftDerivedFunctor.hasRightKanExtension : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [L.IsLocalization W] [F.HasLeftDerivedFunctor W], L.HasRightKanExtension F
-- Mathlib.Data.ZMod.Units
ZMod.coe_int_mul_val_inv : ∀ {n : ℕ} [NeZero n] {m : ℤ}, IsCoprime m ↑n → ↑m * ↑(↑m)⁻¹.val = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.pointEquiv_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {x y : R} (h : W'.Equation x y),
  W'.pointEquiv (WeierstrassCurve.Affine.Point.mk h) = some ⟨(x, y), h⟩
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.ExceptT.bindCont.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instCharZero_1 : ∀ (K : Type u_1) [inst : Field K] [CharZero K], CharZero (NumberField.RingOfIntegers K)
-- Mathlib.RingTheory.LinearDisjoint
/-- The image of `R` in `S` is linearly disjoint with any other subalgebras.  -/
Subalgebra.LinearDisjoint.bot_right : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (A : Subalgebra R S),
  A.LinearDisjoint ⊥
-- Mathlib.Order.DirSupClosed
/-- **Alias** of the reverse direction of `dirSupClosed_compl`. -/
DirSupInacc.compl : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], DirSupInacc s → DirSupClosed sᶜ
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiable_prod_iff : ∀ {𝕜 : 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'] {F' : Type u_14}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_15} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  (f : M → M' × N'), MDiff f ↔ MDiff (Prod.fst ∘ f) ∧ MDiff (Prod.snd ∘ f)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.ofHom_id : ∀ {R : Type u} [inst : Ring R], RingCat.ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (RingCat.of R)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_congr_of_strictMono : ∀ {α γ : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder γ] {f : α → γ},
  StrictMono f → IsCofinal (Set.range f) → Order.cof α = Order.cof γ
-- Mathlib.Data.Sym.Sym2
Sym2.mk_eq_mk_iff : ∀ {α : Type u_1} {p q : α × α}, s(p.1, p.2) = s(q.1, q.2) ↔ p = q ∨ p = q.swap
-- Mathlib.Algebra.BigOperators.Finprod
finprod_nonneg : ∀ {α : Sort u_4} {R : Type u_7} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f : α → R}, (∀ (x : α), 0 ≤ f x) → 0 ≤ ∏ᶠ (x : α), f x
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_δ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (i j : M)
  (X : C) [inst_3 : F.Monoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F i j).app X)
      ((CategoryTheory.Functor.OplaxMonoidal.δ F i j).app X) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj i) (F.obj j)).obj X)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.rotateR.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll Std.DTreeMap.Internal.Impl.leaf r =
    if Std.DTreeMap.Internal.Impl.leaf.size < Std.DTreeMap.Internal.ratio * ll.size then
      Std.DTreeMap.Internal.Impl.singleR k v lk lv ll Std.DTreeMap.Internal.Impl.leaf r
    else Std.DTreeMap.Internal.Impl.singleR k v lk lv ll Std.DTreeMap.Internal.Impl.leaf r
-- Mathlib.GroupTheory.OrderOfElement
/-- If `gcd(|G|,n)=1` then the smul by `n` is a bijection  -/
nsmulCoprime : {n : ℕ} → {G : Type u_6} → [AddGroup G] → (Nat.card G).Coprime n → G ≃ G
-- Mathlib.Control.ULift
ULift.bind_up : ∀ {α : Type u} {β : Type v} (a : α) (f : α → ULift.{u_1, v} β), { down := a }.bind f = f a
-- Aesop.Rule
Aesop.NormSimpRule.mk.injEq : ∀ (name : Aesop.RuleName) (entries : Array Lean.Meta.SimpEntry) (name_1 : Aesop.RuleName)
  (entries_1 : Array Lean.Meta.SimpEntry),
  ({ name := name, entries := entries } = { name := name_1, entries := entries_1 }) =
    (name = name_1 ∧ entries = entries_1)
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.autf8EncodeChar_flatMap_ascii : ∀ {a : List UInt8}, (∀ x ∈ a, x < 128) → List.flatMap (fun a => String.utf8EncodeChar (Char.ofUInt8 a)) a = a
-- Mathlib.Algebra.Group.Units.Basic
Units.eq_inv_mul_iff_mul_eq : ∀ {α : Type u} [inst : Monoid α] (b : αˣ) {a c : α}, a = ↑b⁻¹ * c ↔ ↑b * a = c
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.IsFiltered.final_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFiltered D], (CategoryTheory.Prod.fst C D).Final
-- Init.Data.Vector.Lemmas
Vector.finIdxOf?_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {a : α} {xs : Vector α n},
  xs.toArray.finIdxOf? a = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)
-- Mathlib.Analysis.RCLike.Basic
/-- A mixin over a normed field, saying that the norm field structure is the same as `ℝ` or `ℂ`.
To endow such a field with a compatible `RCLike` structure in a proof, use
`letI := IsRCLikeNormedField.rclike 𝕜`.  -/
IsRCLikeNormedField : (𝕜 : Type u_3) → [hk : NormedField 𝕜] → Prop
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.noConfusionType : Sort v✝ → Lean.Meta.SplitKind → Lean.Meta.SplitKind → Sort v✝
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- Typecheck a `QuadraticForm.Isometry` as a morphism in `Module R`.  -/
QuadraticModuleCat.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : AddCommGroup X] →
        [inst_2 : Module R X] →
          [inst_3 : AddCommGroup Y] →
            [inst_4 : Module R Y] →
              {Q₁ : QuadraticForm R X} →
                {Q₂ : QuadraticForm R Y} → (Q₁ →qᵢ Q₂) → (QuadraticModuleCat.of Q₁ ⟶ QuadraticModuleCat.of Q₂)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.size_shrink_loop : ∀ {α : Type u_1} {xs : Array α} {n : ℕ}, (Array.shrink.loop✝ n xs).size = xs.size - n
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The vertices of `C` on which `S` has non-trivial isotropy  -/
CategoryTheory.Subgroupoid.objs : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → Set C
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.comp_add : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] (g : N →+ P) (f₁ f₂ : M →+ N), g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter.mk : Option Lean.Expr → Option Lean.Expr → ℕ → Bool → Mathlib.Linter.UnusedInstancesInType.Parameter✝
-- Mathlib.Data.FunLike.Equiv
EquivLike.apply_eq_iff_eq : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] (f : E) {x y : α}, f x = f y ↔ x = y
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Interpret a `RingHom` `f` as an `f`-semilinear map.  -/
RingHom.toSemilinearMap : {R : Type u_1} → {S : Type u_5} → [inst : Semiring R] → [inst_1 : Semiring S] → (f : R →+* S) → R →ₛₗ[f] S
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.toList_ne_nil : ∀ {p : DyckWord}, ↑p ≠ [] ↔ p ≠ 0
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.mk_surjective : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  Function.Surjective ⇑Matrix.ProjGenLinGroup.mk
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A], Function.Injective CategoryTheory.MonoidalClosed.curry
-- Init.Data.Order.Ord
Fin.instLawfulEqOrd : ∀ (n : ℕ), Std.LawfulEqOrd (Fin n)
-- Init.Data.List.Basic
List.length_replicate : ∀ {α : Type u} {n : ℕ} {a : α}, (List.replicate n a).length = n
-- Lean.Environment
/-- Sets `Environment.isExporting` to the given value while executing `x`. No-op if
`EnvironmentHeader.isModule` is false.
 -/
Lean.withExporting : {m : Type → Type} →
  {α : Type} → [Monad m] → [Lean.MonadEnv m] → [MonadFinally m] → [Lean.MonadOptions m] → m α → optParam Bool true → m α
-- Mathlib.Topology.Order.HullKernel
PrimitiveSpectrum.closedsGC_closureOperator : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α} [inst_1 : TopologicalSpace α] [Topology.IsLower α],
  (∀ p ∈ T, InfPrime p) →
    PrimitiveSpectrum.OrderGenerates T →
      ∀ (S : Set ↑T), ⋯.closureOperator S = PrimitiveSpectrum.hull T (PrimitiveSpectrum.kernel S)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_sub_iff : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c d : α},
  a - b < c - d ↔ a + d < c + b
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isPathConnected_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ},
  0 ≤ r → IsPathConnected (Metric.closedBall x r)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_last : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc),
  Fin.snoc p x (Fin.last n) = x
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.instEncodableSubtypeAddOppositeMemOp.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : Encodable ↥H],
  H.instEncodableSubtypeAddOppositeMemOp = Encodable.ofEquiv (↥H) H.equivOp.symm
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.toList_flatMapAfterM.match_1.splitter : {α₂ γ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Option (Std.IterM m γ) → Sort u_3) →
      (it₂ : Option (Std.IterM m γ)) → (Unit → motive none) → ((it₂ : Std.IterM m γ) → motive (some it₂)) → motive it₂
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.arrayLit.inj : ∀ {type : Lean.Expr} {xs : List Lean.Meta.Match.Pattern} {type_1 : Lean.Expr} {xs_1 : List Lean.Meta.Match.Pattern},
  Lean.Meta.Match.Pattern.arrayLit type xs = Lean.Meta.Match.Pattern.arrayLit type_1 xs_1 → type = type_1 ∧ xs = xs_1
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.weak_left : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α}, t.Bounded o₁ o₂ → t.Bounded ⊥ o₂
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_map_eq_self_of_injective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Injective ⇑f → ∀ (H : AddSubgroup G), AddSubgroup.comap f (AddSubgroup.map f H) = H
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The proposition that a sesquilinear map is reflexive  -/
LinearMap.IsRefl : {R : Type u_1} →
  {R₁ : Type u_2} →
    {M : Type u_5} →
      {M₁ : Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : CommSemiring R₁] →
                [inst_4 : AddCommMonoid M₁] →
                  [inst_5 : Module R₁ M₁] → {I₁ I₂ : R₁ →+* R} → (M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M) → Prop