mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Attributes
Lean.EnumAttributes.attrs : {α : Type} → Lean.EnumAttributes α → List Lean.AttributeImpl
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_eq_on_Ico : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  (n : ℕ), ∀ a ∈ Set.Ico (↑n) (↑n + 1), ⌊a⌋₊ = n
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compr₂_comp : ∀ {A : Type u_1} {R : Type u_2} [inst : Semiring A] [inst_1 : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8}
  {Pₗ : Type u_9} {Qₗ : Type u_10} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid Nₗ] [inst_4 : AddCommMonoid Pₗ]
  [inst_5 : AddCommMonoid Qₗ] [inst_6 : Module R Nₗ] [inst_7 : Module R Pₗ] [inst_8 : Module R Qₗ]
  [inst_9 : Module A Pₗ] [inst_10 : SMulCommClass R A Pₗ] {Tₗ : Type u_14} [inst_11 : AddCommMonoid Tₗ]
  [inst_12 : Module R Tₗ] [inst_13 : Module A Tₗ] [inst_14 : Module R A] [inst_15 : Module A M] [inst_16 : Module A Qₗ]
  [inst_17 : SMulCommClass R A Qₗ] [inst_18 : SMulCommClass R A Tₗ] [inst_19 : IsScalarTower R A Qₗ]
  [inst_20 : IsScalarTower R A Pₗ] [inst_21 : IsScalarTower R A Tₗ] (f : M →ₗ[A] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[A] Qₗ)
  (h : Qₗ →ₗ[A] Tₗ), f.compr₂ (h ∘ₗ g) = (f.compr₂ g).compr₂ h
-- Mathlib.NumberTheory.FLT.Basic
not_fermatLastTheoremFor_one : ¬FermatLastTheoremFor 1
-- Mathlib.Algebra.RingQuot
RingQuot.instSMulCommClass : ∀ {R : Type uR} [inst : Semiring R] {S : Type uS} [inst_1 : CommSemiring S] {T : Type uT} (r : R → R → Prop)
  [inst_2 : CommSemiring T] [inst_3 : Algebra S R] [inst_4 : Algebra T R] [SMulCommClass S T R],
  SMulCommClass S T (RingQuot r)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_toClopens : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] (s : TopologicalSpace.CompactOpens α),
  ↑s.toClopens = ↑s
-- Mathlib.Data.Seq.Basic
Stream'.Seq.getLast?_toList : ∀ {α : Type u} (s : Stream'.Seq α) (h : s.Terminates), (s.toList h).getLast? = s.get? (s.length h - 1)
-- Mathlib.Data.Set.Prod
Equiv.piCongrLeft_symm_preimage_univ_pi : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (f : ι' ≃ ι) (t : (i : ι) → Set (α i)),
  (⇑(Equiv.piCongrLeft α f).symm ⁻¹' Set.univ.pi fun i' => t (f i')) = Set.univ.pi t
-- Mathlib.Algebra.Ring.Pointwise.Set
/-- `Set α` has distributive negation if `α` has.  -/
Set.hasDistribNeg : {α : Type u_1} → [inst : Mul α] → [HasDistribNeg α] → HasDistribNeg (Set α)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_mul_X_self_pow_eq_add_of_ne_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} (i : σ) (k : ℕ),
  p ≠ 0 → MvPolynomial.degreeOf i (p * MvPolynomial.X i ^ k) = MvPolynomial.degreeOf i p + k
-- Mathlib.Topology.Bases
Dense.isSeparable_iff : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set α},
  Dense s → (TopologicalSpace.IsSeparable s ↔ TopologicalSpace.SeparableSpace α)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₁_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (a : Fin 2),
  (CategoryTheory.ComposableArrows.mk₁ f).obj a = CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ a
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instBracket : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] →
                          Bracket (LeftInvariantDerivation I G) (LeftInvariantDerivation I G)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalars_id_comp : ∀ {R₁ R₂ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] (f₁₂ : R₁ →+* R₂),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (RingHom.id R₁) f₁₂).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsId R₁).hom (ModuleCat.extendScalars f₁₂))
        (ModuleCat.extendScalars f₁₂).leftUnitor.hom) =
    CategoryTheory.CategoryStruct.id (ModuleCat.extendScalars (f₁₂.comp (RingHom.id R₁)))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.union_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ ∪ m₃).Equiv (m₂ ∪ m₃)
-- Mathlib.Algebra.Ring.Torsion
MonoidHom.map_neg_one : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : Monoid M] [IsMulTorsionFree M] (f : R →* M), f (-1) = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true → Std.Internal.List.getKey? k l = Std.Internal.List.getKey? k' l
-- Mathlib.Analysis.Normed.Module.RCLike.Real
frontier_closedBall' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ),
  frontier (Metric.closedBall x r) = Metric.sphere x r
