mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.MemSobolev.neg : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)]
  {f : TemperedDistribution E F}, TemperedDistribution.MemSobolev s p f → TemperedDistribution.MemSobolev s p (-f)
-- Mathlib.RingTheory.Derivation.ToSquareZero
diffToIdealOfQuotientCompEq_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B) (f₁ f₂ : A →ₐ[R] B)
  (e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂) (x : A),
  ↑((diffToIdealOfQuotientCompEq I f₁ f₂ e) x) = f₁ x - f₂ x
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_smul_action : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (r : R),
  LinearMap.rTensor M (DistribSMul.toLinearMap R N r) = DistribSMul.toLinearMap R (TensorProduct R N M) r
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sum_sum' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι}
  [MeasureTheory.IsFiniteMeasure μ] {ι' : Type u_3} {Y : ι' → Ω → ℝ} {t : Finset ι'},
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    (∀ i ∈ t, MeasureTheory.MemLp (Y i) 2 μ) →
      ProbabilityTheory.covariance (∑ i ∈ s, X i) (∑ j ∈ t, Y j) μ =
        ∑ i ∈ s, ∑ j ∈ t, ProbabilityTheory.covariance (X i) (Y j) μ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.compl_add : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [ContinuousAdd α]
  {s : Set β}, Summable (f ∘ Subtype.val) → Summable (f ∘ Subtype.val) → Summable f
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_comp : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)]
  (g : (i : ι) → t i →ₗ[R] t' i) (f : (i : ι) → s i →ₗ[R] t i),
  (PiTensorProduct.map fun i => g i ∘ₗ f i) = PiTensorProduct.map g ∘ₗ PiTensorProduct.map f
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.ExtendScalars.instLieRingModule : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      (M : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : Algebra R A] →
              [inst_3 : LieRing L] →
                [inst_4 : LieAlgebra R L] →
                  [inst_5 : AddCommGroup M] →
                    [inst_6 : Module R M] →
                      [inst_7 : LieRingModule L M] →
                        [LieModule R L M] → LieRingModule (TensorProduct R A L) (TensorProduct R A M)
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.IsZeroAt.eq_1 : ∀ (c : OnePoint ℝ) (f : UpperHalfPlane → ℂ) (k : ℤ),
  c.IsZeroAt f k = ∀ (g : GL (Fin 2) ℝ), g • OnePoint.infty = c → UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k g f)
-- Init.Omega.Int
Lean.Omega.Int.le_of_ge : ∀ {x y : ℤ}, x ≥ y → y ≤ x
-- Std.Http.Protocol.H1.Reader
/-- Checks if the reader has completed parsing the current message.
 -/
