mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.isEmpty = true → ∀ {fallback : α}, (t.insert k).minD fallback = k
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instMulActionAutObjFiniteVFintypeCatFunctorObjActionFunctorToAction : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      (X : C) → MulAction (CategoryTheory.Aut X) ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X).V.obj
-- Batteries.Control.Nondet.Basic
/-- `Nondet m` is an alternative monad.  -/
Nondet.instAlternativeMonad : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → AlternativeMonad (Nondet m)
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- The function `fun x => x⁻¹` is integrable on `a..b` if and only if
`a = b` or `0 ∉ [a, b]`.  -/
intervalIntegrable_inv_iff : ∀ {a b : ℝ}, IntervalIntegrable (fun x => x⁻¹) MeasureTheory.volume a b ↔ a = b ∨ 0 ∉ Set.uIcc a b
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `MonoidHom.domRestrict_mker`. -/
MonoidHom.restrict_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) (f : M →* N),
  MonoidHom.mker (f.domRestrict S) = Submonoid.comap S.subtype (MonoidHom.mker f)
-- Mathlib.Order.Filter.Basic
Filter.instTransForallEventuallyEq : {α : Type u} →
  {β : Type v} → {l : Filter α} → Trans (fun x1 x2 => x1 =ᶠ[l] x2) (fun x1 x2 => x1 =ᶠ[l] x2) fun x1 x2 => x1 =ᶠ[l] x2
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.Error.expectedToString : List String → String
-- Mathlib.Algebra.Algebra.Hom
AlgHom.cancel_right : ∀ {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]
  {g₁ g₂ : B →ₐ[R] C} {f : A →ₐ[R] B}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofFiniteAddGrp.eq_1 : ∀ (G : FiniteAddGrp.{u_1}), ProfiniteAddGrp.ofFiniteAddGrp G = ProfiniteAddGrp.of ↑G.toAddGrp
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : PartialEquivBEq α] [inst_3 : Std.LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α}
  {h' : k ∈ t.insertMany l},
  (t.insertMany l)[k] =
    match w :
      List.findSomeRev?
        (fun x =>
          match x with
          | (a, b) => if cmp a k = Ordering.eq then some b else none)
        l with
    | some v => v
    | none => t[k]
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.mapM.map.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m β) (as : Array α) (i : ℕ) (bs : Array β),
  Array.mapM.map✝ f as i bs =
    if hlt : i < as.size then do
      let __do_lift ← f as[i]
      Array.mapM.map✝ f as (i + 1) (bs.push __do_lift)
    else pure bs
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- A predicate stating the sufficient conditions on an implicit equation `f : E₁ × E₂ → F` that
will lead to a $C^n$ implicit function `ψ : E₁ → E₂`.  -/
IsContDiffImplicitAt : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E₁ : Type u_2} →
      [inst_1 : NormedAddCommGroup E₁] →
        [inst_2 : NormedSpace 𝕜 E₁] →
          {E₂ : Type u_3} →
            [inst_3 : NormedAddCommGroup E₂] →
              [inst_4 : NormedSpace 𝕜 E₂] →
                {F : Type u_4} →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] → WithTop ℕ∞ → (E₁ × E₂ → F) → (E₁ × E₂ →L[𝕜] F) → E₁ × E₂ → Prop
-- Mathlib.Data.FinEnum
FinEnum.PSigma.finEnumPropProp : {α : Prop} → {β : α → Prop} → [Decidable α] → [(a : α) → Decidable (β a)] → FinEnum ((a : α) ×' β a)
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Polynomial.residueFieldMapCAlgEquiv.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime] (J : Ideal (Polynomial R)) [inst_2 : J.IsPrime]
  [inst_3 : J.LiesOver I] [inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
  [inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J] (hJ : J = Ideal.map Polynomial.C I),
  Polynomial.residueFieldMapCAlgEquiv I J hJ = Polynomial.residueFieldMapCAlgEquiv I J hJ
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.one_eq : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] (x : Submonoid A), 1 = Quotient.mk'' 1
-- Lean.Elab.Attributes
Lean.Elab.elabAttr : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadResolveName m] →
        [Lean.MonadError m] →
          [Lean.Elab.MonadMacroAdapter m] →
            [Lean.MonadRecDepth m] →
              [Lean.MonadTrace m] →
                [Lean.MonadOptions m] →
                  [Lean.AddMessageContext m] →
                    [MonadLiftT IO m] → [MonadFinally m] → Lean.Syntax → m Lean.Elab.Attribute
