mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Tilde
_private.Mathlib.AlgebraicGeometry.Modules.Tilde.0.AlgebraicGeometry.QuasicoherentTilde.aux_basicOpen_of_aux_restrict : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec R).Modules) (g : ↑R),
  AlgebraicGeometry.QuasicoherentTilde.Aux✝
      (M.restrict (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))))) ⊤ →
    AlgebraicGeometry.QuasicoherentTilde.Aux✝ M (PrimeSpectrum.basicOpen g)
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), MeromorphicAt id x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.pentagon : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} {A'''' : Type u₁₃} {B'''' : Type u₁₄}
  {C'''' : Type u₁₅} [inst_12 : CategoryTheory.Category.{v₁₃, u₁₃} A'''']
  [inst_13 : CategoryTheory.Category.{v₁₄, u₁₄} B''''] [inst_14 : CategoryTheory.Category.{v₁₅, u₁₅} C'''']
  {F'''' : CategoryTheory.Functor A'''' B''''} {G'''' : CategoryTheory.Functor C'''' B''''}
  {σ : CategoryTheory.Limits.CatCospanTransform F''' G''' F'''' G''''},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (ψ.associator φ τ).hom σ)
      (CategoryTheory.CategoryStruct.comp (ψ.associator (φ.comp τ) σ).hom
        (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (φ.associator τ σ).hom)) =
    CategoryTheory.CategoryStruct.comp ((ψ.comp φ).associator τ σ).hom (ψ.associator φ (τ.comp σ)).hom
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse.mk.inj : ∀ {response? : Option Lean.Json} {serialized : String} {isComplete : Bool} {response?_1 : Option Lean.Json}
  {serialized_1 : String} {isComplete_1 : Bool},
  { response? := response?, serialized := serialized, isComplete := isComplete } =
      { response? := response?_1, serialized := serialized_1, isComplete := isComplete_1 } →
    response? = response?_1 ∧ serialized = serialized_1 ∧ isComplete = isComplete_1
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
/-- The colimit multicofork attached to a `MulticoequalizerDiagram`
structure in the complete lattice of subcomplexes of a simplicial set.  -/
SSet.Subcomplex.MulticoequalizerDiagram.isColimit : {X : SSet} →
  {A : X.Subcomplex} →
    {ι : Type u_1} →
      {U : ι → X.Subcomplex} →
        {V : ι → ι → X.Subcomplex} →
          (h : A.MulticoequalizerDiagram U V) →
            CategoryTheory.Limits.IsColimit
              ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map SSet.Subcomplex.toSSetFunctor)
-- Init.Data.SInt.Bitwise
Int64.toBitVec_not : ∀ {a : Int64}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.Topology.Order
Nontrivial.of_nontrivialTopology : ∀ (α : Type u) [inst : TopologicalSpace α] [h : NontrivialTopology α], Nontrivial α
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.of_norm_le : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {g : α → ℝ},
  (∀ (x : α), ‖f x‖ ≤ g x) → f =O[l] g
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.hom_ext_iff : ∀ {R S : SemiRingCat} {f g : R ⟶ S}, f = g ↔ SemiRingCat.Hom.hom f = SemiRingCat.Hom.hom g
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_eq_single : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  [L.LeAtTop] {f : β → α} (b : β), (∀ (b' : β), b' ≠ b → f b' = 0) → ∑'[L] (b : β), f b = f b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point.0.termX : Lean.ParserDescr
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.Ref.cast_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (ref : aig1.Ref)
  (h : aig1.decls.size ≤ aig2.decls.size), ref.cast h = { gate := ref.gate, invert := ref.invert, hgate := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.stdSimplex.triangle.congr_simp : ∀ {n : ℕ} (a a_1 : Fin (n + 1)) (e_a : a = a_1) (b b_1 : Fin (n + 1)) (e_b : b = b_1) (c c_1 : Fin (n + 1))
  (e_c : c = c_1) (hab : a ≤ b) (hbc : b ≤ c),
  SSet.stdSimplex.triangle a b c hab hbc = SSet.stdSimplex.triangle a_1 b_1 c_1 ⋯ ⋯
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairs.eq_1 : ∀ (σ : Type u_1) [inst : DecidableEq σ] [inst_1 : Fintype σ] (k : ℕ),
  MvPolynomial.NewtonIdentities.pairs✝ σ k = {t | t.1.card ≤ k ∧ (t.1.card = k → t.2 ∈ t.1)}
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoin.finiteDimensional : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsIntegral K x → FiniteDimensional K ↥K⟮x⟯
-- Mathlib.Algebra.MonoidAlgebra.Opposite
MonoidAlgebra.opRingEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Mul M] (r : Rᵐᵒᵖ) (x : Mᵐᵒᵖ),
  MonoidAlgebra.opRingEquiv.symm (MonoidAlgebra.single x r) =
    MulOpposite.op (MonoidAlgebra.single (MulOpposite.unop x) (MulOpposite.unop r))
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Given two (in)equalities, look up the lemma to add them.  -/
Mathlib.Ineq.addRelRelData : Mathlib.Ineq → Mathlib.Ineq → Lean.Name
-- Mathlib.Algebra.Algebra.Unitization
/-- Non-unital algebra homomorphisms from `A` into a unital `R`-algebra `C` lift uniquely to
`Unitization R A →ₐ[R] C`. This is the universal property of the unitization.  -/
Unitization.lift : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : SMulCommClass R A A] →
            [inst_4 : IsScalarTower R A A] →
              {C : Type u_5} → [inst_5 : Semiring C] → [inst_6 : Algebra R C] → (A →ₙₐ[R] C) ≃ (Unitization R A →ₐ[R] C)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesAt.hasStrictDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜},
  HasFPowerSeriesAt f p x → HasStrictDerivAt f ((p 1) fun x => 1) x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_lt_one_of_nonneg_of_lt_one_left : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [PosMulMono M₀],
  0 ≤ a → a < 1 → b ≤ 1 → a * b < 1
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
tsum_mul_left : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α} [T2Space α], ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_filter_le_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool}, (Std.DTreeMap.filter f t).size ≤ t.size
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor `Comma L R ⥤ Comma L R` induced by the identity natural transformation on `R` is
naturally isomorphic to the identity functor.  -/
CategoryTheory.Comma.mapRightId : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (R : CategoryTheory.Functor B T) →
              (L : CategoryTheory.Functor A T) →
                CategoryTheory.Comma.mapRight L (CategoryTheory.CategoryStruct.id R) ≅
                  CategoryTheory.Functor.id (CategoryTheory.Comma L R)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.filter.eq_1 : ∀ (α : Type u_1) (β : Type u_2) (𝓕 : Filter (β × β)), UniformFun.filter α β 𝓕 = (UniformFun.basis α β 𝓕).filter
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁
-- Mathlib.FieldTheory.SeparableDegree
Field.finSepDegree_self : ∀ (F : Type u) [inst : Field F], Field.finSepDegree F F = 1
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.inter_insert_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α} {a : α}, a ∈ s₁ → s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedFeature : Inhabited Aesop.Frontend.Feature
-- Lean.Data.Name
/-- The frontend does not allow user declarations to start with `_` in any of its parts.
We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`).  -/
Lean.Name.isInternal : Lean.Name → Bool
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.iterate_toEnd_mem_lowerCentralSeries : ∀ (R : Type u) (L : Type v) (M : Type w) [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] (x : L)
  (m : M) (k : ℕ), (⇑((LieModule.toEnd R L M) x))^[k] m ∈ LieModule.lowerCentralSeries R L M k
-- Lean.Message
/-- Puts `MessageData` into a comma-separated list with `"or"` at the back (with the serial comma).

Best used on non-empty lists; returns `"– none –"` for an empty list.
 -/
Lean.MessageData.orList : List Lean.MessageData → Lean.MessageData
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (t.modify k f).isEmpty = false → (t.modify k f).maxKey! = if cmp t.maxKey! k = Ordering.eq then k else t.maxKey!
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).isEmpty = l.isEmpty
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] (H : J.OneHypercoverFamily) (P : CategoryTheory.Functor Cᵒᵖ A)
  [H.IsGenerating],
  CategoryTheory.Presheaf.IsSheaf J P ↔
    ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))
-- Mathlib.Topology.Inseparable
IsClosed.not_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, IsClosed s → x ∈ s → y ∉ s → ¬x ⤳ y
-- Mathlib.Data.Part
Part.instOrderBot : {α : Type u_1} → OrderBot (Part α)
-- Mathlib.Topology.Algebra.ConstMulAction
continuousAt_const_smul_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} (c : G),
  ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.mk.sizeOf_spec : ∀ (L : Type w) (R : Type w') (fst snd : L → R),
  sizeOf { L := L, R := R, fst := fst, snd := snd } = 1 + sizeOf L + sizeOf R
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.of_symm_nsmul : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [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]
  (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (n : ℕ) (x : LieAlgebra.ofTwoCocycle c),
  (LieAlgebra.ofProd c).symm (n • x) = n • (LieAlgebra.ofProd c).symm x
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.toOrderMonoidWithZeroHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), f.toOrderMonoidWithZeroHom = ↑f
-- Mathlib.RingTheory.Nilpotent.Lemmas
IsRadical.eq_1 : ∀ {R : Type u_1} [inst : Dvd R] [inst_1 : Pow R ℕ] (y : R), IsRadical y = ∀ (n : ℕ) (x : R), y ∣ x ^ n → y ∣ x
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Given a family of elements of a sieve `S` on `X` whose values factors through `F`, we can
realize it as a family of elements of `S.functorPushforward F`. Since the preimage is obtained by
choice, this is not well-defined generally.
 -/
CategoryTheory.Presieve.FamilyOfElements.functorPushforward : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (F : CategoryTheory.Functor D C) →
            {X : D} →
              {T : CategoryTheory.Presieve X} →
                CategoryTheory.Presieve.FamilyOfElements (F.op.comp P) T →
                  CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.functorPushforward F T)
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The (exact) sequence `0 ⟶ E^n(f₁, f₂, f₃) ⟶ opZ^n(f₂, f₃) ⟶ H^{n+1}(f₁)`.  -/
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE : {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] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k l : ι} →
              (i ⟶ j) →
                (j ⟶ k) →
                  (k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_1 →
                        autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_3 →
                          CategoryTheory.ShortComplex C
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- `allowedImportDirs` relates module prefixes, specifying that modules with the first prefix
are only allowed to import modules in the second directory.
For directories which are low in the import hierarchy, this opt-out approach is both more ergonomic
(fewer updates needed) and needs less configuration.

We always allow imports of `Init`, `Lean`, `Std`, `Qq` and
`Mathlib.Init` (as well as their transitive dependencies.)
 -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.allowedImportDirs : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.all_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String}, s.toSlice.all pat = s.all pat
-- Init.Data.UInt.Bitwise
UInt64.shiftRight_or : ∀ {a b c : UInt64}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RcoSliceData α β)) Id (Std.DTreeMap.Internal.RxoIterator α β)
        ((a : α) × β a)
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.id_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : P.IsMultiplicative] (X : CategoryTheory.WideSubcategory P),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
-- Mathlib.RingTheory.IdealFilter.Basic
/-- `IdealFilter A` is the type of `Order.PFilter`s on the lattice of ideals of `A`.  -/
IdealFilter : (A : Type u_1) → [Ring A] → Type u_1
-- Mathlib.CategoryTheory.Limits.Pi
/-- A cone over `F : J ⥤ Π i, C i` has as its components cones over each of the `F ⋙ Pi.eval C i`.
 -/
CategoryTheory.pi.coneCompEval : {I : Type v₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type v₁} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          {F : CategoryTheory.Functor J ((i : I) → C i)} →
            CategoryTheory.Limits.Cone F → (i : I) → CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Pi.eval C i))
-- Mathlib.Analysis.Complex.Conformal
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals `ContinuousLinearMap.complexOfReal` of the real derivative.
 -/
complexOfReal_hasDerivWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ},
  DifferentiableWithinAt ℝ f s x →
    ∀ (h₂ : (fderivWithin ℝ f s x) Complex.I = Complex.I • (fderivWithin ℝ f s x) 1),
      HasDerivWithinAt f (((fderivWithin ℝ f s x).complexOfReal h₂) 1) s x
-- Mathlib.Algebra.Homology.QuasiIso
HomotopyEquiv.quasiIso_hom : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (e : HomotopyEquiv K L) [inst_2 : ∀ (n : ι), K.HasHomology n]
  [inst_3 : ∀ (n : ι), L.HasHomology n], QuasiIso e.hom
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.toAddSubgroup_injective : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G], Function.Injective ClosedAddSubgroup.toAddSubgroup
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unfoldRule.injEq : ∀ (r r_1 : Aesop.UnfoldRule),
  (Aesop.BaseRuleSetMember.unfoldRule r = Aesop.BaseRuleSetMember.unfoldRule r_1) = (r = r_1)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Configurations that avoid a family `F` of patterns are stable under the shift.

Formally: if `x` avoids every `p ∈ F` at every position, then for any `h : G`,
the shifted configuration `shift h x` also avoids every `p ∈ F` at every position.  -/
SymbolicDynamics.FullShift.Pattern.mapsTo_shift_forbidden : ∀ {A : Type u_3} {G : Type u_4} [inst : Inhabited A] [inst_1 : AddMonoid G]
  (F : Set (SymbolicDynamics.FullShift.Pattern A G)) (h : G),
  Set.MapsTo (SymbolicDynamics.FullShift.shift h) (SymbolicDynamics.FullShift.forbidden F)
    (SymbolicDynamics.FullShift.forbidden F)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.endsWith_bool_eq_getLast? : ∀ {p : Char → Bool} {s : String}, s.endsWith p = Option.any p s.toList.getLast?
-- Init.Data.Option.Lemmas
Option.map_dif : ∀ {α : Type u_1} {β : Type u_2} {c : Prop} {f : α → β} {x : Decidable c} {a : c → α},
  Option.map f (if h : c then some (a h) else none) = if h : c then some (f (a h)) else none
-- Init.Data.Array.Erase
Array.eraseP_eq_empty_iff : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, xs.eraseP p = #[] ↔ xs = #[] ∨ ∃ x, p x = true ∧ xs = #[x]
-- Lean.Attributes
Lean.AttributeExtensionOLeanEntry.ref : Lean.AttributeExtensionOLeanEntry → Lean.Name
-- Mathlib.Algebra.Ring.Parity
Nat.not_even_two_mul_add_one : ∀ (n : ℕ), ¬Even (2 * n + 1)
-- Batteries.Recycling.RBTree.Basic
/-- Asserts that `t₁` and `t₂` have the same number of elements in the same order,
and `R` holds pairwise between them. The tree structure is ignored.
 -/
RBTree.RBSet.all₂ : {α : Type u_1} →
  {β : Type u_2} →
    {cmpα : α → α → Ordering} →
      {cmpβ : β → β → Ordering} → (α → β → Bool) → RBTree.RBSet α cmpα → RBTree.RBSet β cmpβ → Bool
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.noinline : Lean.Compiler.InlineAttributeKind
-- Mathlib.CategoryTheory.Subfunctor.Image
/-- The preimage of a subfunctor by a morphism of type-valued functors.  -/
CategoryTheory.Subfunctor.preimage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F' : CategoryTheory.Functor C (Type w)} → CategoryTheory.Subfunctor F → (F' ⟶ F) → CategoryTheory.Subfunctor F'
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ofGroup_toList : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G),
  (HNNExtension.NormalWord.ofGroup g).toList = []
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C)
  (X_1 : SimplexCategoryᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id
      (X.obj
        (match CategoryTheory.WithTerminal.incl.obj X_1 with
        | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
        | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))
-- Mathlib.Order.Basic
/-- **Alias** of `lt_or_eq_of_le'`. -/
LE.le.lt_or_eq' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → b < a ∨ a = b
-- Mathlib.Analysis.Normed.Group.Constructions
Additive.toNorm : {E : Type u_2} → [Norm E] → Norm (Additive E)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Mul α] [inst_4 : Mul β] [inst_5 : Mul γ] {g₁ g₂ : α ≃*o β} {f : β ≃*o γ},
  Function.Injective ⇑f → (g₁.trans f = g₂.trans f ↔ g₁ = g₂)
-- Lean.DocString.Extension
/-- Adds a builtin docstring to the compiler.

Links to the Lean manual aren't validated.
 -/
Lean.addBuiltinDocString : Lean.Name → String → IO Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_inter_le_size_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (m₁ ∩ m₂).size ≤ m₁.size
-- Lean.Elab.Tactic.Induction
/-- Elaborates the `foo args` of `fun_induction` or `fun_cases`, inferring the args if omitted from the goal
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.elabFunTargetCall : Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Expr
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.of_near : ∀ (f : ℕ → ℚ) (x : ℝ), (∀ ε > 0, ∃ i, ∀ j ≥ i, |↑(f j) - x| < ε) → ∃ (h' : IsCauSeq abs f), Real.mk ⟨f, h'⟩ = x
-- Mathlib.Data.PNat.Interval
PNat.map_subtype_embedding_Ioo : ∀ (a b : ℕ+), Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.isIso_limMap : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) [CategoryTheory.IsIso α],
  CategoryTheory.IsIso (CategoryTheory.Limits.limMap α)
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `link` which can be used in the absence of balance information but
still assumes the preconditions of `link`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.link! : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β