mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β} {f : Option β → Option β},
  Std.DTreeMap.Const.getD (Std.DTreeMap.Const.alter t k f) k fallback = (f (Std.DTreeMap.Const.get? t k)).getD fallback
-- Lean.Elab.Command
Lean.Elab.Command.Linter.name : Lean.Linter → Lean.Name
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k k' fallback : α},
      (k == k') = true →
        m.contains k = false →
          List.Pairwise (fun a b => (a == b) = false) l →
            k ∈ l → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKeyD k' fallback = k
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdxD.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : ℕ) (x_2 : (a : α) × β a),
  x.entryAtIdxD x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback =>
      match compare n l.size with
      | Ordering.lt => l.entryAtIdxD n fallback
      | Ordering.eq => ⟨k, v⟩
      | Ordering.gt => r.entryAtIdxD (n - l.size - 1) fallback
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorInt8 : LawfulXor Int8
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.limitConstTerminal_hom : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.Limits.limitConstTerminal.hom =
    CategoryTheory.Limits.terminal.from (CategoryTheory.Limits.limit ((CategoryTheory.Functor.const J).obj (⊤_ C)))
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_mod : ∀ (a b : UInt16), a < 256 → b < 256 → (a % b).toUInt8 = a.toUInt8 % b.toUInt8
-- Mathlib.Algebra.Group.Basic
mul_eq_one_iff_eq_inv : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a * b = 1 ↔ a = b⁻¹
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_eq_zero_iff : ∀ (x : ENNReal), x.toReal = 0 ↔ x = 0 ∨ x = ⊤
-- Mathlib.Data.Sym.Sym2.Finsupp
Finsupp.mem_sym2_support_of_mul_ne_zero : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : CommMonoidWithZero M₀] {f : α →₀ M₀} (p : Sym2 α),
  (Sym2.map (⇑f) p).mul ≠ 0 → p ∈ f.support.sym2
-- Mathlib.RingTheory.Idempotents
Subsemigroup.mem_corner_iff : ∀ {R : Type u_1} {e : R} [inst : Semigroup R],
  IsIdempotentElem e → ∀ {r : R}, r ∈ Subsemigroup.corner e ↔ e * r = r ∧ r * e = r
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.stacksTagDB.quot : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.ExtDHashMap.alter : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [LawfulBEq α] → Std.ExtDHashMap α β → (a : α) → (Option (β a) → Option (β a)) → Std.ExtDHashMap α β
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_sInf : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (s : Set (Submodule R E)),
  ↑(sInf s) = sInf (PointedCone.ofSubmodule '' s)
-- Std.Http.Internal.LowerCase
Char.isUpper.eq_1 : ∀ (c : Char), c.isUpper = decide (c.val ≥ 'A'.val ∧ c.val ≤ 'Z'.val)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.id'_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (M : Bimod A B), M.id'.hom = CategoryTheory.CategoryStruct.id M.X
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₂.getKey k ⋯
-- Batteries.Data.List.Perm
_private.Batteries.Data.List.Perm.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap_assoc : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₂ f₁ f₂ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁' f₂'),
  β = CategoryTheory.ComposableArrows.homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯ →
    ∀ (n₀ n₁ n₂ : ℤ)
      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap._auto_3) {Z : C}
      (h : (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).cycles ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.ShortComplex.cyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)) h) =
        CategoryTheory.CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁' f₂' β n₁)
          (CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).inv h)
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- Scalar multiplication by `r : R`. Use `•` instead.  -/
SymmetricPower.smul' : {R : Type u} →
  (ι : Type u) →
    [inst : CommSemiring R] →
      (M : Type v) →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → R → SymmetricPower R ι M →+ SymmetricPower R ι M
-- Mathlib.Algebra.Ring.Defs
/-- A non-unital non-associative commutative ring is a `NonUnitalNonAssocRing` with commutative
multiplication.  -/
NonUnitalNonAssocCommRing : Type u → Type u
-- Mathlib.Order.Concept
Concept.surjective_ofAttributes : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, Function.Surjective (Concept.ofAttributes r)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_ball_center : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (x : E) (r : ℝ), μ (Metric.ball x r) = μ (Metric.ball 0 r)
-- Mathlib.Data.Set.Lattice.Image
Set.kernImage_compl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Set.kernImage f sᶜ = (f '' s)ᶜ
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.subsingleton_of_injective : ∀ {R : Type u_1} {P : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid P] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R P] [inst_4 : Module R N] [IsArtinian R N] {f : P × N →ₗ[R] N},
  Function.Injective ⇑f → Subsingleton P
