mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt16HAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Mathlib.CategoryTheory.Abelian.CommSq
/-- Given a commutative diagram in an abelian category
```
X₁ ⟶ X₂
|    |  \
v    v   \
X₃ ⟶ X₄   \
 \     \   v
  \     \> X₅
   \_____>
```
where the top/left square is a pushout square,
the outer square involving `X₁`, `X₂`, `X₃` and `X₅`
is a pullback square, and `X₂ ⟶ X₅` is mono,
then `X₄ ⟶ X₅` is a mono.
 -/
CategoryTheory.IsPushout.mono_of_isPullback_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂}
  {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPushout t l r b →
    ∀ {X₅ : C} {r' : X₂ ⟶ X₅} {b' : X₃ ⟶ X₅},
      CategoryTheory.IsPullback t l r' b' →
        ∀ (k : X₄ ⟶ X₅),
          CategoryTheory.CategoryStruct.comp r k = r' →
            CategoryTheory.CategoryStruct.comp b k = b' → ∀ [CategoryTheory.Mono r'], CategoryTheory.Mono k
-- Lean.Elab.Do.Basic
Lean.Elab.Do.SavedState.mk : Lean.Elab.Term.SavedState → Lean.Elab.Do.SavedState
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The functor which associates to a functor `F` the bifunctor `F (- ⊗ -)`.  -/
CategoryTheory.MonoidalCategory.curriedTensorPostFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor C (CategoryTheory.Functor C D))
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateCasesImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.Expr → Lean.FVarId → Array (Lean.Compiler.LCNF.Alt pu) → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSemiringOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → Semiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → Semiring (DirectLimit G f)
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse.toSerializedMessage : Lean.JsonRpc.RequestID → Lean.Server.SerializedLspResponse → String
-- Lean.Parser.Do
Lean.Parser.Term.doIfLetBind : Lean.Parser.Parser
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff' : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G}
  {x : MulAction.orbitRel.Quotient G α} {a b : ↑x.orbit} {c : α},
  ⟦a⟧ = ⟦b⟧ → (↑a ∈ MulAction.orbit (↥H) c ↔ ↑b ∈ MulAction.orbit (↥H) c)
-- Mathlib.Data.Nat.ModEq
/-- **Alias** of the reverse direction of `Nat.modEq_iff_dvd'`.

---

A variant of `modEq_iff_dvd` with `Nat` divisibility  -/
Nat.modEq_of_dvd' : ∀ {n a b : ℕ}, a ≤ b → n ∣ b - a → a ≡ b [MOD n]
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.instInv : {𝕜 : Type u_1} → [inst : NormedDivisionRing 𝕜] → Inv ↑(Metric.sphere 0 1)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.instEquivLike : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → EquivLike (A ≃ₗc[R] B) A B
-- Mathlib.Order.Types.Arithmetic
/-- The order type of the real numbers. 

Conventions for notations in identifiers:

 * The recommended spelling of `θ` in identifiers is `theta`. -/
OrderType.termθ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.self_trans_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), e.trans e.symm = ContinuousAffineEquiv.refl k P₁
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.exists_i₁ : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ → ∀ (i : ι), (∀ (i₂ : ι₂), e₂.f i₂ ≠ i) → ∃ i₁, i = e₁.f i₁
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.tail_neg : ∀ {α : Type u_1} {n : ℕ} [inst : Neg α] (a : Fin n.succ → α), Matrix.vecTail (-a) = -Matrix.vecTail a
-- Mathlib.LinearAlgebra.Pi
/-- A linear map `f` applied to `x : ι → R` can be computed using the image under `f` of elements
of the canonical basis.  -/
LinearMap.pi_apply_eq_sum_univ : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (f : (ι → R) →ₗ[R] M₂) (x : ι → R),
  f x = ∑ i, x i • f fun j => if i = j then 1 else 0
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.Weight.IsZero.neg : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_5 : H.IsCartanSubalgebra] [inst_6 : LieModule.IsTriangularizable K (↥H) L] {α : LieModule.Weight K (↥H) L},
  α.IsZero → (-α).IsZero
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyoneda.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.shrinkCoyoneda.{w, v, u} = CategoryTheory.shrinkCoyoneda.{w, v, u}
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.addConjMap_ofFixingAddSubgroup_coe_apply : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {g : M} {hg : g +ᵥ t = s}
  (x : ↥(SubAddAction.ofFixingAddSubgroup M t)), ↑((SubAddAction.addConjMap_ofFixingAddSubgroup hg) x) = g +ᵥ ↑x
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- `mabs a`, denoted `|a|ₘ`, is the absolute value of `a`.  -/
mabs : {α : Type u_1} → [Lattice α] → [Group α] → α → α
-- Mathlib.Data.Set.Prod
Set.Subsingleton.prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s.Subsingleton → t.Subsingleton → (s ×ˢ t).Subsingleton
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKeyD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a fallback : α),
  Std.DHashMap.Internal.AssocList.getKeyD a fallback Std.DHashMap.Internal.AssocList.nil = fallback
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.image_symm_image : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂), ⇑e '' ⇑e.symm '' s = s
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects colimits of shape `Jᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` reflects limits
of shape `J`.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.Limits.ReflectsColimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.ReflectsLimitsOfShape J F.rightOp
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))} (f : X ⟶ Y) (n : α),
  (((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.map f).f n).f = f.f.f n
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_mul : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)] (f g : DirectSum ι fun x => M),
  (f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_nil_basis : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial), m.toLogFun [] = 0
