mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
_private.Mathlib.Geometry.Manifold.WhitneyEmbedding.0.SmoothBumpCovering.embeddingPiTangent.congr_simp : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (↑⊤) M] [inst_7 : T2Space M] [inst_8 : Fintype ι] {s : Set M}
  (f f_1 : SmoothBumpCovering ι I M s),
  f = f_1 → SmoothBumpCovering.embeddingPiTangent✝ f = SmoothBumpCovering.embeddingPiTangent✝ f_1
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerYield_flatMapM_pure : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [inst_5 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)}
  {it₁ it₁' : Std.Iter β} {it₂' : Std.IterM m γ} {b : β},
  it₁.IsPlausibleStep (Std.IterStep.yield it₁' b) →
    MonadAttach.CanReturn (f b) it₂' →
      (Std.Iter.flatMapAfterM f it₁ none).IsPlausibleStep
        (Std.IterStep.skip (Std.Iter.flatMapAfterM f it₁' (some it₂')))
-- Mathlib.Tactic.Simps.Basic
/-- You can specify custom projections for the `@[simps]` attribute.
To do this for the projection `MyStructure.originalProjection` by adding a declaration
`MyStructure.Simps.myProjection` that is definitionally equal to
`MyStructure.originalProjection` but has the projection in the desired (simp-normal) form.
Then you can call
```
initialize_simps_projections (originalProjection → myProjection, ...)
```
to register this projection. See `elabInitializeSimpsProjections` for more information.

You can also specify custom projections that are definitionally equal to a composite of multiple
projections. This is often desirable when extending structures (without `oldStructureCmd`).

`CoeFun` and notation class (like `Mul`) instances will be automatically used, if they
are definitionally equal to a projection of the structure (but not when they are equal to the
composite of multiple projections).
 -/
LibraryNote.custom_simps_projection : Batteries.Util.LibraryNote
-- Mathlib.Order.Filter.CountableInter
Filter.EventuallyEq.countable_bInter : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) → ⋂ i, ⋂ (h : i ∈ S), s i h =ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.supOfBasis.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.house.supOfBasis✝ K =
    Finset.univ.sup' ⋯ fun r =>
      NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) ((NumberField.house.newBasis✝ K) r))
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.Sentence.instSetLike : {L : FirstOrder.Language} → {T : L.Theory} → {α : Type w} → SetLike (T.CompleteType α) (L.withConstants α).Sentence
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂Measurable_toGerm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ]
  [inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : MeasurableSpace β] [inst_6 : BorelSpace β]
  [inst_7 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_8 : SecondCountableTopologyEither β γ]
  [inst_9 : MeasurableSpace γ] [inst_10 : BorelSpace γ] [inst_11 : TopologicalSpace.PseudoMetrizableSpace δ]
  [inst_12 : SecondCountableTopology δ] [inst_13 : MeasurableSpace δ] [inst_14 : OpensMeasurableSpace δ] (g : β → γ → δ)
  (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ),
  (MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm
-- Lean.Parser.Term
Lean.Parser.Term.letConfigItem : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- On square matrices, `Matrix.mulLinearMap` and `LinearMap.mul` coincide.  -/
mulLinearMap_eq_mul : ∀ {m : Type u_2} (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : CommSemiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A]
  [inst_5 : IsScalarTower R A A], mulLinearMap R = LinearMap.mul R (Matrix m m A)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_nat : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddMonoidWithOne G]
  [inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℕ), f (x + ↑n) = f x + ↑n
-- Init.Data.BitVec.Basic
/-- Interprets the bitvector as an integer stored in two's complement form.
 -/
BitVec.toInt : {n : ℕ} → BitVec n → ℤ
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_map_iff : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {hl₁ : S₁.LeftHomologyData}
  {hl₂ : S₂.LeftHomologyData} (ψl : CategoryTheory.ShortComplex.LeftHomologyMapData φ hl₁ hl₂)
  [inst_5 : (F.mapShortComplex.obj S₁).HasHomology] [inst_6 : (F.mapShortComplex.obj S₂).HasHomology]
  [hl₁.IsPreservedBy F] [hl₂.IsPreservedBy F],
  CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.IsIso (F.map ψl.φH)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.mk_zero : Complex.UnitClosedDisc.mk 0 Complex.UnitClosedDisc.mk_zero._proof_1 = 0