-- Mathlib.Order.Lattice.Nat
Nat.sInf_add : ∀ {n : ℕ} {p : ℕ → Prop}, n ≤ sInf {m | p m} → sInf {m | p (m + n)} + n = sInf {m | p m}
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.smul_mem_pointwise_smul : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddGroup A] [inst_2 : DistribMulAction M A] (m : A) (a : M)
  (S : AddSubgroup A), m ∈ S → a • m ∈ a • S
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_lt_arctan_iff : ∀ {x y : ℝ}, Real.arctan x < Real.arctan y ↔ x < y
-- Mathlib.Data.Int.ModEq
Int.ModEq.neg : ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → -a ≡ -b [ZMOD n]
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- The inessential (i.e. finite dimensional) part of a Fredholm decomposition.  -/
FredholmDecomposition.X₀ : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [inst_3 : TopologicalSpace E] → FredholmDecomposition 𝕜 E → Submodule 𝕜 E
-- Mathlib.Data.Multiset.Range
Multiset.nodup_range : ∀ (n : ℕ), (Multiset.range n).Nodup
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.lift_of : ∀ {α : Type u_3} {M : Type u_4} [inst : AddMonoid M] (f : α → M) {rels : FreeAddMonoid α → FreeAddMonoid α → Prop}
  (h : ∀ (a b : FreeAddMonoid α), rels a b → (FreeAddMonoid.lift f) a = (FreeAddMonoid.lift f) b) {x : α},
  (PresentedAddMonoid.lift f h) (PresentedAddMonoid.of rels x) = f x
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSMulCommClass_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M] [inst_4 : Mul M] [inst_5 : ContinuousMul M]
  [SMulCommClass R M M], SMulCommClass R C(α, M) C(α, M)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsMarkovKernel.mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β},
  (∀ (a : α), MeasureTheory.IsProbabilityMeasure (κ a)) → ProbabilityTheory.IsMarkovKernel κ
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_lt_mul_left_of_neg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R}, c < 0 → (c * a < c * b ↔ b < a)
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift_nonempty : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f₁ : α₁ → β₁ → Finset γ₁} {f₂ : α₂ → β₂ → Finset γ₂} {g₁ : α₁ → β₂ → Finset γ₁} {g₂ : α₁ → β₂ → Finset γ₂}
  {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂},
  (Finset.sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔
    (∃ a₁ b₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
      (∃ a₁ b₂, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
        ∃ a₂ b₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ (f₂ a₂ b₂).Nonempty
-- Lean.ToExpr
Lean.instToExprBitVec : {n : ℕ} → Lean.ToExpr (BitVec n)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_Icc_castSucc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc ⁻¹' Set.Icc i.castSucc j.castSucc = Set.Icc i j
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductLimitCone_isLimit : ∀ (X Y : Type u),
  (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).isLimit = CategoryTheory.Limits.Types.binaryProductLimit X Y
-- Mathlib.RingTheory.Flat.Localization
IsSMulRegular.of_isLocalizedModule : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (p : Submonoid R) [IsLocalization p S] {M : Type u_3} [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : Module S M] [IsScalarTower R S M] {K : Type u_6} [inst_8 : AddCommMonoid K] [inst_9 : Module R K]
  (f : K →ₗ[R] M) [IsLocalizedModule p f] {x : R}, IsSMulRegular K x → IsSMulRegular M ((algebraMap R S) x)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.algHom_ext : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Ring A] [inst_2 : Algebra R A]
  {f g : QuadraticAlgebra R a b →ₐ[R] A}, f QuadraticAlgebra.omega = g QuadraticAlgebra.omega → f = g
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves
monomorphisms.  -/
CategoryTheory.Functor.ReflectsMonomorphisms.reflects : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.ReflectsMonomorphisms] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f
-- Mathlib.FieldTheory.Galois.Basic
/-- The map from the `Gal(E/L)` to `Gal(K/F)` where `E/L/F` and `E/K/F` are two towers of
extensions induced by the restriction to `K`. Note that we do require `K/F` to be normal but not
`E/L`. If this is the case (and everything is finite dimensional) and `K ∩ L = F` then this
map is surjective, see `IntermediateField.restrictRestrictMapHom_surjective`.
This map is injective if the compositum of `K` and `L` is `E`,
see `IntermediateField.restrictRestrictAlgEquivMapHom_injective`.
 -/
IntermediateField.restrictRestrictAlgEquivMapHom : (F : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      (E : Type u_4) →
        [inst : Field F] →
          [inst_1 : Field K] →
            [inst_2 : Field L] →
              [inst_3 : Field E] →
                [inst_4 : Algebra F K] →
                  [inst_5 : Algebra F L] →
                    [inst_6 : Algebra F E] →
                      [inst_7 : Algebra K E] →
                        [inst_8 : Algebra L E] →
                          [IsScalarTower F K E] → [IsScalarTower F L E] → [Normal F K] → Gal(E/L) →* Gal(K/F)
-- Lean.Meta.Tactic.Simp.Main
/-- Simplify `simp` result to the given local declaration. Return `none` if the goal was closed.
This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context.  -/
Lean.Meta.applySimpResultToLocalDecl : Lean.MVarId → Lean.FVarId → Lean.Meta.Simp.Result → Bool → Lean.MetaM (Option (Lean.FVarId × Lean.MVarId))
-- Init.Data.UInt.Bitwise
UInt32.toUInt64_shiftLeft : ∀ (a b : UInt32), (a <<< b).toUInt64 = a.toUInt64 <<< (b % 32).toUInt64 % 4294967296
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyLift_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {F P Q : CategoryTheory.Functor Cᵒᵖ D} (a : F ⟶ P) (hP : CategoryTheory.Presheaf.IsSheaf J P) (η : P ⟶ Q)
  (hQ : CategoryTheory.Presheaf.IsSheaf J Q),
  CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.comp a η) hQ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J a hP) η