-- Init.System.CancelToken
_private.Init.System.CancelToken.0.IO.CancelToken.promise : IO.CancelToken → IO.Promise Unit
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.truthIsRegularMono`.

---

`truth C` is a regular monomorphism (because it is split).  -/
CategoryTheory.HasClassifier.truthIsRegularMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasSubobjectClassifier C] →
      CategoryTheory.RegularMono (CategoryTheory.HasSubobjectClassifier.truth C)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_one_diagonal : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (d : n → R),
  Matrix.detp 1 (Matrix.diagonal d) = ∏ i, d i
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
MulOpposite.op_finsuppSum : ∀ {ι : Type u_16} {M : Type u_17} {N : Type u_18} [inst : AddCommMonoid M] [inst_1 : Zero N] (f : ι →₀ N)
  (g : ι → N → M), MulOpposite.op (f.sum g) = f.sum fun i n => MulOpposite.op (g i n)
-- Lean.Parser.Basic
Lean.Parser.instInhabitedLeadingIdentBehavior.default : Lean.Parser.LeadingIdentBehavior
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.not_dvd_of_not_mod_zero : ∀ {a b : ℤ}, ¬b % a = 0 → ¬a ∣ b
-- Std.Data.HashSet.Lemmas
Std.HashSet.equiv_empty_iff_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.Equiv ∅ ↔ m.isEmpty = true
-- Mathlib.Algebra.MvPolynomial.Expand
/-- Expand the polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`.

See also `Polynomial.expand`.  -/
MvPolynomial.expand : {σ : Type u_1} → {R : Type u_3} → [inst : CommSemiring R] → ℕ → MvPolynomial σ R →ₐ[R] MvPolynomial σ R
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioi_ssubset_Ioi : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], a < b → Finset.Ioi b ⊂ Finset.Ioi a
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- The action of a localizer morphism `Φ` on `SmallShiftedHom`.  -/
CategoryTheory.LocalizerMorphism.smallShiftedHomMap : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    {C₂ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              {M : Type w'} →
                [inst_2 : AddMonoid M] →
                  [inst_3 : CategoryTheory.HasShift C₁ M] →
                    [inst_4 : CategoryTheory.HasShift C₂ M] →
                      [Φ.functor.CommShift M] →
                        {X₁ Y₁ : C₁} →
                          {X₂ Y₂ : C₂} →
                            [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁] →
                              [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂] →
                                [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂] →
                                  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] →
                                    (Φ.functor.obj X₁ ≅ X₂) →
                                      (Φ.functor.obj Y₁ ≅ Y₂) →
                                        {m : M} →
                                          CategoryTheory.Localization.SmallShiftedHom W₁ X₁ Y₁ m →
                                            CategoryTheory.Localization.SmallShiftedHom W₂ X₂ Y₂ m
-- Mathlib.Algebra.Category.Grp.Basic
/-- The underlying monoid homomorphism.  -/
AddGrpCat.Hom.hom' : {A B : AddGrpCat} → A.Hom B → ↑A →+ ↑B
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [CompactSpace α],
  (uniformity C(α, β)).HasBasis (fun V => V ∈ uniformity β) fun V => {fg | ∀ (x : α), (fg.1 x, fg.2 x) ∈ V}
-- Mathlib.Algebra.Ring.Regular
/-- A ring is Dedekind-finite if and only if every element has at most one left inverse.  -/
IsDedekindFiniteMonoid.iff_eq_of_mul_right_eq_one : ∀ {α : Type u_1} [inst : Ring α], IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decompose_symm_one : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring A]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜],
  (DirectSum.decompose 𝒜).symm 1 = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k k' : α}, cmp k k' = Ordering.eq → t.getKey! k = t.getKey! k'
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (s : Multiset α) (t : Multiset β),
  s.disjSum t = Multiset.map Sum.inl s + Multiset.map Sum.inr t
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.surjOn_iff_le_map : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂},
  Set.SurjOn ⇑f ↑p ↑q ↔ q ≤ Submodule.map f p