-- Mathlib.Data.Complex.Basic
Complex.I_sq : Complex.I ^ 2 = -1
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The functor part of the equivalence of categories `LightDiagram' ≌ LightDiagram`.  -/
LightDiagram'.toLightFunctor : CategoryTheory.Functor LightDiagram' LightDiagram
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_mem_coeffsIn : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S} {i : σ →₀ ℕ} {x : S}, (MvPolynomial.monomial i) x ∈ MvPolynomial.coeffsIn σ M ↔ x ∈ M
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_mk : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Multiset ι) (hs : s.Nodup) (f : ι → M),
  { val := s, nodup := hs }.prod f = (Multiset.map f s).prod
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ioo_top : ∀ (x : ℝ), Real.toEReal ⁻¹' Set.Ioo ↑x ⊤ = Set.Ioi x
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv_leadingCoeff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x : HahnSeries Γ Rᵃᵒᵖ),
  (AddOpposite.unop (HahnSeries.addOppositeEquiv x)).leadingCoeff = AddOpposite.unop x.leadingCoeff
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [IsEmpty β], HasSum f 0 L
-- Init.Data.FloatArray.Basic
FloatArray.emptyWithCapacity : ℕ → FloatArray
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.pullbackMap.eq_1 : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] [inst_3 : p.IsPreFibered] {R S : 𝒮} {a : 𝒳} (f : R ⟶ S)
  (ha : p.obj a = S),
  HasFibers.pullbackMap f ha =
    CategoryTheory.CategoryStruct.comp (HasFibers.Fib.mkIsoSelf ⋯).hom
      (CategoryTheory.Functor.IsPreFibered.pullbackMap ha f)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReflBEqMon : ReflBEq Lean.Grind.CommRing.Mon