-- Mathlib.Tactic.Polyrith
/-- The `polyrith` tactic is no longer supported in Mathlib,
because it relied on a defunct external service.

---

Attempts to prove polynomial equality goals through polynomial arithmetic
on the hypotheses (and additional proof terms if the user specifies them).
It proves the goal by generating an appropriate call to the tactic
`linear_combination`. If this call succeeds, the call to `linear_combination`
is suggested to the user.

* `polyrith` will use all relevant hypotheses in the local context.
* `polyrith [t1, t2, t3]` will add proof terms t1, t2, t3 to the local context.
* `polyrith only [h1, h2, h3, t1, t2, t3]` will use only local hypotheses
  `h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

Notes:
* This tactic only works with a working internet connection, since it calls Sage
  using the SageCell web API at <https://sagecell.sagemath.org/>.
  Many thanks to the Sage team and organization for allowing this use.
* This tactic assumes that the user has `curl` available on path.
 -/
Mathlib.Tactic.Polyrith.«tacticPolyrithOnly[_]» : Lean.ParserDescr
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.withReader_ReaderT : ∀ {m : Type u → Type v} {psm : Std.Do.PostShape} {ρ α : Type u} {f : ρ → ρ} {x : ReaderT ρ m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ psm)} [inst : Std.Do.WP m psm],
  ⦃fun r => (Std.Do.wp x).apply (fun a x => Q.1 a r, Q.2) (f r)⦄ MonadWithReaderOf.withReader f x ⦃Q⦄
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.mk : String → Option UInt64 → Option UInt64 → Option String → Option String → Std.Internal.UV.System.PasswdInfo
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
Echelon.Decomposition.L_lowerTriangular : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : LinearOrder m] {n : Type u_2} [inst_2 : LinearOrder n] {R : Type u_3}
  [inst_3 : CommRing R] {A : Matrix m n R} (self : Echelon.Decomposition A), self.L.IsLowerTriangular
-- Init.Data.Int.DivMod.Bootstrap
Int.add_ediv_of_dvd_right : ∀ {a b c : ℤ}, c ∣ b → (a + b) / c = a / c + b / c
-- Mathlib.FieldTheory.IsSepClosed
isSepClosure_iff : ∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra k K],
  IsSepClosure k K ↔ IsSepClosed K ∧ Algebra.IsSeparable k K
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constInsertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (l : List (α × β)), (Std.DTreeMap.Const.insertMany t₁ l).Equiv (Std.DTreeMap.Const.insertMany t₂ l)
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_choose : ∀ (j : ℕ), (fwdDiff 1 fun x => ↑(x.choose (j + 1))) = fun x => ↑(x.choose j)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.isoOfLE.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hUV : U ≤ V),
  AlgebraicGeometry.Scheme.Opens.isoOfLE hUV =
    AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq
      (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι V.ι) U.ι ⋯
-- Mathlib.Algebra.Lie.Extension
/-- The bundled `LieAlgebra.Extension` corresponding to `LieAlgebra.IsExtension`  -/
LieAlgebra.IsExtension.extension : {R : Type u_1} →
  {N : Type u_2} →
    {L : Type u_3} →
      {M : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : LieRing N] →
                [inst_4 : LieAlgebra R N] →
                  [inst_5 : LieRing M] →
                    [inst_6 : LieAlgebra R M] →
                      {i : N →ₗ⁅R⁆ L} → {p : L →ₗ⁅R⁆ M} → LieAlgebra.IsExtension i p → LieAlgebra.Extension R N M
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.lctx : Lean.Elab.InlayHint → Lean.LocalContext
-- Mathlib.Data.Sym.Sym2
Sym2.filter_image_mk_not_isDiag : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α),
  {x ∈ Finset.image (Function.uncurry Sym2.mk) (s ×ˢ s) | ¬x.IsDiag} = Finset.image (Function.uncurry Sym2.mk) s.offDiag
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.le_one_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : Associates M}, p ≤ 1 ↔ p = 1
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.mono : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {f : ℝ → X} {a b c d : ℝ},
  AbsolutelyContinuousOnInterval f a b → Set.uIcc c d ⊆ Set.uIcc a b → AbsolutelyContinuousOnInterval f c d
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.top_lowerCentralSeries_one`. -/
lowerCentralSeries_one : ∀ {G : Type u_1} [inst : Group G], ⊤.lowerCentralSeries 1 = commutator G
-- Mathlib.Topology.FiberBundle.Basic
/-- Local homeomorphism version of the trivialization change.  -/
FiberBundleCore.trivChange : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → ι → ι → OpenPartialHomeomorph (B × F) (B × F)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.toList.eq_1 : ∀ {α : Type u_1} {cmp : α → α → Ordering} (t : RBTree.RBSet α cmp), t.toList = (↑t).toList
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- **Alias** of `Submonoid.coe_finsetProd`. -/
Submonoid.coe_finset_prod : ∀ {ι : Type u_4} {M : Type u_5} [inst : CommMonoid M] (S : Submonoid M) (f : ι → ↥S) (s : Finset ι),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.retractClosure_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C)
  [Q.IsStableUnderRetracts], P.retractClosure ≤ Q ↔ P ≤ Q
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_tryCatch_ExceptT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ (ε → Pred) EPred} (x : ExceptT ε m α) (h : ε → ExceptT ε m α),
  Lean.Order.PartialOrder.rel
    (Std.Internal.Do.wp x post (EPost.Cons.mk✝ (fun e => Std.Internal.Do.wp (h e) post epost) epost.tail))
    (Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost)
