mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substInvFun.eq_3 : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)] (n : ℕ),
  (n = 0 → False) →
    P.substInvFun n.succ =
      -⅟((PowerSeries.coeff 1) P) *
        (PowerSeries.coeff (n + 1)) (PowerSeries.subst (∑ i, PowerSeries.C (P.substInvFun ↑i) * PowerSeries.X ^ ↑i) P)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_val_nd : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), (s₁ ∩ s₂).val = s₁.val.ndinter s₂.val
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1π_eq_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x y : ↥(groupHomology.cycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) x =
      (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) y ↔
    ↑x - ↑y ∈ groupHomology.boundaries₁ A
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] [inst_6 : Module R M]
  [inst_7 : Module R N] (P : RootPairing ι R M N) {x : M}, x ∈ P.rootSpan R → (P.RootForm x) x = 0 → x = 0
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.instEssSurjOppositeOp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.EssSurj], F.op.EssSurj
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.mul_smul_self_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] (X : C) [inst_3 : CategoryTheory.ModObj M X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.ModObj.smul)
      CategoryTheory.ModObj.smul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) CategoryTheory.ModObj.smul)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : CommGroup X] [inst_1 : CommGroup Y] (f : X →* Y),
  CommGrpCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.alter_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Hashable α]
  {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {k : α} {f : Option β → Option β},
  Std.DHashMap.Raw.Const.alter m k f = ↑(Std.DHashMap.Internal.Raw₀.Const.alter ⟨m, ⋯⟩ k f)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] [inst_6 : P.IsCrystallographic] {i : ι}, b.IsPos i → ∃ j ∈ b.support, 0 < P.pairingIn ℤ j i
-- Init.Data.Sum.Basic
Sum.getLeft?_inl : ∀ {α : Type u_1} {β : Type u_2} {x : α}, (Sum.inl x).getLeft? = some x
-- Mathlib.ModelTheory.LanguageMap
/-- The inclusion of an empty language into any other language.  -/
FirstOrder.Language.LHom.ofIsEmpty : (L : FirstOrder.Language) → (L' : FirstOrder.Language) → [L.IsAlgebraic] → [L.IsRelational] → L →ᴸ L'
-- Init.Grind.AC
Lean.Grind.AC.Seq.cons.injEq : ∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq) (x_1 : Lean.Grind.AC.Var) (s_1 : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons x s = Lean.Grind.AC.Seq.cons x_1 s_1) = (x = x_1 ∧ s = s_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      ∀ {k fallback : α},
        (t₁ ∩ t₂).getKeyD k fallback = if t₂.contains k = true then t₁.getKeyD k fallback else fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_erase_eq_iff_not_compare_maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey! = t.maxKey! ↔ ¬compare k t.maxKey! = Ordering.eq)
-- Mathlib.Order.Bounds.Basic
minimal_iff_isLeast : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {a : α}, Minimal (fun x => x ∈ s) a ↔ IsLeast s a
-- Aesop.Util.Tactic.Unfold
Aesop.tacticAesop_unfold_ : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.restrict_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s t : Set β}
  (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α),
  MeasurableSet t → ((κ.restrict hs) a) t = (κ a) (t ∩ s)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.IsCompatible.of_hom : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 2)} (g : (SSet.horn (n + 1) i).toSSet ⟶ X),
  SSet.horn.IsCompatible fun j hj => CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hj) g
-- Lean.Environment
/-- Checks whether a declaration named `n` may be added to the environment in the given context. See
also `AsyncContext.declPrefix`.
 -/