-- Init.Data.UInt.Basic
/-- Converts an `Int` to a `UInt64` by taking the (non-negative remainder of the division by `2 ^ 64`.  -/
UInt64.ofInt : ℤ → UInt64
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.IterM.Partial.size : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → [Monad m] → Std.IterM.Partial m β → m (ULift.{w, 0} ℕ)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.π_map : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A n) (groupHomology.map f φ n) =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ n) (groupHomology.π B n)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t'_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j k : D.J),
  CategoryTheory.IsIso (D.t' i j k)
-- Mathlib.Topology.Algebra.MulAction
instContinuousSMulForall_1 : ∀ {ι : Type u_5} {γ : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (γ i)] {N : ι → Type u_7}
  [inst_1 : (i : ι) → TopologicalSpace (N i)] [inst_2 : (i : ι) → SMul (N i) (γ i)]
  [∀ (i : ι), ContinuousSMul (N i) (γ i)], ContinuousSMul ((i : ι) → N i) ((i : ι) → γ i)
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Basic theoretical "normal form" object of the `field_simp` tactic: a type
synonym for a list of ordered pairs in `ℤ × M`, where typically `M` is a field.  This is the
form to which the tactics reduce field expressions.  -/
Mathlib.Tactic.FieldSimp.NF : Type u_1 → Type u_1
-- Lean.Meta.Sym.DSimp.DSimpM
/-- The result of definitionally simplifying an expression `e`.

The `done` flag controls whether simplification should continue after this result:
- `done = false` (default): Continue with subsequent simplification steps. If a
  `pre`/`post` method returns `.step e' false`, `dsimp` recurses on `e'`.
- `done = true`: Stop processing, return this result as final.

Unlike `Sym.Simp.Result`, this carries no proof term and no `contextDependent` flag.
 -/
Lean.Meta.Sym.DSimp.Result : Type
-- Init.Data.Fin.Lemmas
Fin.addNat_mk : ∀ {m : ℕ} (n i : ℕ) (hi : i < m), ⟨i, hi⟩.addNat n = ⟨i + n, ⋯⟩
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {h e f : L}
  {m : M} {μ : R} {t : IsSl2Triple h e f},
  t.HasPrimitiveVectorWith m μ →
    ∀ (n : ℕ), ⁅f, ((LieModule.toEnd R L M) f ^ n) m⁆ = ((LieModule.toEnd R L M) f ^ (n + 1)) m
-- Mathlib.NumberTheory.FLT.Polynomial
_private.Mathlib.NumberTheory.FLT.Polynomial.0.Ne.isUnit_C : ∀ {k : Type u_1} [inst : Field k] {u : k}, u ≠ 0 → IsUnit (Polynomial.C u)
-- Init.Data.SInt.Lemmas
Int16.add_right_inj : ∀ {a b : Int16} (c : Int16), c + a = c + b ↔ a = b
-- Mathlib.Algebra.Order.Field.Power
zpow_two_nonneg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α), 0 ≤ a ^ 2
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Analogue of `IntervalIntegrable.abs`: If a real-valued function `f` is circle integrable, then so is
`|f|`.
 -/
CircleIntegrable.abs : ∀ {c : ℂ} {R : ℝ} {f : ℂ → ℝ}, CircleIntegrable f c R → CircleIntegrable |f| c R
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalarsRange₂.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7}
  {P' : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : SMul S R] [inst_3 : AddCommMonoid M]
  [inst_4 : Module R M] [inst_5 : AddCommMonoid N] [inst_6 : Module R N] [inst_7 : AddCommMonoid P]
  [inst_8 : Module R P] [inst_9 : Module S M] [inst_10 : Module S N] [inst_11 : Module S P]
  [inst_12 : IsScalarTower S R M] [inst_13 : IsScalarTower S R N] [inst_14 : IsScalarTower S R P]
  [inst_15 : AddCommMonoid M'] [inst_16 : Module S M'] [inst_17 : AddCommMonoid N'] [inst_18 : Module S N']
  [inst_19 : AddCommMonoid P'] [inst_20 : Module S P'] [inst_21 : SMulCommClass R S P] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N)
  (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (B : M →ₗ[R] N →ₗ[R] P)
  (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range),
  i.restrictScalarsRange₂ j k hk B hB =
    ((LinearMap.restrictScalarsₗ S R N P S ∘ₗ ↑S B).compl₁₂ i j).codRestrict₂ k hk hB
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
LinearMap.lTensor_range : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} (Q : Type u_5) [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] {g : N →ₗ[R] P}, (LinearMap.lTensor Q g).range = (LinearMap.lTensor Q g.range.subtype).range
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_Z : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.Z✝ S
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.Nonempty.zero_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {s : Finset α}, s.Nonempty → 0 * s = 0
-- Mathlib.Topology.ContinuousOn
/-- A function is continuous at a point `x` within a set `s` if `x` is not an accumulation point of
`s`.  -/
continuousWithinAt_of_not_accPt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ¬AccPt x (Filter.principal s) → ContinuousWithinAt f s x
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.le_order_subst : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (a : MvPowerSeries τ S),
  PowerSeries.HasSubst a → ∀ (f : PowerSeries R), a.order * f.order ≤ (PowerSeries.subst a f).order