-- Aesop.Search.Queue
Aesop.FIFOQueue.goals : Aesop.FIFOQueue → Array Aesop.GoalRef
-- Mathlib.Tactic.CancelDenoms.Core
/-- `CancelResult mα e v'` provides a value for `v * e` where the denominators have been cancelled.
 -/
Mathlib.Tactic.CancelDenoms.CancelResult : {u : Lean.Level} → {α : Q(Type u)} → Q(Mul «$α») → Q(«$α») → Q(«$α») → Type
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.instHasInitial : CategoryTheory.Limits.HasInitial AugmentedSimplexCategory
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_add : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_13 : ContinuousAdd M₂]
  [inst_14 : ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M₁ →SL[σ₁₂] M₂), g ∘SL (f₁ + f₂) = g ∘SL f₁ + g ∘SL f₂
-- Mathlib.CategoryTheory.EffectiveEpi.Coproduct
/-- This is an auxiliary lemma used twice in the definition of  `EffectiveEpiFamilyOfEffectiveEpiDesc`.
It is the `h` hypothesis of `EffectiveEpi.desc` and `EffectiveEpi.fac`.
 -/
CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B} [inst_1 : CategoryTheory.Limits.HasCoproduct X]
  [inst_2 : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)]
  [inst_3 :
    ∀ {Z : C} (g : Z ⟶ ∐ X),
      CategoryTheory.Limits.HasCoproduct fun a => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)]
  [∀ {Z : C} (g : Z ⟶ ∐ X),
      CategoryTheory.Epi
        (CategoryTheory.Limits.Sigma.desc fun a =>
          CategoryTheory.Limits.pullback.fst g (CategoryTheory.Limits.Sigma.ι X a))]
  {W : C} {e : (a : α) → X a ⟶ W},
  (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
    ∀ {Z : C} {g₁ g₂ : Z ⟶ ∐ fun b => X b},
      CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc π) =
          CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc π) →
        CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc e) =
          CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc e)
-- Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
/-- If a category has all binary products and all equalizers, then it also has all pullbacks.
As usual, this is not an instance, since there may be a more direct way to construct
pullbacks.  -/
CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C]
  [CategoryTheory.Limits.HasEqualizers C], CategoryTheory.Limits.HasPullbacks C
-- Mathlib.Logic.Function.Iterate
Function.Semiconj.iterate_right : ∀ {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β},
  Function.Semiconj f ga gb → ∀ (n : ℕ), Function.Semiconj f ga^[n] gb^[n]
