mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.exp_sub_sum_range_isBigO_pow : ∀ (n : ℕ), (fun x => Complex.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial) =O[nhds 0] fun x => x ^ n
-- Mathlib.Order.Filter.Basic
Filter.principal_eq_bot_iff : ∀ {α : Type u} {s : Set α}, Filter.principal s = ⊥ ↔ s = ∅
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A correspondence `f : α → Set β` has open lower sections if and only if its *lower inverse*
(i.e., `b : β ↦ (f ⁻¹' Iic {b}ᶜ)ᶜ = {x | b ∈ f x}`) sends every point to an open set.  -/
hasOpenLowerSections_iff_isOpen_compl_preimage_Iic_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β},
  HasOpenLowerSections f ↔ ∀ (b : β), IsOpen (f ⁻¹' Set.Iic {b}ᶜ)ᶜ
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.mk.inj : ∀ {V : Type u₁} {inst : CategoryTheory.ReflQuiver V} {W : Type u₂} {inst_1 : CategoryTheory.ReflQuiver W}
  {toPrefunctor : V ⥤q W}
  {map_id :
    autoParam
      (∀ (X : V), toPrefunctor.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (toPrefunctor.obj X))
      CategoryTheory.ReflPrefunctor.map_id._autoParam}
  {toPrefunctor_1 : V ⥤q W}
  {map_id_1 :
    autoParam
      (∀ (X : V),
        toPrefunctor_1.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (toPrefunctor_1.obj X))
      CategoryTheory.ReflPrefunctor.map_id._autoParam},
  { toPrefunctor := toPrefunctor, map_id := map_id } = { toPrefunctor := toPrefunctor_1, map_id := map_id_1 } →
    toPrefunctor = toPrefunctor_1
-- Mathlib.Order.CompleteLattice.Basic
sInf_union : ∀ {α : Type u_1} [inst : CompleteLattice α] {s t : Set α}, sInf (s ∪ t) = sInf s ⊓ sInf t
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.mahlerTerm.congr_simp : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] (a a_1 : E),
  a = a_1 → ∀ (n n_1 : ℕ), n = n_1 → PadicInt.mahlerTerm a n = PadicInt.mahlerTerm a_1 n_1
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_neg : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (a : PadicSeq p), (-a).norm = a.norm
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).leadingCoeff = a
-- Mathlib.Data.List.Sigma
List.mem_keys_kunion : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)},
  a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIccQuot_comp_mk_eq_toIocMod : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜] (p a : 𝕜)
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜],
  ⇑(AddCircle.equivIccQuot p a) ∘ Quotient.mk'' = fun x => Quot.mk (AddCircle.EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
-- Std.Do.WP.SimpLemmas
Option.tryCatch.eq_1 : ∀ {α : Type u_1} (handle : Unit → Option α) (val : α), (some val).tryCatch handle = some val
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.mkSimprocAttr : Lean.Name → String → Lean.Meta.Simp.SimprocExtension → Lean.Name → IO Unit
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_update : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ) (a : R) [inst_1 : DecidableEq R],
  (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- `K.homology i` is the kernel of `K.fromOpcycles i j : K.opcycles i ⟶ K.X j`
when `c.next i = j`.  -/
HomologicalComplex.homologyIsKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) →
              [inst_2 : K.HasHomology i] →
                c.next i = j → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (K.homologyι i) ⋯)
-- Mathlib.Topology.NhdsSet
tendsto_nhdsSet_of_tendsto_nhds : ∀ {α : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {f : α → X} {l : Filter α} {x : X},
  x ∈ s → Filter.Tendsto f l (nhds x) → Filter.Tendsto f l (nhdsSet s)
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (β : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk sq₁₃.π) {Z : C₃}
  (h : (CategoryTheory.Arrow.mk f₃).left ⟶ Z),
  CategoryTheory.CategoryStruct.comp sq₁₂.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β)) h) =
    CategoryTheory.CategoryStruct.comp (adj₂.homEquiv.symm (CategoryTheory.Arrow.Hom.left β)) h
-- Std.Time.Internal.Bounded
/-- Convert a `Bounded.LE` to a Nat.
 -/