Std.Http.Protocol.H1.Reader.isComplete : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
            P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3 →
              W.dblXYZ P =
                W.dblZ P •
                  ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                      (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                    W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                      (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                    1]
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_addNat_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (fun x => x.addNat m) (Finset.Ioc i j) = Finset.Ioc (i.addNat m) (j.addNat m)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.iff_flat_and_ideal_smul_eq_top : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔ Module.Flat R M ∧ ∀ (I : Ideal R), I • ⊤ = ⊤ → I = ⊤
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Triangle inequality** for the norm.  -/
norm_mul_le' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a * b‖ ≤ ‖a‖ + ‖b‖
-- Mathlib.RingTheory.Flat.Basic
/-- If `A`, `B` are `R`-algebras, `R` injects into `A`,
and `B` is a nontrivial flat `R`-algebra, then `A ⊗[R] B` is nontrivial.  -/
Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_right : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) (B : Type u_3) [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  Function.Injective ⇑(algebraMap R A) → ∀ [Module.Flat R B] [Nontrivial B], Nontrivial (TensorProduct R A B)
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableOn.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {H : Type u_5} [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G},
  DifferentiableOn 𝕜 c s → DifferentiableOn 𝕜 d s → DifferentiableOn 𝕜 (fun y => c y ∘SL d y) s
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The `j`-th projection from the pullback.  -/
CategoryTheory.Limits.WidePullback.π : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {B : C} →
        {objs : J → C} →
          (arrows : (j : J) → objs j ⟶ B) →
            [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] →
              (j : J) → CategoryTheory.Limits.widePullback B objs arrows ⟶ objs j
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_sub_add_cancel : ∀ (a b c : Ordinal.{u_4}), a + b - (a + c) = b - c
-- Mathlib.NumberTheory.FunctionField
/-- Let `K` be a function field over `F`. If `E` is an algebraic extension of `F` which is
contained in `K` then it is finite over `F`.  -/
FunctionField.finiteDimensional_of_constantExtension : ∀ {F : Type u_1} (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : FaithfulSMul (Polynomial F) K] [FunctionField F K] {E : Type u_3} [inst_5 : Field E] [inst_6 : Algebra F E]
  [inst_7 : Algebra (Polynomial E) K] [FaithfulSMul (Polynomial E) K] [IsScalarTower (Polynomial F) (Polynomial E) K]
  [Algebra.IsAlgebraic F E], FiniteDimensional F E
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.iselect_cons : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (ps : PFunctor.Approx.Path F) {a : F.A}
  (f : F.B a → F.M) {i : F.B a}, PFunctor.M.iselect (⟨a, i⟩ :: ps) (PFunctor.M.mk ⟨a, f⟩) = PFunctor.M.iselect ps (f i)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Formula for `sinZeta` as a Dirichlet series in the convergence range, with sum over `ℤ`.  -/
HurwitzZeta.hasSum_int_sinZeta : ∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum (fun n => -Complex.I * ↑n.sign * Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2)
      (HurwitzZeta.sinZeta (↑a) s)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.congr_inv.inj : ∀ {R : Type u} {inst : Rack R} {a a' : Rack.PreEnvelGroup R} {ha ha_1 : Rack.PreEnvelGroupRel' R a a'},
  ha.congr_inv = ha_1.congr_inv → ha = ha_1
-- Mathlib.Topology.Algebra.UniformField
Subfield.completableTopField : ∀ (L : Type u_2) [inst : Field L] [inst_1 : UniformSpace L] [CompletableTopField L] (K : Subfield L),
  CompletableTopField ↥K
-- Mathlib.Tactic.Widget.GCongr
/-- Return the link text and inserted text above and below of the gcongr widget.  -/
makeGCongrString : Array Lean.SubExpr.GoalsLocation →
  Lean.Expr → SelectInsertParams → Lean.MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw))
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_hom_comp_biproduct_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C) (j : J)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) h
-- Lean.Server.References
Lean.Server.instInhabitedReferences.default : Lean.Server.References
-- Mathlib.Order.Booleanisation
Booleanisation.comp_inf_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.comp a ⊓ Booleanisation.lift b = Booleanisation.lift (b \ a)
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EIO.bind_eq_EST_bind : ∀ {ε α β : Type} (ma : EIO ε α) (f : α → EIO ε β), ma >>= f = EST.bind ma f
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.uniformContinuous_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun x => x.1 ×ˢ x.2
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_sup_right : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S T : StarSubalgebra R A} {x : A},
  x ∈ T → x ∈ S ⊔ T
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
IsClosed.analyticSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PolishSpace α] {s : Set α}, IsClosed s → MeasureTheory.AnalyticSet s
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- Given `X : SpectralObject C ι` and `data : SpectralSequenceDataCore ι c r₀`, this is
the property which allows to construct a spectral sequence by using the recipe given
by `data`. The conditions given allow to show that the homology of a page identifies
to the next page.  -/
CategoryTheory.Abelian.SpectralObject.HasSpectralSequence : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            {c : ℤ → ComplexShape κ} →
              {r₀ : ℤ} →
                CategoryTheory.Abelian.SpectralObject C ι →
                  CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.sup_range_r_range_b : ∀ {X Y : SSet} (i : X ⟶ Y) (d : ℕ),
  SSet.Subcomplex.range (SSet.relativeCellComplexOfMono.r i d) ⊔
      SSet.Subcomplex.range (SSet.relativeCellComplexOfMono.b i d) =
    ⊤