-- Mathlib.Analysis.Seminorm
Seminorm.instSemilatticeSup : {𝕜 : Type u_3} →
  {E : Type u_7} →
    [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → SemilatticeSup (Seminorm 𝕜 E)
-- Mathlib.CategoryTheory.ObjectProperty.Extensions
/-- Given `P : ObjectProperty C`, we say that `P` is closed under extensions
if whenever `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` is a short exact short complex,
then `P X₁` and `P X₃` implies `P X₂`.  -/
CategoryTheory.ObjectProperty.IsClosedUnderExtensions : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Mathlib.ModelTheory.Bundled
/-- A model of a theory is also a model of any subtheory.  -/
FirstOrder.Language.Theory.ModelType.subtheoryModel : {L : FirstOrder.Language} → {T : L.Theory} → T.ModelType → {T' : L.Theory} → T' ⊆ T → T'.ModelType
-- Init.Data.List.Range
List.range'.eq_1 : ∀ (x x_1 : ℕ), List.range' x 0 x_1 = []
-- Lean.Parser.Command
Lean.Parser.Command.in.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.toList.Perm t₂.toList → t₁ = t₂
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.mk.injEq : ∀ (toProfinite : Profinite) [addGroup : AddGroup ↑toProfinite.toTop]
  [topologicalAddGroup : IsTopologicalAddGroup ↑toProfinite.toTop] (toProfinite_1 : Profinite)
  (addGroup_1 : AddGroup ↑toProfinite_1.toTop) (topologicalAddGroup_1 : IsTopologicalAddGroup ↑toProfinite_1.toTop),
  ({ toProfinite := toProfinite, addGroup := addGroup, topologicalAddGroup := topologicalAddGroup } =
      { toProfinite := toProfinite_1, addGroup := addGroup_1, topologicalAddGroup := topologicalAddGroup_1 }) =
    (toProfinite = toProfinite_1 ∧ addGroup ≍ addGroup_1)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.num.sizeOf_spec : ∀ (k : ℤ), sizeOf (Lean.Grind.CommRing.Expr.num k) = 1 + sizeOf k
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unsafeRule.inj : ∀ {r r_1 : Aesop.UnsafeRule}, Aesop.BaseRuleSetMember.unsafeRule r = Aesop.BaseRuleSetMember.unsafeRule r_1 → r = r_1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m),
  (CochainComplex.mappingCone.liftCochain φ α β h).comp (CochainComplex.mappingCone.snd φ) ⋯ = β
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterM m α → Sort u_3) (x : α) (xs : List α)
  (h_1 : Unit → motive { internalState := { list := [] } })
  (h_2 : (x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }),
  (match { internalState := { list := x :: xs } } with
    | { internalState := { list := [] } } => h_1 ()
    | { internalState := { list := x :: xs } } => h_2 x xs) =
    h_2 x xs
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).toReal = OfNat.ofNat n
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- If `J : CardinalDirectedPoset κ` and `κ'` is any regular cardinal,
then `J.withTop` is the `κ'`-filtered colimit of its subsets that are of
cardinality `< κ'` and contain `⊤`.  -/
CategoryTheory.CardinalDirectedPoset.isColimitCoconeWithTop : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) →
      (κ' : Cardinal.{u}) → [inst_1 : Fact κ'.IsRegular] → CategoryTheory.Limits.IsColimit (J.coconeWithTop κ')
-- Mathlib.RingTheory.Adjoin.PowerBasis
/-- The elements `1, x, ..., x ^ (d - 1)` for a basis for the `K`-module `K[x]`,
where `d` is the degree of the minimal polynomial of `x`.  -/
Algebra.adjoin.powerBasisAux : {K : Type u_1} →
  {S : Type u_2} →
    [inst : Field K] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra K S] → {x : S} → IsIntegral K x → Module.Basis (Fin (minpoly K x).natDegree) K ↥K[x]
-- Mathlib.Tactic.NormDet
/-- Extract the entries of a square `!![...]` matrix literal in row-major order.
Returns `none` if `A` is not an `n × n` matrix literal.  -/
_private.Mathlib.Tactic.NormDet.0.entriesOfMatrixLiteral? : {u : Lean.Level} →
  {α : Q(Type u)} → {n : Q(ℕ)} → Q(Matrix (Fin «$n») (Fin «$n») «$α») → Lean.MetaM (Option (Array Q(«$α»)))
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_mul_C_of_isUnit : ∀ {R : Type u} {a : R} [inst : Semiring R],
  IsUnit a → ∀ (p : Polynomial R), (p * Polynomial.C a).natDegree = p.natDegree