-- Init.Prelude
/-- `a ++ b` is the result of concatenation of `a` and `b`, usually read "append".
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `++` in identifiers is `append`. -/
HAppend.hAppend : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAppend α β γ] → α → β → γ
-- Lean.Meta.Tactic.Assert
Lean.Meta.AssertAfterResult.mvarId : Lean.Meta.AssertAfterResult → Lean.MVarId
-- Lean.Elab.Attributes
/-- ```
attrKind := leading_parser optional («scoped» <|> «local»)
```
 -/
Lean.Elab.toAttributeKind : Lean.Syntax → Lean.MacroM Lean.AttributeKind
-- Mathlib.CategoryTheory.Abelian.Exact
/-- A functor preserving zero morphisms, epis, and kernels preserves homology.  -/
CategoryTheory.Functor.preservesHomology_of_preservesEpis_and_kernels : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Abelian A] [inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B)
  [inst_4 : L.PreservesZeroMorphisms] [L.PreservesEpimorphisms]
  [∀ {X Y : A} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) L],
  L.PreservesHomology
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.NatTrans.mapElements.hcongr_5 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (F : CategoryTheory.Functor C (Type w)) (F' : CategoryTheory.Functor C' (Type w)),
          F ≍ F' →
            ∀ (G : CategoryTheory.Functor C (Type w)) (G' : CategoryTheory.Functor C' (Type w)),
              G ≍ G' →
                ∀ (φ : F ⟶ G) (φ' : F' ⟶ G'),
                  φ ≍ φ' → CategoryTheory.NatTrans.mapElements φ ≍ CategoryTheory.NatTrans.mapElements φ'
-- Mathlib.RingTheory.Ideal.Operations
Ideal.prod_le_inf : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {s : Finset ι} {f : ι → Ideal R}, s.prod f ≤ s.inf f
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Unlike `HasFDerivAt.finsetProd`, supports non-commutative multiply and duplicate elements.
 -/
HasFDerivAt.list_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸 : Type u_6} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E},
  (∀ i ∈ l, HasFDerivAt (fun x => f i x) (f' i) x) →
    HasFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod)
      (∑ i,
        (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod •
          MulOpposite.op (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod • f' l[i])
      x
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
/-- **Alias** of `TensorProduct.directSumRight`.

---

Tensor products distribute over a direct sum on the right.  -/
TensorProduct.directSumRight' : (R : Type u) →
  [inst : CommSemiring R] →
    (S : Type u_1) →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {ι₂ : Type v₂} →
            [DecidableEq ι₂] →
              (M₁' : Type w₁') →
                (M₂ : ι₂ → Type w₂) →
                  [inst_4 : AddCommMonoid M₁'] →
                    [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] →
                      [inst_6 : Module R M₁'] →
                        [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)] →
                          [inst_8 : Module S M₁'] →
                            [inst_9 : IsScalarTower R S M₁'] →
                              TensorProduct R M₁' (DirectSum ι₂ fun i => M₂ i) ≃ₗ[S]
                                DirectSum ι₂ fun i => TensorProduct R M₁' (M₂ i)
-- Std.Data.TreeSet.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.empty : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp
-- Lean.Meta.Match.Match
Lean.Meta.Match.State : Type
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_set_eq_iInter : ∀ {α : Type u_2} {β : Type u_3} (s : Finset α) (f : α → Set β), s.inf f = ⋂ x ∈ s, f x
-- Init.Data.BitVec.Basic
BitVec.shiftLeft_eq : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), x.shiftLeft n = x <<< n
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- Adding a one-form taking values in the endomorphisms of the vector bundle to a covariant
derivative gives a covariant derivative.  -/
CovariantDerivative.addOneForm : {𝕜 : 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_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            CovariantDerivative I F V →
                                              ((x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x) →
                                                CovariantDerivative I F V
-- Mathlib.Data.Finset.Lattice.Fold
Finset.isGLB_inf' : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Finset α} (hs : s.Nonempty), IsGLB (↑s) (s.inf' hs id)
-- Mathlib.RingTheory.Morita.Basic
IsMoritaEquivalent.refl : ∀ (R : Type u₀) [inst : CommSemiring R] (A : Type u₁) [inst_1 : Ring A] [inst_2 : Algebra R A], IsMoritaEquivalent R A A
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- The regularized hypergeometric series.  -/
Complex.regularizedHGFunSeries : Multiset ℂ → Multiset ℂ → FormalMultilinearSeries ℂ ℂ ℂ
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.liesOver_conjugate_extensionEmbedding : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [inst_3 : Algebra v.Completion w.Completion]
  [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion]
  [NumberField.ComplexEmbedding.LiesOver (NumberField.ComplexEmbedding.conjugate w.embedding) v.embedding],
  NumberField.ComplexEmbedding.LiesOver
    (NumberField.ComplexEmbedding.conjugate (NumberField.InfinitePlace.Completion.extensionEmbedding w))
    (NumberField.InfinitePlace.Completion.extensionEmbedding v)
-- Mathlib.Computability.DFA
DFA.evalFrom_of_append : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (x y : List α),
  M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A version of `QuadraticMap.associated_left_inverse` for general targets.  -/
QuadraticMap.associated_left_inverse' : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] {B₁ : LinearMap.BilinMap R M N},
  LinearMap.flip B₁ = B₁ → (QuadraticMap.associatedHom S) B₁.toQuadraticMap = B₁
-- Mathlib.RingTheory.Norm.Defs
Algebra.norm_eq_matrix_det : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {ι : Type w}
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R S) (s : S),
  (Algebra.norm R) s = ((Algebra.leftMulMatrix b) s).det
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.inv_image_trans_target : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  ↑e'.symm '' (e.trans e').target = e'.source ∩ e.target
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDivisionMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionMonoid α],
  Lex.instDivisionMonoid =
    { toDivInvMonoid := Lex.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.instPow : {M : Type uM} → {N : Type uN} → [inst : MulOneClass M] → [inst_1 : CommMonoid N] → Pow (M →* N) ℕ
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Option.merge.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Option α → Sort u_2) →
    (x x_1 : Option α) →
      (Unit → motive none none) →
        ((x : α) → motive (some x) none) →
          ((y : α) → motive none (some y)) → ((x y : α) → motive (some x) (some y)) → motive x x_1
-- Mathlib.CategoryTheory.Core
CategoryTheory.CoreHom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : CategoryTheory.Core C} {iso iso_1 : X.of ≅ Y.of},
  { iso := iso } = { iso := iso_1 } → iso = iso_1
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instMinOfSemilatticeInf : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [SemilatticeInf Y] → [inst_2 : Zero Y] → Min (Function.locallyFinsuppWithin U Y)
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_rco : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_rco._auto_1) [Std.TransCmp cmp]
  {t : Std.DTreeMap α β cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
    List.filter (fun e => decide ((cmp e.fst lowerBound).isGE = true ∧ (cmp e.fst upperBound).isLT = true)) t.toList
-- Init.Data.Vector.Lemmas
Vector.replace_empty : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, #v[].replace a b = #v[]
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.iso_w' : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g),
  g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left e.inv)
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Arrow.Hom.right e.hom))
-- Mathlib.SetTheory.Cardinal.NatCard
Set.card_union_le : ∀ {α : Type u_1} (s t : Set α), Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
-- Mathlib.Order.SetNotation
/-- Indexed supremum.  -/
«term⨆_,_» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List (α × β)}
  {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Internal.Impl.Const.get?
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)) k =
      none
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_neg_index : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] [inst_2 : DecidableEq ι]
  [inst_3 : InvolutiveNeg ι] (s : Finset ι) (f : ι → M), ((-s).expect fun i => f i) = s.expect fun i => f (-i)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Generate the smallest sieve containing the given presieve.  -/
CategoryTheory.Sieve.generate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Presieve X → CategoryTheory.Sieve X
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
ContDiffAt.mem_toOpenPartialHomeomorph_source : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕂 E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕂 F] [inst_5 : CompleteSpace E] {f : E → F}
  {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0),
  a ∈ (ContDiffAt.toOpenPartialHomeomorph f hf hf' hn).source
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.valuesArray.eq_1 : ∀ {α : Type u} {β : Type v} (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.valuesArray = Std.DTreeMap.Internal.Impl.foldl (fun l x v => l.push v) (Array.emptyWithCapacity t.size) t