Std.Time.Internal.Bounded.LE.toNat' : {lo hi : ℤ} → Std.Time.Internal.Bounded.LE lo hi → lo ≥ 0 → ℕ
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.instInhabitedShouldCanonResult : Inhabited Lean.Meta.Sym.Canon.ShouldCanonResult✝
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.DecompositionResult.comp.inj : ∀ {f g f_1 g_1 : Lean.Expr},
  Mathlib.Meta.FunProp.DecompositionResult.comp f g = Mathlib.Meta.FunProp.DecompositionResult.comp f_1 g_1 →
    f = f_1 ∧ g = g_1
-- Lean.Elab.DefView
/-- Result of body elaboration.  -/
Lean.Elab.HeaderProcessedSnapshot.bodySnap : Lean.Elab.HeaderProcessedSnapshot → Lean.Language.SnapshotTask (Option Lean.Elab.BodyProcessedSnapshot)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.hasZeroObject_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.HasZeroObject Cᵒᵖ
-- Lean.Parser.Term
Lean.Parser.Term.funImplicitBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey?ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α β) (k : α),
  l.getKey?ₘ k = Std.DTreeMap.Internal.Impl.applyCell k l fun c x => c.getKey?
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.comm : ∀ {n a b : ℕ}, a ≡ b [MOD n] ↔ b ≡ a [MOD n]
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_div : ∀ {a b : ℕ} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8), UInt8.ofNatLT (a / b) ⋯ = UInt8.ofNatLT a ha / UInt8.ofNatLT b hb
-- Mathlib.Algebra.Group.Basic
add_sub_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a + (b - a) = b
-- Mathlib.Algebra.Algebra.Hom
AlgHom.comp_toLinearMap : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (g : B →ₐ[R] C), (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.
 -/
Std.ExtDTreeMap.maxEntry : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → t ≠ ∅ → (a : α) × β a
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The morphism that is part of an object in `Under X`.  -/
CategoryTheory.Under.hom : {T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → {X : T} → (f : CategoryTheory.Under X) → X ⟶ f.right
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.CodescendsAlong.of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q W : CategoryTheory.MorphismProperty C}
  [P.CodescendsAlong Q], W ≤ Q → P.CodescendsAlong W
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0)
  (hg₂ : S₂.g = 0), (CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φK = φ.τ₂
-- Mathlib.FieldTheory.PrimitiveElement
Field.exists_primitive_element_of_finite_intermediateField : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [Finite (IntermediateField F E)] (K : IntermediateField F E), ∃ α, F⟮α⟯ = K
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.minpoly_frobeniusAlgHom : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [Finite L], minpoly K (FiniteField.frobeniusAlgHom K L).toLinearMap = Polynomial.X ^ Module.finrank K L - 1
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of a face of a `spineToSimplex`, the
arrows not contained in the original path can be recovered as the diagonal edge
of the `spineToSimplex` that "composes" arrows `i` and `i + 1`.  -/
SSet.StrictSegal.spine_δ_arrow_eq : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin n} {j : Fin (n + 2)},
  j = i.succ.castSucc →
    (X.spine n
            ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X j)) (sx.spineToSimplex f))).arrow
        i =
      sx.spineToDiagonal (f.interval (↑i) 2 ⋯)
-- Mathlib.SetTheory.Cardinal.ToNat
/-- `toNat` has a right-inverse: coercion.  -/
Cardinal.toNat_rightInverse : Function.RightInverse Nat.cast ⇑Cardinal.toNat
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Ico : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Finset.Ico a b ↔ a ≤ x ∧ x < b
-- Mathlib.Order.Filter.IsBounded
Filter.isCoboundedUnder_le_add : ∀ {α : Type u_5} {R : Type u_6} [inst : LinearOrder R] [inst_1 : Add R] {f : Filter α} [f.NeBot] [AddLeftMono R]
  [AddRightMono R] {u v : α → R},
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The value of `weightedVSubOfPoint`, where the given points are equal.  -/
Finset.weightedVSubOfPoint_apply_const : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p b : P),
  (s.weightedVSubOfPoint (fun x => p) b) w = (∑ i ∈ s, w i) • (p -ᵥ b)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