_private.Lean.Environment.0.Lean.AsyncContext.mayContain : Lean.AsyncContext✝ → Lean.Name → Bool
-- Mathlib.Algebra.Group.Prod
Prod.instDivisionMonoid.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : DivisionMonoid G] [inst_1 : DivisionMonoid H],
  Prod.instDivisionMonoid =
    { toDivInvMonoid := Prod.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- The representative is isomorphic to the original module.  -/
Module.Finite.reprEquivₛ : (R : Type u) →
  (M : Type u_1) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module.Finite R M] → Module.Finite.reprₛ R M ≃ₗ[R] M
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_def₂ : ∀ (x : GaussianInt), GaussianInt.toComplex x = { re := ↑x.re, im := ↑x.im }
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instBot : {α : Type u_1} → Bot (WithZero α)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.mono_left : ∀ {α : Type u_1} [inst : Preorder α] {x y : α},
  x ≤ y → ∀ {t : Ordnode α} {o : WithTop α}, Ordnode.Valid' (↑y) t o → Ordnode.Valid' (↑x) t o
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.eq_mul_inv_iff_mul_eq : ∀ {k : Type u_2} [inst : Field k] {φ₁ φ₂ φ₃ : PowerSeries k},
  PowerSeries.constantCoeff φ₃ ≠ 0 → (φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_filterMap_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ},
  m.WF →
    ((Std.DHashMap.Raw.filterMap f m).isEmpty = true ↔
      ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (Std.DHashMap.Raw.Const.get m k h) = none)
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.ins.match_1.eq_4 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (parent : RBTree.RBNode.Path α) (y : α)
  (b a : RBTree.RBNode α) (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_4 parent y b a
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
/-- A morphism of schemes `f : X ⟶ Y` is geometrically `P` if for any field `K` and
morphism `Spec K ⟶ Y`, the base change `X ×[Y] Spec K` satisfies `P`.  -/
AlgebraicGeometry.geometrically : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme → CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Mathlib.Analysis.Convex.TotallyBounded
totallyBounded_convexHull : ∀ {E : Type u_1} {s : Set E} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : UniformSpace E]
  [IsUniformAddGroup E] [LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E],
  TotallyBounded ((convexHull ℝ) s) ↔ TotallyBounded s
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Get the `j`th "injection" in the cofan.
(Note that the initial letter of `inj` matches the greek letter in `Cocone.ι`.)  -/
CategoryTheory.Limits.Cofan.inj : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] → {f : β → C} → (p : CategoryTheory.Limits.Cofan f) → (j : β) → f j ⟶ p.pt
-- Batteries.Data.Array.Basic
/-- Find the first minimal element of an array. If the array is empty, `default` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.rangeMinI : {α : Type u_1} → [ord : Ord α] → [Inhabited α] → (xs : Array α) → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.Data.Set.Basic
Set.Nonempty.inr : ∀ {α : Type u} {s t : Set α}, t.Nonempty → (s ∪ t).Nonempty
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'TR.go.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (bs : List β)
  (acc : Array γ) (h_1 : (bs : List β) → (acc : Array γ) → motive [] bs acc)
  (h_2 : (as : List α) → (acc : Array γ) → motive as [] acc)
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc),
  (match [], bs, acc with
    | [], bs, acc => h_1 bs acc
    | as, [], acc => h_2 as acc
    | a :: as, b :: bs, acc => h_3 a as b bs acc) =
    h_1 bs acc
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.smulRightₗ.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Module R S] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₂] [inst_6 : Module S M₂]
  [inst_7 : IsScalarTower R S M₂] [inst_8 : TopologicalSpace S] [inst_9 : TopologicalSpace M₂]
  [inst_10 : ContinuousSMul S M₂] [inst_11 : TopologicalSpace M] [inst_12 : AddCommMonoid M] [inst_13 : Module R M]
  [inst_14 : ContinuousAdd M₂] [inst_15 : Module T M₂] [inst_16 : ContinuousConstSMul T M₂]
  [inst_17 : SMulCommClass R T M₂] [inst_18 : SMulCommClass S T M₂] (c c_1 : M →L[R] S),
  c = c_1 → c.smulRightₗ = c_1.smulRightₗ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The first left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction₂.fst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₂ X Y → W.LeftFraction X Y
-- Mathlib.GroupTheory.Commutator.Basic
conj_eq_commutatorElement_mul : ∀ {G : Type u_1} [inst : Group G] {g₁ g₂ : G}, (MulAut.conj g₁) g₂ = ⁅g₁, g₂⁆ * g₂
-- Mathlib.Lean.Expr.Basic
/-- Given `f a₀ a₁ ... aₙ₋₁`, sets the argument on the `i`th argument to `x` or
returns the original expression if out of bounds.  -/
Lean.Expr.setArg : (e : Lean.Expr) → ℕ → Lean.Expr → optParam ℕ e.getAppNumArgs → Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_add : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] (A B : Matrix n n R),
  (A + B).trace = A.trace + B.trace
-- Mathlib.CategoryTheory.Limits.Connected
/-- (Impl).
Given a cone for (X × K -), produce a cone for K using the natural transformation `γ₂`  -/
CategoryTheory.ProdPreservesConnectedLimits.forgetCone : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      {J : Type v₂} →
        [inst_2 : CategoryTheory.SmallCategory J] →
          {X : C} →
            {K : CategoryTheory.Functor J C} →
              CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X)) →
                CategoryTheory.Limits.Cone K