-- Mathlib.RingTheory.SimpleRing.Basic
IsSimpleRing.one_mem_of_ne_zero_mem : ∀ {A : Type u_2} [inst : NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) {x : A}, x ≠ 0 → x ∈ I → 1 ∈ I
-- Init.Data.String.Iterate
String.Slice.ByteIterator.mk.sizeOf_spec : ∀ (s : String.Slice) (offset : String.Pos.Raw), sizeOf { s := s, offset := offset } = 1 + sizeOf s + sizeOf offset
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioo_inl_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a₁ a₂ : α),
  Finset.Ioo (Sum.inlₗ a₁) (Sum.inlₗ a₂) =
    Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ioo a₁ a₂)
-- Mathlib.Analysis.Fourier.AddCircle
/-- The linear span of the monomials `fourier n` is dense in `C(AddCircle T, ℂ)`.  -/
span_fourier_closure_eq_top : ∀ {T : ℝ} [hT : Fact (0 < T)], (Submodule.span ℂ (Set.range fourier)).topologicalClosure = ⊤
-- Init.Data.Array.Attach
Array.attach_eq_empty_iff : ∀ {α : Type u_1} {xs : Array α}, xs.attach = #[] ↔ xs = #[]
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioi_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n),
  ∏ i > Fin.cast h a, f i = ∏ i > a, f (Fin.cast h i)
-- Mathlib.Logic.Equiv.Prod
/-- Any `Unique` type is a right identity for type product up to equivalence.  -/
Equiv.prodUnique : (α : Type u_9) → (β : Type u_10) → [Unique β] → α × β ≃ α
-- Mathlib.Tactic.Ring.Common
/-- An atomic expression `e` with id `id`.

Atomic expressions are those which `ring` cannot parse any further.
For instance, `a + (a % b)` has `a` and `(a % b)` as atoms.
The `ring1` tactic does not normalize the subexpressions in atoms, but `ring_nf` does.

Atoms in fact represent equivalence classes of expressions, modulo definitional equality.
The field `index : ℕ` should be a unique number for each class,
while `e : Q($α)` contains a representative of this class.
 -/
Mathlib.Tactic.Ring.Common.ExBaseNat.atom : {e : Q(ℕ)} → ℕ → Mathlib.Tactic.Ring.Common.ExBaseNat e
-- Lean.Meta.Instances
Lean.Meta.DefaultInstanceEntry.mk.injEq : ∀ (className instanceName : Lean.Name) (priority : ℕ) (className_1 instanceName_1 : Lean.Name) (priority_1 : ℕ),
  ({ className := className, instanceName := instanceName, priority := priority } =
      { className := className_1, instanceName := instanceName_1, priority := priority_1 }) =
    (className = className_1 ∧ instanceName = instanceName_1 ∧ priority = priority_1)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS₂_mul_b : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ),
  complEDS₂ b c d k * b =
    normEDS b c d (k - 1) ^ 2 * normEDS b c d (k + 2) - normEDS b c d (k - 2) * normEDS b c d (k + 1) ^ 2
-- Mathlib.Order.InitialSeg
PrincipalSeg.mk : {α : Type u_4} →
  {β : Type u_5} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        (toRelEmbedding : r ↪r s) → (top : β) → (∀ (b : β), b ∈ Set.range ⇑toRelEmbedding ↔ s b top) → PrincipalSeg r s
-- Lean.Elab.Deriving.Util
/-- Return instance binder syntaxes binding `className α` for every generic parameter `α`
of the inductive `indVal` for which such a binding is type-correct. `argNames` is expected
to provide names for the parameters (see `mkInductArgNames`). The output matches `instBinder*`.

For example, given `inductive Foo {α : Type} (n : Nat) : (β : Type) → Type`, where `β` is an index,
invoking ``mkInstImplicitBinders `BarClass foo #[`α, `n, `β]`` gives `` `([BarClass α])``.  -/
Lean.Elab.Deriving.mkInstImplicitBinders : Lean.Name → Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.deriv_weierstrassPExcept_same : ∀ (L : PeriodPair) (l : ℂ), deriv (L.weierstrassPExcept l) l = L.derivWeierstrassPExcept l l
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKey! k = m.getKey! k
-- Mathlib.Tactic.ITauto
/-- Get a new name in the pattern `h0, h1, h2, ...`  -/
Mathlib.Tactic.ITauto.freshName : StateM ℕ Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_add_nat_mul_two_pi : ∀ (x : ℂ) (n : ℕ), Complex.sin (x + ↑n * (2 * ↑Real.pi)) = Complex.sin x