-- Mathlib.Order.MinMax
max_choice : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = a ∨ max a b = b
-- Init.Data.Iterators.Consumers.Monadic.Total
Std.IterM.Total.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : SizeOf α] [inst_1 : (a : Type w) → SizeOf (m a)]
  [inst_2 : SizeOf β] (it : Std.IterM m β), sizeOf { it := it } = 1 + sizeOf it
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- Notation for a pseudofunctor between bicategories.  -/
CategoryTheory.Bicategory.«term_⥤ᵖ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory MonCat fun x1 x2 => ↑x1 →* ↑x2
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.collision.injEq : ∀ {α : Type u} {β : Type v} (ks : Array α) (vs : Array β) (h : ks.size = vs.size) (ks_1 : Array α) (vs_1 : Array β)
  (h_1 : ks_1.size = vs_1.size),
  (Lean.PersistentHashMap.Node.collision ks vs h = Lean.PersistentHashMap.Node.collision ks_1 vs_1 h_1) =
    (ks = ks_1 ∧ vs = vs_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → (Std.DHashMap.Raw.Const.insertMany m l).getKey? k' = some k
-- Init.SimpLemmas
implies_congr_right : ∀ {p : Sort u} {q₁ q₂ : Sort v}, q₁ = q₂ → (p → q₁) = (p → q₂)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- A finite family of vectors `v i` is linear independent iff the linear map that sends
`c : ι → R` to `∑ i, c i • v i` is injective.  -/
Fintype.linearIndependent_iff'ₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι],
  LinearIndependent R v ↔ Function.Injective ⇑((LinearMap.lsum R (fun x => R) ℕ) fun i => LinearMap.id.smulRight (v i))
-- Init.Data.BitVec.Lemmas
BitVec.lt_of_isSome_getMsb? : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), (x.getMsb? i).isSome = true → i < w
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Naturality of the oplax functoriality constraint, on the left.  -/
CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c)
  {Z : self.obj a ⟶ self.obj c} (h : CategoryTheory.CategoryStruct.comp (self.map f') (self.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g))
      (CategoryTheory.CategoryStruct.comp (self.mapComp f' g) h) =
    CategoryTheory.CategoryStruct.comp (self.mapComp f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g)) h)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  ⋃₀ ↑(hC.disjointOfDiff hs ht) = s \ t
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_ratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ), (↑q).imJ = 0
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {_P : CategoryTheory.MorphismProperty C}
  [inst_1 : _P.IsMultiplicative] (obj obj_1 : C), ({ obj := obj } = { obj := obj_1 }) = (obj = obj_1)
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.of_boundaryLE : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₁ : ι₁} (h : e₁.BoundaryLE i₁),
  ac.Boundary i₁ (ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryLE ac h)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.dilatransvection.coe_toLinearMap : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} {h : IsUnit (1 + f v)}, ↑(LinearEquiv.dilatransvection h) = LinearMap.transvection f v
-- Mathlib.Data.Rel
/-- Notation for apply a relation `R : SetRel α β` to `a : α`, `b : β`,
scoped to the `SetRel` namespace.