-- Mathlib.Data.Complex.Basic
Complex.conj_natCast : ∀ (n : ℕ), (starRingEnd ℂ) ↑n = ↑n
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsOrtho.eq_1 : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : CommSemiring R₁] [inst_2 : AddCommMonoid M₁] [inst_3 : Module R₁ M₁] [inst_4 : CommSemiring R₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₂ M₂] [inst_7 : AddCommMonoid M] [inst_8 : Module R M] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) (x : M₁) (y : M₂), B.IsOrtho x y = ((B x) y = 0)
-- Lean.Parser.Term
Lean.Parser.Term.posConfigItem.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  k ∈ Std.ExtHashMap.filterMap f m ↔ ∃ (h : k ∈ m), (f (m.getKey k h) m[k]).isSome = true
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_smul : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {R : Type u_2} [inst_1 : SMul R NNReal] [inst_2 : SMul R ENNReal]
  [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [inst_5 : TopologicalSpace Ω]
  [OpensMeasurableSpace Ω] [IsScalarTower R NNReal NNReal] [inst_8 : PseudoMetricSpace R] [inst_9 : Zero R]
  [inst_10 : IsBoundedSMul R NNReal] (μ : MeasureTheory.FiniteMeasure Ω) (c : R)
  (f : BoundedContinuousFunction Ω NNReal), μ.testAgainstNN (c • f) = c • μ.testAgainstNN f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_insertIfNew_le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {km kmi : α}, t.minKey? = some km → (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.linearIndependent_single : ∀ (p : ENNReal) (𝕜 : Type u_1) [inst : Semiring 𝕜] {η : Type u_5} {ιs : η → Type u_6} {Ms : η → Type u_7}
  [inst_1 : (i : η) → AddCommGroup (Ms i)] [inst_2 : (i : η) → Module 𝕜 (Ms i)] [inst_3 : DecidableEq η]
  (v : (j : η) → ιs j → Ms j),
  (∀ (i : η), LinearIndependent 𝕜 (v i)) → LinearIndependent 𝕜 fun ji => PiLp.single p ji.fst (v ji.fst ji.snd)
-- Mathlib.Algebra.Group.ULift
ULift.cancelMonoid.eq_1 : ∀ {α : Type u} [inst : CancelMonoid α], ULift.cancelMonoid = Function.Injective.cancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldRev_eq : ∀ {α : Type u} {β : α → Type v} {γ : Type w} {l : Std.DHashMap.Raw α β} {f : γ → (a : α) → β a → γ} {init : γ},
  Std.DHashMap.Raw.Internal.foldRev f init l =
    Array.foldr (fun l acc => Std.DHashMap.Internal.AssocList.foldr (fun a b g => f g a b) acc l) init l.buckets
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A : C} {a : A ⟶ G.obj A}
  {counit :
    autoParam (CategoryTheory.CategoryStruct.comp a (G.ε.app A) = CategoryTheory.CategoryStruct.id A)
      CategoryTheory.Comonad.Coalgebra.counit._autoParam}
  {coassoc :
    autoParam (CategoryTheory.CategoryStruct.comp a (G.δ.app A) = CategoryTheory.CategoryStruct.comp a (G.map a))
      CategoryTheory.Comonad.Coalgebra.coassoc._autoParam}
  {A_1 : C} {a_1 : A_1 ⟶ G.obj A_1}
  {counit_1 :
    autoParam (CategoryTheory.CategoryStruct.comp a_1 (G.ε.app A_1) = CategoryTheory.CategoryStruct.id A_1)
      CategoryTheory.Comonad.Coalgebra.counit._autoParam}
  {coassoc_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp a_1 (G.δ.app A_1) = CategoryTheory.CategoryStruct.comp a_1 (G.map a_1))
      CategoryTheory.Comonad.Coalgebra.coassoc._autoParam},
  { A := A, a := a, counit := counit, coassoc := coassoc } =
      { A := A_1, a := a_1, counit := counit_1, coassoc := coassoc_1 } →
    A = A_1 ∧ a ≍ a_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPullback.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C}, sq.IsPullback → sq.op.IsPushout
-- Mathlib.Algebra.Torsor.Basic
/-- If dividing the same point by two points produces equal results, those points are equal.  -/
sdiv_right_cancel : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {p₁ p₂ p : P}, p /ₛ p₁ = p /ₛ p₂ → p₁ = p₂
-- Init.Internal.Order.Basic
Lean.Order.admissible_apply : ∀ {α : Sort u} {β : α → Sort v} [inst : (x : α) → Lean.Order.CCPO (β x)] (P : (x : α) → β x → Prop) (x : α),
  Lean.Order.admissible (P x) → Lean.Order.admissible fun f => P x (f x)