/-- A set is simply connected iff it's path connected
and any loop is homotopic to the constant path within `s`.  -/
isSimplyConnected_iff_exists_homotopy_refl_forall_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsSimplyConnected s ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.monoid : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : Monoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffMul I' n G] → Monoid (ContMDiffMap I I' N G n)
-- Mathlib.Tactic.Translate.Core
/-- `RelevantArg` represents an optional argument that should be checked to determine
whether or not to translate the given constant.  -/
Mathlib.Tactic.Translate.RelevantArg : Type
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow.match_1.congr_eq_3 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ)
  (k_1 : ℕ),
  k = k_1.succ →
    (k_1 = 0 → False) →
      (match k with
        | 0 => h_1 ()
        | 1 => h_2 ()
        | k.succ => h_3 k) ≍
        h_3 k_1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.prod_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) (m : (i : ι) → M₁ i),
  (f.prod g) m = (f m, g m)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.mk_nat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] (N : AddSubgroup R) [inst_1 : N.Normal] (n : ℕ) (a : R), ↑(↑n * a) = n • ↑a
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.leftUnitor_inv_out_app : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.leftUnitor F).inv.out.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.coe_refl : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : Add α], ⇑(OrderAddMonoidIso.refl α) = id
-- Init.Data.SInt.Lemmas
Int8.le_iff_toInt_le : ∀ {x y : Int8}, x ≤ y ↔ x.toInt ≤ y.toInt
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Simplex.scalene_reindex_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {m n : ℕ}
  {s : Affine.Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)), (s.reindex e).Scalene ↔ s.Scalene
-- Mathlib.Data.Nat.Choose.Factorization
/-- A logarithmic upper bound on the multiplicity of a prime in a binomial coefficient.  -/
Nat.factorization_choose_le_log : ∀ {p n k : ℕ}, (n.choose k).factorization p ≤ Nat.log p n
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
/-- An equivalence between the "proxy type" `CategoryTheory.Limits.WalkingMultispan.proxyType` and `CategoryTheory.Limits.WalkingMultispan`. The proxy type is a reducible definition that represents the inductive type using `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum` (and whatever other inductive types appear within the inductive type), and the intended use is to define typeclass instances uses pre-existing instances on these. (Generated by the `proxy_equiv%` elaborator.) -/
CategoryTheory.Limits.WalkingMultispan.proxyTypeEquiv : (J : CategoryTheory.Limits.MultispanShape) → J.L ⊕ J.R ≃ CategoryTheory.Limits.WalkingMultispan J
-- Init.Simproc
/-- A user-defined defeq simplification procedure declaration. To activate this procedure in `simp` tactic,
we must provide it as an argument, or use the command `attribute` to set its `[simproc]` attribute.
 -/
Lean.Parser.«command_Dsimproc_decl_(_):=_» : Lean.ParserDescr
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_toAddSubgroup : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), f.range.toAddSubgroup = f.toAddMonoidHom.range
-- Mathlib.SetTheory.Cardinal.Free
instInfiniteFreeAbelianGroupOfNonempty : ∀ (α : Type u) [Nonempty α], Infinite (FreeAbelianGroup α)
-- Lean.Parser.Command
Lean.Parser.Command.public.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.Grp.Basic
MulEquiv.toCommGrpIso.eq_1 : ∀ {X Y : CommGrpCat} (e : ↑X ≃* ↑Y),
  e.toCommGrpIso =
    { hom := CommGrpCat.ofHom e.toMonoidHom, inv := CommGrpCat.ofHom e.symm.toMonoidHom, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.equivalenceJ_counitIso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃),
  (w.equivalenceJ g).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).comp (CategoryTheory.TwoSquare.EquivalenceJ.functor w g))
-- Mathlib.Order.Rel.GaloisConnection
/-- The maps `leftDual` and `rightDual` induce inverse bijections between the sets of fixed points.
 -/
SetRel.equivFixedPoints : {α : Type u_1} → {β : Type u_2} → (R : SetRel α β) → ↑R.leftFixedPoints ≃ ↑R.rightFixedPoints
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite limits, then `F : C ⥤ D` reflects finite colimits.  -/
CategoryTheory.Limits.reflectsFiniteColimits_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteLimits F.op],
  CategoryTheory.Limits.ReflectsFiniteColimits F
-- Mathlib.Combinatorics.SimpleGraph.Matching
/-- Given a vertex with one edge in a graph of cycles this gives the other edge incident
to the same vertex.
 -/