-- Mathlib.RingTheory.WittVector.Compare
_private.Mathlib.RingTheory.WittVector.Compare.0.term𝕎 : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivWithinAt_const_add_iff`. -/
HasDerivWithinAt.const_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F),
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => c + f x) f' s x
-- Aesop.Builder.Apply
Aesop.RuleBuilder.checkNoIff : Lean.Expr → Lean.MetaM Unit
-- Mathlib.Data.Sym.Sym2
Sym2.toFinset.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (z : Sym2 α), z.toFinset = z.toMultiset.toFinset
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.algebraMap_left_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [inst_1 : CommRing R]
  (v : Valuation R Γ₀) [inst_2 : Semiring S] [inst_3 : Algebra R S] (s : WithVal v),
  (algebraMap (WithVal v) S) s = (algebraMap R S) s.ofVal
-- Lean.Parser.Term
/-- Term-level form of the interactive debugger. See the `doIdbg` do element for full documentation.  -/
Lean.Parser.Term.idbg : Lean.Parser.Parser
-- Mathlib.NumberTheory.AlmostPrime
Nat.Prime.isAlmostPrime_one : ∀ {p : ℕ}, Nat.Prime p → Nat.IsAlmostPrime 1 p
-- Mathlib.Data.Int.GCD
/-- Euclid's lemma: if `a ∣ b * c` and `gcd a c = 1` then `a ∣ b`.
Compare with `IsCoprime.dvd_of_dvd_mul_left` and
`UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors`  -/
Int.dvd_of_dvd_mul_left_of_gcd_one : ∀ {a b c : ℤ}, a ∣ b * c → a.gcd c = 1 → a ∣ b
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- A fundamental sequence for `a` is an increasing sequence of length `o = cof a` that converges at
`a`. We provide `o` explicitly in order to avoid type rewrites.  -/
Ordinal.IsFundamentalSequence : Ordinal.{u} → (o : Ordinal.{u}) → ((b : Ordinal.{u}) → b < o → Ordinal.{u}) → Prop
-- Mathlib.Algebra.Group.Units.Hom
Units.map_comp : ∀ {M : Type u} {N : Type v} {P : Type w} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] (f : M →* N)
  (g : N →* P), Units.map (g.comp f) = (Units.map g).comp (Units.map f)
-- Mathlib.Data.Nat.MaxPowDiv
Nat.not_dvd_divMaxPow : ∀ {p n : ℕ}, 1 < p → n ≠ 0 → ¬p ∣ n.divMaxPow p
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.coe_addChar_of_value_at_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] {r : R}
  (hr : Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0)),
  ⇑(PadicInt.addChar_of_value_at_one r hr) = ⇑(PadicInt.mahlerSeries fun x => r ^ x)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right]
  (X :
    CategoryTheory.Limits.Cofork
      (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))
      (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))),
  (I.multicoforkEquivSigmaCofork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.tryTactic : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM Bool
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
/-- denotes expression definition equal to `n`  -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.const : ℕ → Nat.NatOffset✝
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' : ∀ {R : Type u_1} [inst : NormedRing R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    Summable f →
      (Summable fun x => ‖g x‖) →
        Summable g → (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
-- Mathlib.Algebra.Homology.LocalCohomology
/-- The diagram of all ideals with radical containing `J`, represented as a functor.
This is the "largest" diagram that computes local cohomology with support in `J`.  -/
localCohomology.selfLERadicalDiagram : {R : Type u} → [inst : CommRing R] → (J : Ideal R) → CategoryTheory.Functor (localCohomology.SelfLERadical J) (Ideal R)
-- Mathlib.Order.Interval.Set.Image
AntitoneOn.mapsTo_Iic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  AntitoneOn f (Set.Iic b) → Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
-- Mathlib.GroupTheory.Exponent
/-- The exponent is zero iff for all nonzero `n`, one can find a `g` such that `g ^ n ≠ 1`.  -/
Monoid.exponent_eq_zero_iff_forall : ∀ {G : Type u} [inst : Monoid G], Monoid.exponent G = 0 ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_vecMulVec : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Mul R] [ContinuousMul R] {A : X → m → R} {B : X → n → R},
  Continuous A → Continuous B → Continuous fun x => Matrix.vecMulVec (A x) (B x)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_subset_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  r ≠ 0 →
    v.intValuationDef r = WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instContinuousConstSMul : ∀ {S : Type u_2} {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M]
  [inst_2 : SMul S R] [inst_3 : SMul S M] [ContinuousConstSMul S R] [ContinuousConstSMul S M],
  ContinuousConstSMul S (TrivSqZeroExt R M)
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getUnifyKeyArgs : Lean.Expr → Bool → Lean.MetaM (Lean.Meta.DiscrTree.Key × Array Lean.Expr)
-- Mathlib.Data.Setoid.Basic
Setoid.trans' : ∀ {α : Type u_1} (r : Setoid α) {x y z : α}, r x y → r y z → r x z
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_self : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, nhdsSetWithin s s = Filter.principal s
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instReprOffset : Repr Std.Time.Nanosecond.Offset
-- Batteries.Data.List.Basic
/-- Inner loop for `swapTR`.  -/
List.swapTR.go : {α : Type u_1} → List α → List α → ℕ → ℕ → Array α → List α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.WithCache.val : {α : Type u} → {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} → Std.Tactic.BVDecide.BVExpr.WithCache α aig → α
-- Mathlib.Computability.NFA
/-- Set of starting states  -/
NFA.start : {α : Type u} → {σ : Type v} → NFA α σ → Set σ
-- Mathlib.Algebra.Order.Group.Defs
/-- Assuming `α` equipped with `LinearOrder` is `AddCancelCommMonoid` and `IsAddOrderedMonoid`, it
is also `IsAddOrderedCancelMonoid`.

TODO: make it an `instance`. To avoid slowdown, it was not an instance when it was submitted. See
https://github.com/leanprover-community/mathlib4/pull/32828.  -/
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid' : ∀ {α : Type u} [inst : AddCancelCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α],
  IsOrderedCancelAddMonoid α
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries.eq_1 : ∀ (𝕂 : Type u_1) (𝔸 : Type u_2) [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (n : ℕ),
  NormedSpace.expSeries 𝕂 𝔸 n = (↑n.factorial)⁻¹ • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸
-- Mathlib.Topology.Algebra.GroupCompletion
AddMonoidHom.extension_coe : ∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : IsUniformAddGroup β] [inst_6 : CompleteSpace β]
  [inst_7 : T0Space β] (f : α →+ β) (hf : Continuous ⇑f) (a : α), (f.extension hf) ↑a = f a
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoSelf_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I)
  {Z : CategoryTheory.Limits.FormalCoproduct C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X.toFun i)
      (CategoryTheory.CategoryStruct.comp X.coproductIsoSelf.hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))) h
-- Mathlib.Order.Partition.Finpartition
/-- Extend a partition of `a` to a partition of `b` when `a ≤ b`, by adding `b \ a` as a `part`.  -/
Finpartition.extendOfLE : {α : Type u_1} →
  [inst : GeneralizedBooleanAlgebra α] → [DecidableEq α] → {a b : α} → Finpartition a → a ≤ b → Finpartition b
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_smul_inv_left_eq_smul_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ (c : ENNReal), c ≠ 0 → c ≠ ⊤ → MeasureTheory.llr (c⁻¹ • μ) ν =ᵐ[μ] MeasureTheory.llr μ (c • ν)
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan.eq_1 : catalan 0 = 1
-- Mathlib.Algebra.Order.Hom.Basic
/-- `AddGroupSeminormClass F α` states that `F` is a type of `β`-valued seminorms on the additive
group `α`.

You should extend this class when you extend `AddGroupSeminorm`.  -/
AddGroupSeminormClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [AddGroup α] → [AddCommMonoid β] → [PartialOrder β] → [FunLike F α β] → Prop
-- Mathlib.Order.Defs.LinearOrder
/-- The category of linear orders.

This will get reused to define `OrderType`.  -/
LinOrd : Type (u_2 + 1)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mod.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] {g g_1 : PowerSeries A} (e_g : g = g_1) {I I_1 : Ideal A} (e_I : I = I_1)
  (H : g.IsWeierstrassDivisorAt I) (f f_1 : PowerSeries A),
  f = f_1 → ∀ [inst_1 : IsPrecomplete I A], H.mod f = ⋯.mod f_1
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
ContDiffAt.image_mem_toOpenPartialHomeomorph_target : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕂 E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕂 F] [inst_5 : CompleteSpace E] {f : E → F}
  {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0),
  f a ∈ (ContDiffAt.toOpenPartialHomeomorph f hf hf' hn).target
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.op.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (h : CategoryTheory.SplitEpi f),
  h.op = { retraction := h.section_.op, id := ⋯ }
-- Mathlib.Data.List.Sort
List.Sublist.orderedInsert_sublist : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [IsTrans α r] {as bs : List α} (x : α),
  as.Sublist bs → List.Pairwise r bs → (List.orderedInsert r x as).Sublist (List.orderedInsert r x bs)
-- Init.Data.Slice.Basic
Std.Slice.mk : {γ : Type u} → γ → Std.Slice γ
-- Mathlib.Logic.Unique
Pi.default_def : ∀ {α : Sort u_1} {β : α → Sort v} [inst : (a : α) → Inhabited (β a)], default = fun a => default
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
/-- The property of objects in the functor category `J ⥤ C`
which preserves limits of shape `K`.  -/
CategoryTheory.ObjectProperty.preservesLimitsOfShape : {J : Type u_1} →
  {C : Type u_3} →
    (K : Type u_5) →
      [CategoryTheory.Category.{v_1, u_5} K] →
        [inst : CategoryTheory.Category.{v_3, u_1} J] →
          [inst_1 : CategoryTheory.Category.{v_5, u_3} C] → CategoryTheory.ObjectProperty (CategoryTheory.Functor J C)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.flatten.match_1.eq_1 : ∀ {α : Type u_1} (motive : Stream'.WSeq α ⊕ Computation (Stream'.WSeq α) → Sort u_2) (s : Stream'.WSeq α)
  (h_1 : (s : Stream'.WSeq α) → motive (Sum.inl s)) (h_2 : (c' : Computation (Stream'.WSeq α)) → motive (Sum.inr c')),
  (match Sum.inl s with
    | Sum.inl s => h_1 s
    | Sum.inr c' => h_2 c') =
    h_1 s
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitAuxAux_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
  (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A),
  (CategoryTheory.OverPresheafAux.counitAuxAux F s).inv =
    TypeCat.ofHom (CategoryTheory.OverPresheafAux.counitBackward F s)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.lt_of_intCast_lt_intCast : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a b : ℤ), ↑a < ↑b → a < b
-- Aesop.Tree.Data
Aesop.instInhabitedNodeState : Inhabited Aesop.NodeState
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.Intermediate.dropWhileM_eq_dropWhileWithPostcondition : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → m (ULift.{u_1, 0} Bool)} {dropping : Bool},
  Std.IterM.Intermediate.dropWhileM P dropping it =
    Std.IterM.Intermediate.dropWhileWithPostcondition (Std.Iterators.PostconditionT.attachLift ∘ P) dropping it
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.union_insert_right_equiv_insert_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {p : (a : α) × β a},
  m₁.WF → m₂.WF → (m₁ ∪ m₂.insert p.fst p.snd).Equiv ((m₁ ∪ m₂).insert p.fst p.snd)
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.add_left_inj : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] {a b : M} (c : M), a + c = b + c ↔ a = b
-- Mathlib.Logic.Unique
unique_subtype_iff_existsUnique : ∀ {α : Sort u_1} (p : α → Prop), Nonempty (Unique (Subtype p)) ↔ ∃! a, p a
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.hasRightDerivedFunctor_iff : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [L.IsLocalization W], F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F
-- Mathlib.Tactic.Push
/-- Elaborate the `(disch := ...)` syntax for a `simp`-like tactic.  -/
Mathlib.Tactic.Push.elabDischarger : Lean.TSyntax `Lean.Parser.Tactic.discharger → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Discharge
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `w₁ w₂` are words such that `w₁` reduces to `w₂`, then `w₂` is a sublist of `w₁`.  -/
FreeGroup.Red.sublist : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red L₁ L₂ → L₂.Sublist L₁
-- Mathlib.Order.Atoms
IsStronglyAtomic.exists_covBy_le_of_lt : ∀ {α : Type u_5} {inst : Preorder α} [self : IsStronglyAtomic α] (a b : α), a < b → ∃ x, a ⋖ x ∧ x ≤ b