-- Init.Data.Order.Classes
Std.LawfulOrderBEq : (α : Type u) → [BEq α] → [LE α] → Prop
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.false.inj : ∀ {p p_1 : Lean.Expr}, Nat.EqResult.false✝ p = Nat.EqResult.false✝ p_1 → p = p_1
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalHom.frob_equivariant : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {k : Type u_1} [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p] {V : Type u_2} [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V]
  {V₂ : Type u_3} [inst_6 : AddCommGroup V₂] [inst_7 : WittVector.Isocrystal p k V₂]
  (self : WittVector.IsocrystalHom p k V V₂) (x : V),
  (WittVector.Isocrystal.frobenius p k) (self.toLinearMap x) =
    self.toLinearMap ((WittVector.Isocrystal.frobenius p k) x)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGT! : {α : Type u} →
  {β : α → Type v} → [Ord α] → [Inhabited ((a : α) × β a)] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.ae_dirac_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {a : α} {p : α → Prop},
  MeasurableSet {x | p x} → ((∀ᵐ (x : α) ∂MeasureTheory.Measure.dirac a, p x) ↔ p a)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_getValueCast?_eq_isSome_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α},
  (Std.Internal.List.getValueCast? a l).isSome = (Std.Internal.List.getEntry? a l).isSome
-- Mathlib.Order.SymmDiff
bihimp_bihimp_self : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp (bihimp a b) a = b
-- Init.Data.String.Decode
/-- Decodes and returns the `Char` whose UTF-8 encoding begins at `i` in `bytes`.

This function requires a proof that there is, in fact, a valid `Char` at `i`. `utf8DecodeChar?` is
an alternative function that returns `Option Char` instead of requiring a proof ahead of time.
 -/
ByteArray.utf8DecodeChar : (bytes : ByteArray) → (i : ℕ) → (bytes.utf8DecodeChar? i).isSome = true → Char
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The `L`-function of the trivial character mod `N`.  -/
DirichletCharacter.LFunctionTrivChar : (N : ℕ) → [NeZero N] → ℂ → ℂ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.instEpiSigmaπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.left] [inst_3 : CategoryTheory.Limits.HasCoproduct I.right],
  CategoryTheory.Epi (CategoryTheory.Limits.Multicoequalizer.sigmaπ I)
-- Std.Time.Time.Unit.Second
Std.Time.Second.instInhabitedOffset : Inhabited Std.Time.Second.Offset
-- Lean.Compiler.LCNF.Basic
/-- A pure application of a constant.
 -/
Lean.Compiler.LCNF.LetValue.const : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Name →
    List Lean.Level →
      Array (Lean.Compiler.LCNF.Arg pu) →
        autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_3 →
          Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Topology.Order.OrderClosed
Continuous.if_ge : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α]
  {f g : β → α} [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ] [inst_5 : (x : β) → Decidable (g x ≤ f x)]
  {f' g' : β → γ},
  Continuous f' →
    Continuous g' →
      Continuous f →
        Continuous g → (∀ (x : β), f x = g x → f' x = g' x) → Continuous fun x => if g x ≤ f x then f' x else g' x
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
/-- If `Fᵢ : C ⥤ Dᵢ` is a conservative family of functors which also
preserve the (existing) limit of a functor `G : J ⥤ C`, then a cone
for `G` is a limit if it is so after applying the functors `Fᵢ`
(see also `reflectsLimit_of_reflectsIsomorphisms` in the file
`Mathlib/CategoryTheory/Limits/Preserves/Basic.lean` for the corresponding
result for a single functor).  -/
CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectsLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_5, u_1} C] →
    {I : Type u_2} →
      {D : I → Type u_3} →
        [inst_1 : (i : I) → CategoryTheory.Category.{u_6, u_3} (D i)] →
          {F : (i : I) → CategoryTheory.Functor C (D i)} →
            CategoryTheory.JointlyReflectIsomorphisms F →
              {J : Type u_4} →
                [inst_2 : CategoryTheory.Category.{v_1, u_4} J] →
                  {G : CategoryTheory.Functor J C} →
                    {c : CategoryTheory.Limits.Cone G} →
                      ((i : I) → CategoryTheory.Limits.IsLimit ((F i).mapCone c)) →
                        [CategoryTheory.Limits.HasLimit G] →
                          [∀ (i : I), CategoryTheory.Limits.PreservesLimit G (F i)] → CategoryTheory.Limits.IsLimit c
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_psum : ∀ (α : Type u) (β : Type v),
  Cardinal.mk (α ⊕' β) = Cardinal.lift.{v, u} (Cardinal.mk α) + Cardinal.lift.{u, v} (Cardinal.mk β)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.getElem!_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α} [inst_4 : Inhabited β], m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁[k]! = m₂[k]!
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listEncode.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (i : α), (FirstOrder.Language.var i).listEncode = [Sum.inl i]
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.inv_def : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁), e⁻¹ = e.symm
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
ContinuousLinearMap.apply'.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} (F : Type u_6) [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] (σ₁₂ : 𝕜 →+* 𝕜₂) [inst_6 : RingHomIsometric σ₁₂],
  ContinuousLinearMap.apply' F σ₁₂ = ContinuousLinearMap.apply' F σ₁₂