SimpleGraph.IsCycles.other_adj_of_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {v w : V}, G.IsCycles → G.Adj v w → ∃ w', w ≠ w' ∧ G.Adj v w'
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.multispan.match_1.eq_3 : ∀ {J : CategoryTheory.Limits.MultispanShape}
  (motive : (x y : CategoryTheory.Limits.WalkingMultispan J) → (x ⟶ y) → Sort u_3) (b : J.L)
  (h_1 : (x : CategoryTheory.Limits.WalkingMultispan J) → motive x x (CategoryTheory.Limits.WalkingMultispan.Hom.id x))
  (h_2 :
    (b : J.L) →
      motive (CategoryTheory.Limits.WalkingMultispan.left b) (CategoryTheory.Limits.WalkingMultispan.right (J.fst b))
        (CategoryTheory.Limits.WalkingMultispan.Hom.fst b))
  (h_3 :
    (b : J.L) →
      motive (CategoryTheory.Limits.WalkingMultispan.left b) (CategoryTheory.Limits.WalkingMultispan.right (J.snd b))
        (CategoryTheory.Limits.WalkingMultispan.Hom.snd b)),
  (match CategoryTheory.Limits.WalkingMultispan.left b, CategoryTheory.Limits.WalkingMultispan.right (J.snd b),
      CategoryTheory.Limits.WalkingMultispan.Hom.snd b with
    | x, .(x), CategoryTheory.Limits.WalkingMultispan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMultispan.left b), .(CategoryTheory.Limits.WalkingMultispan.right (J.fst b)),
      CategoryTheory.Limits.WalkingMultispan.Hom.fst b => h_2 b
    | .(CategoryTheory.Limits.WalkingMultispan.left b), .(CategoryTheory.Limits.WalkingMultispan.right (J.snd b)),
      CategoryTheory.Limits.WalkingMultispan.Hom.snd b => h_3 b) =
    h_3 b
-- Mathlib.Tactic.TacticAnalysis
/-- A tactic analysis framework.
It is aimed at allowing developers to specify refactoring patterns,
which will be tested against a whole project,
to report proposed changes.

It hooks into the linting system to move through the infotree,
collecting tactic syntax and state to call the passes on.
 -/
Mathlib.TacticAnalysis.tacticAnalysis : Lean.Linter
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_sub : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2]
  (f g : P1 →ᵃ[k] V2), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Algebra.Algebra.Hom
AlgHom.comp_apply : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A), (φ₁.comp φ₂) p = φ₁ (φ₂ p)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.restr_source : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : Equidecomp X G) (A : Set X), (f.restr A).source = f.source ∩ A
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.conjCLE_nnorm : ‖↑Complex.conjCLE‖₊ = 1
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.coeff_pderivFun : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {i : σ} (f : MvPowerSeries σ R) (d : σ →₀ ℕ),
  (MvPowerSeries.coeff d) (MvPowerSeries.pderivFun i f) = (MvPowerSeries.coeff (d + fun₀ | i => 1)) f * (↑(d i) + 1)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.containsThenInsert_snd : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.containsThenInsert k).2 = t.insert k
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Lift an `R`-balanced map to the tensor product.
A map `f : M →+ N →+ P` additive in both components is `R`-balanced, or middle linear with respect
to `R`, if scalar multiplication in either argument is equivalent, `f (r • m) n = f m (r • n)`.
Note that strictly the first action should be a right-action by `R`, but for now `R` is commutative
so it doesn't matter.  -/
TensorProduct.liftAddHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        {P : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    (f : M →+ N →+ P) →
                      (∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)) → TensorProduct R M N →+ P
-- Mathlib.Algebra.Star.StarAlgHom
/-- Turn an element of a type `F` satisfying `AlgHomClass F R A B` and `StarHomClass F A B` into an
actual `StarAlgHom`. This is declared as the default coercion from `F` to `A →⋆ₐ[R] B`.  -/
StarAlgHomClass.toStarAlgHom : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Star A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] → [AlgHomClass F R A B] → [StarHomClass F A B] → F → A →⋆ₐ[R] B
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.ext_iff : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B},
  f = g ↔ autoParam (f.f = g.f) CategoryTheory.DifferentialObject.ext._auto_1