-- Lean.Data.Json.Basic
Lean.Json.num.sizeOf_spec : ∀ (n : Lean.JsonNumber), sizeOf (Lean.Json.num n) = 1 + sizeOf n
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.DerivedLitsInvariant : {n : ℕ} →
  (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) →
    f.assignments.size = n →
      (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
        assignments.size = n → Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Prop
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapM_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → o δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.mapM f it)).toListRev =
    (Std.IterM.mapM
        (fun b => do
          let __do_lift ← liftM (f b)
          g __do_lift)
        it).toListRev
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Finset.summable : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
  Summable (f ∘ Subtype.val)
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.toSubsemiring : {R : Type u_1} → [inst : Ring R] → RingCone R → Subsemiring R
-- Mathlib.Analysis.Distribution.DerivNotation
/-- `∂^{m} f` is the iterated line derivative of `f`, where `m` is a finite number of (different)
directions.  -/
LineDeriv.«term∂^{_}» : Lean.ParserDescr
-- Init.Data.Nat.Lemmas
Nat.one_lt_pow' : ∀ (n m : ℕ), 1 < (m + 2) ^ (n + 1)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.id_onTerm : ∀ {L : FirstOrder.Language} {α : Type u'}, (FirstOrder.Language.LHom.id L).onTerm = id
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_toInfTopHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β), ⇑f.toInfTopHom = ⇑f
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictSupport_mono : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] {s t : Set (σ →₀ ℕ)},
  s ⊆ t → MvPolynomial.restrictSupport R s ≤ MvPolynomial.restrictSupport R t
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conjAut_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X),
  α.conjAut f = α.symm ≪≫ f ≪≫ α
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.coverEntropyInf_restrict_subset : ∀ {X : Type u_1} [inst : UniformSpace X] {T : X → X} {F G : Set X},
  F ⊆ G →
    ∀ (hG : Set.MapsTo T G G),
      Dynamics.coverEntropyInf (Set.MapsTo.restrict T G G hG) (Subtype.val ⁻¹' F) = Dynamics.coverEntropyInf T F
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₁_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.a₁ = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (toPreOneHypercover : CategoryTheory.PreOneHypercover S) (mem₀ : toPreOneHypercover.sieve₀ ∈ J S)
  (mem₁ :
    ∀ (i₁ i₂ : toPreOneHypercover.I₀) ⦃W : C⦄ (p₁ : W ⟶ toPreOneHypercover.X i₁) (p₂ : W ⟶ toPreOneHypercover.X i₂),
      CategoryTheory.CategoryStruct.comp p₁ (toPreOneHypercover.f i₁) =
          CategoryTheory.CategoryStruct.comp p₂ (toPreOneHypercover.f i₂) →
        toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W)
  (toPreOneHypercover_1 : CategoryTheory.PreOneHypercover S) (mem₀_1 : toPreOneHypercover_1.sieve₀ ∈ J S)
  (mem₁_1 :
    ∀ (i₁ i₂ : toPreOneHypercover_1.I₀) ⦃W : C⦄ (p₁ : W ⟶ toPreOneHypercover_1.X i₁)
      (p₂ : W ⟶ toPreOneHypercover_1.X i₂),
      CategoryTheory.CategoryStruct.comp p₁ (toPreOneHypercover_1.f i₁) =
          CategoryTheory.CategoryStruct.comp p₂ (toPreOneHypercover_1.f i₂) →
        toPreOneHypercover_1.sieve₁ p₁ p₂ ∈ J W),
  ({ toPreOneHypercover := toPreOneHypercover, mem₀ := mem₀, mem₁ := mem₁ } =
      { toPreOneHypercover := toPreOneHypercover_1, mem₀ := mem₀_1, mem₁ := mem₁_1 }) =
    (toPreOneHypercover = toPreOneHypercover_1)
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the open ball of radius `r ≤ ∞` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.hasSum_taylorSeries_on_eball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄
  ⦃r : ENNReal⦄,
  DifferentiableOn ℂ f (Metric.eball c r) →
    ∀ ⦃z : ℂ⦄, z ∈ Metric.eball c r → HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
-- Lean.Parser.Types
Lean.Parser.FirstTokens.toStr : Lean.Parser.FirstTokens → String
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.Functor.CommShift₂.precomp₂ : {C₁ : Type u_1} →
  {C₂ : Type u_3} →
    {C₂' : Type u_4} →
      {D : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} C₂'] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D] →
                {M : Type u_6} →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : CategoryTheory.HasShift C₁ M] →
                      [inst_6 : CategoryTheory.HasShift C₂' M] →
                        [inst_7 : CategoryTheory.HasShift C₂ M] →
                          [inst_8 : CategoryTheory.HasShift D M] →
                            (F : CategoryTheory.Functor C₂' C₂) →
                              [F.CommShift M] →
                                (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  (h : CategoryTheory.CommShift₂Setup D M) →
                                    [G.CommShift₂ h] →
                                      (G.comp ((CategoryTheory.Functor.whiskeringLeft C₂' C₂ D).obj F)).CommShift₂ h