-- Mathlib.Topology.UniformSpace.Cauchy
SequentiallyComplete.seq_pair_mem : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α}
  (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃N m n : ℕ⦄,
  N ≤ m → N ≤ n → (SequentiallyComplete.seq hf U_mem m, SequentiallyComplete.seq hf U_mem n) ∈ U N
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnityEquivNthRoots_apply : ∀ {R : Type u_4} {k : ℕ} [inst : NeZero k] [inst_1 : CommRing R] [inst_2 : IsDomain R] (x : ↥(rootsOfUnity k R)),
  ↑((rootsOfUnityEquivNthRoots R k) x) = ↑↑x
-- Lean.DocString.Markdown
/-- Strips leading and trailing whitespace from `inline`, returning the leading whitespace, the stripped
middle (still an `Inline`), and the trailing whitespace, in order. The caller can then re-emit the
leading and trailing whitespace *outside* of emphasis.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.trim : {i : Type u_1} → Lean.Doc.Inline i → String × Lean.Doc.Inline i × String
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.preservesMonomorphisms_of_adjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : G ⊣ F), F.PreservesMonomorphisms
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.normalizer.congr_simp : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N N_1 : LieSubmodule R L M), N = N_1 → N.normalizer = N_1.normalizer
-- Mathlib.Topology.Category.TopCat.Opens
/-- An open map `f : X ⟶ Y` induces an adjunction between `Opens X` and `Opens Y`.
 -/
IsOpenMap.adjunction : {X Y : TopCat} →
  {f : X ⟶ Y} → (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) → hf.functor ⊣ TopologicalSpace.Opens.map f
-- Lean.Declaration
Lean.ReducibilityHints.regular.injEq : ∀ (a a_1 : UInt32), (Lean.ReducibilityHints.regular a = Lean.ReducibilityHints.regular a_1) = (a = a_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.mk_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (v : (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q)) (p q : ℤ) (hpq : p + n = q),
  (CochainComplex.HomComplex.Cochain.mk v).v p q hpq = v p q hpq
-- Mathlib.Data.Set.Image
Set.image_inter_nonempty_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β}, (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
-- Mathlib.Order.RelIso.Basic
RelHom.coe_ofOnFun : ∀ {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β), ⇑(RelHom.ofOnFun r f) = f
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
/-- Let `S` be generated over `R` by `P : R[X] → S` with kernel `I` and let `T`
be the localization of `S` away from `g` generated over `S` by `S[Y] → T` with
kernel `K`.
Denote by `J` the kernel of the induced `R[X, Y] → T`. Then
`J/J² ≃ₗ[T] T ⊗[S] (I/I²) × (K/K²)`.

This is the splitting characterised by `x ↦ (0, g * X - 1)`.
 -/
Algebra.Generators.cotangentCompLocalizationAwayEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      {ι : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] →
                  [inst_5 : Algebra S T] →
                    [inst_6 : IsScalarTower R S T] →
                      (g : S) →
                        [inst_7 : IsLocalization.Away g T] →
                          (P : Algebra.Generators R S ι) →
                            {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent} →
                              (Algebra.Extension.Cotangent.map
                                      ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom)
                                    x =
                                  Algebra.Generators.cMulXSubOneCotangent T g →
                                ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent ≃ₗ[T]
                                  TensorProduct S T P.toExtension.Cotangent ×
                                    (Algebra.Generators.localizationAway T g).toExtension.Cotangent
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.mul : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'}, Meromorphic f → Meromorphic g → Meromorphic (f * g)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.instDecidableRelRelDown : (α : Type u_1) →
  [inst : AddRightCancelSemigroup α] →
    [DecidableEq α] → [inst_2 : One α] → DecidableRel fun a a_1 => (ComplexShape.down α).Rel a_1 a