Since `SetRel α β := Set (α × β)`, `a ~[R] b` is simply notation for `(a, b) ∈ R`, but this should
be considered an implementation detail.  -/
SetRel.«term_~[_]_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
Subgroup.SchurZassenhausInduction.step7 : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index →
    (∀ (G' : Type u) [inst : Group G'] [Finite G'],
        Nat.card G' < Nat.card G →
          ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H') →
      (∀ (H : Subgroup G), ¬N.IsComplement' H) → ∀ [Finite G], IsMulCommutative ↥N
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectIsoComp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X' : C} (f : X' ⟶ X) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) [inst_3 : CategoryTheory.Limits.HasKernel g],
  CategoryTheory.Limits.kernelSubobjectIsoComp f g =
    CategoryTheory.Limits.kernelSubobjectIso (CategoryTheory.CategoryStruct.comp f g) ≪≫
      CategoryTheory.Limits.kernelIsIsoComp f g ≪≫ (CategoryTheory.Limits.kernelSubobjectIso g).symm
-- Mathlib.RingTheory.AdjoinRoot
/-- **Alias** of `AdjoinRoot.quotMapOfEquivQuotMapCMapMk`.

---

The natural isomorphism `R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f))` for `α` a root of
`f : R[X]` and `I : Ideal R`.

See `AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot`
for the isomorphism with `(R/I)[X] / (f mod I)`.  -/
AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (f : Polynomial R) →
        AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I ≃+*
          AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.mk f) (Ideal.map Polynomial.C I)
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.ActionResult.toMessageData : Lean.Meta.Grind.ActionResult → Lean.MessageData
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_comp_toProd : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  (MonoidHom.snd M N).comp Monoid.Coprod.toProd = Monoid.Coprod.snd
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_of_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.isEmpty = true → m[a]? = none
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insertMany_empty_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {k : α},
  Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯) =
    (List.map Sigma.fst l).contains k
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_Ioc : ∀ {a b : ℝ}, MeasureTheory.volume.real (Set.Ioc a b) = max (b - a) 0
-- Mathlib.Probability.Independence.Integration
/-- If `f` and `g` are independent random variables with values in `ℝ≥0∞`,
then `E[f * g] = E[f] * E[g]`. However, instead of directly using the independence
of the random variables, it uses the independence of measurable spaces for the
domains of `f` and `g`. This is similar to the sigma-algebra approach to
independence. See `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun` for
a more common variant of the product of independent variables.  -/
ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace : ∀ {Ω : Type u_1} {f g : Ω → ENNReal} {Mf Mg mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  Mf ≤ mΩ →
    Mg ≤ mΩ →
      ProbabilityTheory.Indep Mf Mg μ →
        Measurable f → Measurable g → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_inf : ∀ {G : Type u_2} [inst : Group G] (S₁ S₂ : Subgroup Gᵐᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.FormatterAliasValue : Type
-- Mathlib.Algebra.Order.Module.Pointwise
smul_lowerBounds_subset_upperBounds_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : AddCommGroup β]
  [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β] {s : Set β} {a : α},
  a ≤ 0 → a • lowerBounds s ⊆ upperBounds (a • s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ')
  (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (y : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map η).app S).fst.app y =
    η.left.app (S.fst.obj y)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- If `d : MulticospanIndex J C`, `c : Multifork d` is a limit multifork,
and `F : C ⥤ D` is a functor which preserves the limit of `d.multicospan`,
then the multifork `c.map F` is limiting.  -/
CategoryTheory.Limits.Multifork.isLimitMapOfPreserves : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {J : CategoryTheory.Limits.MulticospanShape} →
          {d : CategoryTheory.Limits.MulticospanIndex J C} →
            (c : CategoryTheory.Limits.Multifork d) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.Limits.PreservesLimit d.multicospan F] →
                  CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (c.map F)
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_one' : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), (Polynomial.hasseDeriv 1) f = Polynomial.derivative f
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.finsetProd'`. -/
MeasureTheory.IsStronglyProgressive.finset_prod' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : CommMonoid β]
  [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) → MeasureTheory.IsStronglyProgressive f (∏ c ∈ s, U c)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instHasColimitsOfShapeOfModuleCat : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_2} J] [CategoryTheory.Limits.HasColimitsOfShape J (ModuleCat R)],
  CategoryTheory.Limits.HasColimitsOfShape J (TopModuleCat R)
-- Mathlib.Analysis.RCLike.Basic
RCLike.isCauSeq_re : ∀ {K : Type u_1} [inst : RCLike K] (f : CauSeq K norm), IsCauSeq abs fun n => RCLike.re (↑f n)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.isLocallySurjective_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) [CategoryTheory.IsIso φ], CategoryTheory.Sheaf.IsLocallySurjective φ