-- Mathlib.Order.Restriction
Preorder.frestrictLe_updateFinset_of_le : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] [inst_2 : DecidableEq α]
  {a b : α} (hab : a ≤ b) (x : (c : α) → π c) (y : (c : ↥(Finset.Iic b)) → π ↑c),
  Preorder.frestrictLe a (Function.updateFinset x (Finset.Iic b) y) = Preorder.frestrictLe₂ hab y
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabSynth : Lean.Elab.Command.CommandElab
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
QuadraticMap.lift_mk : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} {N : Submodule R M} (hN : N ≤ Q.radical) (m : M),
  (Q.lift N hN) (Submodule.Quotient.mk m) = Q m
-- Mathlib.Data.PFun
PFun.preimage_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (s : Set γ),
  (f.comp g).preimage s = g.preimage (f.preimage s)
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The morphism `ιFunctorObj f πX : X ⟶ functorObj f πX` is obtained by
attaching `f`-cells.  -/
CategoryTheory.SmallObject.attachCellsιFunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                [inst_2 :
                    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
                      (CategoryTheory.SmallObject.functorObjLeft f πX)] →
                  HomotopicalAlgebra.AttachCells f (CategoryTheory.SmallObject.ιFunctorObj f πX)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffWithinAt.pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_3 : NormedRing 𝔸]
  [inst_4 : NormedAlgebra 𝕜 𝔸] {f : E → 𝔸},
  ContDiffWithinAt 𝕜 n f s x → ∀ (m : ℕ), ContDiffWithinAt 𝕜 n (fun y => f y ^ m) s x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.ε_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Grp.forget₂Mon C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon C))
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_rat`. -/
LinearOrderedField.inducedMap_rat : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (q : ℚ),
  ConditionallyCompleteLinearOrderedField.inducedMap α β ↑q = ↑q
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.nonsingular_transpose_iff : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  {A : Matrix n n R}, A.transpose.Nonsingular ↔ A.Nonsingular
-- Mathlib.Order.CompleteBooleanAlgebra
PUnit.sSup_eq : ∀ (s : Set PUnit.{u + 1}), sSup s = PUnit.unit
-- Mathlib.Topology.Connected.Clopen
/-- In a preconnected set, given a transitive relation `P`, if `P x y` and `P y x` are true
for `y` close enough to `x`, then `P x y` holds for all `x, y`. This is a version of the fact
that, if an equivalence relation has open classes, then it has a single equivalence class.  -/
IsPreconnected.induction₂' : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsPreconnected s →
    ∀ (P : α → α → Prop),
      (∀ x ∈ s, ∀ᶠ (y : α) in nhdsWithin x s, P x y ∧ P y x) →
        (∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) → ∀ {x y : α}, x ∈ s → y ∈ s → P x y
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromy.congr_simp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x y : X} (γ γ_1 : Path.Homotopic.Quotient x y),
  γ = γ_1 → ∀ (a a_1 : ↑(p ⁻¹' {x})), a = a_1 → cov.monodromy γ a = cov.monodromy γ_1 a_1
-- Mathlib.Tactic.ArithMult
/-- `arith_mult` solves goals of the form `IsMultiplicative f` for `f : ArithmeticFunction R`
by applying lemmas tagged with the user attribute `arith_mult`.  -/
ArithmeticFunction.arith_mult : Lean.ParserDescr
-- Mathlib.Algebra.Torsor.Basic
Prod.instAddTorsor.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'],
  Prod.instAddTorsor =
    { vadd := fun v p => (v.1 +ᵥ p.1, v.2 +ᵥ p.2), add_vadd := ⋯, zero_vadd := ⋯,
      vsub := fun p₁ p₂ => (p₁.1 -ᵥ p₂.1, p₁.2 -ᵥ p₂.2), nonempty := ⋯, vsub_vadd' := ⋯, vadd_vsub' := ⋯ }
-- Mathlib.Order.SuccPred.Basic
Order.Iic_subset_Iio_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α), Set.Iic a ⊆ Set.Iio (Order.succ a)
-- Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Finset.sum_preimage' : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [inst : AddCommMonoid β] (f : ι → κ)
  [inst_1 : DecidablePred fun x => x ∈ Set.range f] (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β),
  ∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ s with x ∈ Set.range f, g x
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.instInhabitedEdgeLabeling : {V : Type u_1} → {G : SimpleGraph V} → {K : Type u_3} → [Inhabited K] → Inhabited (G.EdgeLabeling K)