mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_right : ∀ {α : Type u_1} {s t : Multiset α}, Disjoint s t ↔ ∀ {a : α}, a ∈ t → a ∉ s
-- Mathlib.Data.Set.Lattice
Set.union_distrib_iInter_left : ∀ {α : Type u_1} {ι : Sort u_5} (s : ι → Set α) (t : Set α), t ∪ ⋂ i, s i = ⋂ i, t ∪ s i
-- Init.Core
/-- The transitive closure `TransGen r` of a relation `r` is the smallest relation which is
transitive and contains `r`. `TransGen r a z` if and only if there exists a sequence
`a r b r ... r z` of length at least 1 connecting `a` to `z`.
 -/
Relation.TransGen : {α : Sort u} → (α → α → Prop) → α → α → Prop
-- Mathlib.AlgebraicGeometry.Spec
/-- This is the `AlgHom` version of `toPushforwardStalk`, which is the map `S ⟶ (f∗ 𝒪ₛ)ₚ` for some
algebra `R ⟶ S` and some `p : Spec R`.
 -/
AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom : (R S : CommRingCat) →
  (p : PrimeSpectrum ↑R) →
    [inst : Algebra ↑R ↑S] →
      ↑S →ₐ[↑R]
        ↑(((TopCat.Presheaf.pushforward CommRingCat
                    (AlgebraicGeometry.Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
            p)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.map_id : ∀ {X Y : SSet.Truncated 2} (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 }))
  (f : X ⟶ Y),
  (SSet.Truncated.Edge.id x).map f =
    SSet.Truncated.Edge.id
      ((CategoryTheory.ConcreteCategory.hom
          (f.app (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })))
        x)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_list_prod : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (L : List (Polynomial R)),
  Polynomial.map f L.prod = (List.map (Polynomial.map f) L).prod
-- Mathlib.Topology.MetricSpace.Thickening
/-- **Alias** of `Metric.cthickening_eq_preimage_infEDist`. -/
Metric.cthickening_eq_preimage_infEdist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.cthickening δ E = (fun x => Metric.infEDist x E) ⁻¹' Set.Iic (ENNReal.ofReal δ)
-- Mathlib.Algebra.Ring.Defs
/-- One is a left neutral element for multiplication  -/
NonAssocSemiring.one_mul : ∀ {α : Type u} [self : NonAssocSemiring α] (a : α), 1 * a = a
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.exists_eq_restrict : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → ∃ R ⊆ M.E, N = M.restrict R
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.Hom.ext_iff : ∀ {R S : RingCat} {x y : R.Hom S}, x = y ↔ x.hom' = y.hom'
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- The convex body equal to the set of points `x : mixedSpace K` such that
`∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B`.  -/
NumberField.mixedEmbedding.convexBodySum : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℝ → Set (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Data.Finset.Insert
Finset.forall_mem_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) (p : α → Prop), (∀ x ∈ Finset.cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x
-- Init.Data.Ord.SInt
Int16.instLawfulOrderOrd : Std.LawfulOrderOrd Int16
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.dNext_cochainComplex : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) (j : ℕ),
  (dNext j) f = CategoryTheory.CategoryStruct.comp (P.d j (j + 1)) (f (j + 1) j)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
/-- The semivariation of a vector measure, defined as the supremum of the variations
of the images of the vector measures under continuous linear forms of norm at most `1`.  -/
MeasureTheory.VectorMeasure.semivariation : {X : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → {mX : MeasurableSpace X} → MeasureTheory.VectorMeasure X E → Set X → ENNReal
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_sub_const_iff`. -/
Sbtw.sub_const : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Sbtw R x y z → Sbtw R (x - v) (y - v) (z - v)
-- Qq.Typ
/-- `QuotedLevelDefEq u v` says that the levels `u` and `v` are definitionally equal.

You should usually write this using the notation `$u =QL $v`.
 -/
Qq.QuotedLevelDefEq : Lean.Level → Lean.Level → Prop
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₂_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.π₂.obj S = S.X₂
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_lt_zero : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1]
  {n : ℤ}, ↑n < 0 ↔ n < 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.Equation.map : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} {S : Type s} [inst_1 : CommRing S] (f : R →+* S)
  {x y : R}, W.Equation x y → (W.map f).Equation (f x) (f y)
-- Mathlib.CategoryTheory.ObjectProperty.Extensions
CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  ⊤.IsClosedUnderExtensions
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesColimitsOfShapeEvalOfHasColimitsOfShape : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] (n : ι),
  CategoryTheory.Limits.PreservesColimitsOfShape J (HomologicalComplex.eval C c n)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.isPrefixOfAux.eq_1 : ∀ {α : Type u} [inst : BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : ℕ),
  as.isPrefixOfAux bs hle i =
    if h : i < as.size then
      have a := as[i];
      have this := ⋯;
      have b := bs[i];
      if (a == b) = true then as.isPrefixOfAux bs hle (i + 1) else false
    else true
-- Init.Data.Rat.Lemmas
Rat.abs_nonneg : ∀ {x : ℚ}, 0 ≤ x.abs
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ici_mul_Ioi_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [MulLeftStrictMono α]
  [MulRightStrictMono α] [inst_5 : LocallyFiniteOrderTop α] (a b : α), Finset.Ici a * Finset.Ioi b ⊆ Finset.Ioi (a * b)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_mk : ∀ {α : Type u} {L : List (α × Bool)} {β : Type v} [inst : Group β] {f : α → β},
  (FreeGroup.lift f) (FreeGroup.mk L) = (List.map (fun x => bif x.2 then f x.1 else (f x.1)⁻¹) L).prod
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.npowRec'.match_1.eq_2 : ∀ {M : Type u_2} (motive : ℕ → M → Sort u_1) (m : M) (h_1 : (x : M) → motive 0 x) (h_2 : (m : M) → motive 1 m)
  (h_3 : (k : ℕ) → (m : M) → motive k.succ.succ m),
  (match 1, m with
    | 0, x => h_1 x
    | 1, m => h_2 m
    | k.succ.succ, m => h_3 k m) =
    h_2 m
-- Std.Internal.Do.Order.PreservesSup
/-- `f : α → α` *preserves `Sup`* if it distributes over arbitrary joins:
`f (sup s) = sup { f x | x ∈ s }`. Equivalently `f` is a lower adjoint, so it has an upper adjoint
`PreservesSup.upperAdjoint f`.

A frame operator acts by a `Sup`-preserving map for each resource `r`: the lattice meet `(a ⊓ ·)`,
or a cost combinator `(costConj r)` for a counter resource. The upper adjoint is the corresponding
implication: Heyting `⇨` for the meet, a magic wand for separating conjunction.
 -/
Lean.Order.PreservesSup : {α : Type u} → [Lean.Order.CompleteLattice α] → (α → α) → Prop
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.regularSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], RegularSpace (TopologicalSpace.Compacts α) ↔ RegularSpace α
-- Mathlib.Data.List.AList
_private.Mathlib.Data.List.AList.0.AList.insertRec.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : AList β → Sort u_3) (nodupKeys : [].NodupKeys)
  (h_1 : (nodupKeys : [].NodupKeys) → motive { entries := [], nodupKeys := nodupKeys })
  (h_2 :
    (c : Sigma β) → (l : List (Sigma β)) → (h : (c :: l).NodupKeys) → motive { entries := c :: l, nodupKeys := h }),
  (match { entries := [], nodupKeys := nodupKeys } with
    | { entries := [], nodupKeys := nodupKeys } => h_1 nodupKeys
    | { entries := c :: l, nodupKeys := h } => h_2 c l h) =
    h_1 nodupKeys
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.State.mk.inj : ∀ {perfect perfect_1 : Bool}, { perfect := perfect } = { perfect := perfect_1 } → perfect = perfect_1
-- Mathlib.RingTheory.Etale.QuasiFinite
Ideal.fiberIsoOfBijectiveResidueField.eq_1 : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : CommRing S]
  [inst_3 : Algebra R R'] [inst_4 : Algebra R S] {p : Ideal R} {q : Ideal R'} [inst_5 : p.IsPrime] [inst_6 : q.IsPrime]
  [inst_7 : q.LiesOver p] (H : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)),
  Ideal.fiberIsoOfBijectiveResidueField H =
    (PrimeSpectrum.primesOverOrderIsoFiber R' (TensorProduct R R' S) q).trans
      ((PrimeSpectrum.comapEquiv
            ((AlgEquiv.restrictScalars p.ResidueField
                    (Algebra.TensorProduct.cancelBaseChange R R' q.ResidueField q.ResidueField S)).trans
                (Algebra.TensorProduct.congr (AlgEquiv.ofBijective (Algebra.ofId p.ResidueField q.ResidueField) H).symm
                  AlgEquiv.refl)).toRingEquiv).trans
        (PrimeSpectrum.primesOverOrderIsoFiber R S p).symm)
-- Mathlib.Tactic.DuplicateDecls
/-- Given a module name, return a number that can be used for sorting.  -/
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.libraryNumber : Lean.Name → ℕ
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.codRestrict_apply_coe : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N)
  (h : ∀ (v : ι → M), f v ∈ p) (v : ι → M), ↑((f.codRestrict p h) v) = f v
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart.value : Lean.Lsp.InlayHintLabelPart → String
-- Lean.Data.Position
Lean.MonadFileMap : (Type → Type) → Type
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
instIsPrimeValIdealMemSetAssociatedPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (I : ↑(associatedPrimes R M)), (↑I).IsPrime
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.SubgroupNormal.mem_comm : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H ≤ K → ∀ [hN : (H.addSubgroupOf K).Normal] {a b : G}, b ∈ K → a + b ∈ H → b + a ∈ H
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.prod_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B]
  (S : NonUnitalStarSubalgebra R A) (S₁ : NonUnitalStarSubalgebra R B),
  (S.prod S₁).toNonUnitalSubalgebra = S.prod S₁.toNonUnitalSubalgebra
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.wasCancelledByEdit : Lean.Server.RequestCancellationToken → BaseIO Bool
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.iUnion_openCell_eq_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : T2Space X] [inst_1 : Topology.CWComplex C] (n : ℕ∞),
  ⋃ m, ⋃ (_ : ↑m < n + 1), ⋃ j, Topology.RelCWComplex.openCell m j = ↑(Topology.RelCWComplex.skeleton C n)
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.rel : {α : Type u} →
  [inst : Lean.Grind.Semiring α] →
    Equivalence (Lean.Grind.Ring.OfSemiring.r α) →
      Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α → Prop
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_eq_span_image2 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N),
  Submodule.map₂ f p q = Submodule.span R (Set.image2 (fun m n => (f m) n) ↑p ↑q)
-- Mathlib.GroupTheory.Index
AddSubgroup.isFiniteRelIndex_of_finiteIndex : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [h : H.FiniteIndex], H.IsFiniteRelIndex K
-- Mathlib.Algebra.Group.Action.Prod
/-- An `AddAction` by a product monoid is equivalent to commuting `AddAction`s by the factors.  -/
AddAction.prodEquiv : (M : Type u_1) →
  (N : Type u_2) →
    (α : Type u_5) →
      [inst : AddMonoid M] →
        [inst_1 : AddMonoid N] →
          AddAction (M × N) α ≃ (x : AddAction M α) ×' (x_1 : AddAction N α) ×' VAddCommClass M N α
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMap_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
  [inst_4 : S₃.HasLeftHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
  CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ₁)
      (CategoryTheory.ShortComplex.leftHomologyMap φ₂)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_erase_eq_of_not_compare_eq_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, ¬cmp k (t.min ⋯) = Ordering.eq → (t.erase k).min he = t.min ⋯
-- Mathlib.Order.Filter.Map
Filter.map_def : ∀ {α β : Type u_6} (m : α → β) (f : Filter α), m <$> f = Filter.map m f
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `CompSource` tracks the source of a comparison.
The atomic source of a comparison is an assumption, indexed by a natural number.
Two comparisons can be added to produce a new comparison,
and one comparison can be scaled by a natural number to produce a new comparison.
 -/
Mathlib.Tactic.Linarith.CompSource : Type
-- Batteries.Data.Nat.Bisect
Nat.avg_le_left : ∀ {b a : ℕ}, b ≤ a → a.avg b ≤ a
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trTape'_move_left : ∀ {Γ : Type u_1} {n : ℕ} {enc : Γ → List.Vector Bool n} [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (L R : Turing.ListBlank Γ),
  (Turing.Tape.move Turing.Dir.left)^[n] (Turing.TM1to1.trTape' enc0 L R) =
    Turing.TM1to1.trTape' enc0 L.tail (Turing.ListBlank.cons L.head R)
-- Mathlib.Data.Set.Function
Set.BijOn.prodMap : ∀ {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁}
  {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂},
  Set.BijOn f₁ s₁ t₁ → Set.BijOn f₂ s₂ t₂ → Set.BijOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_eq_getKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α} {h : a ∈ t}, t.getKey a h = t.getKey! a
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.AbelMode.raw.sizeOf_spec : sizeOf Mathlib.Tactic.Abel.AbelMode.raw = 1
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_compl_finset_of_infinite : ∀ {α : Type u_1} [Infinite α] (s : Finset α), Cardinal.mk ↑(↑s)ᶜ = Cardinal.mk α
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toArray_eq_toArray_roi : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toArray = #[r.lower] ++ r.lower<...*.toArray
-- Mathlib.Analysis.SpecialFunctions.Log.Base
ContinuousWithinAt.logb : ∀ {α : Type u_1} {b : ℝ} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α} {a : α},
  ContinuousWithinAt f s a → f a ≠ 0 → ContinuousWithinAt (fun x => Real.logb b (f x)) s a
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso'_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C}
  (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' X i).hom.left = ⋯.isoPushout.inv
-- Mathlib.Order.RelIso.Basic
Subtype.relEmbedding_apply : ∀ {X : Type u_5} (r : X → X → Prop) (p : X → Prop) (self : Subtype p), (Subtype.relEmbedding r p) self = ↑self
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.coinduct : ∀ (pred : {basis : Tactic.ComputeAsymptotics.Basis} → Tactic.ComputeAsymptotics.MultiseriesExpansion basis → Prop),
  (∀ {basis : Tactic.ComputeAsymptotics.Basis} (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion basis),
      pred ms →
        basis = [] ∨
          (∃ basis_hd basis_tl f,
              f =ᶠ[Filter.atTop] 0 ∧
                basis = basis_hd :: basis_tl ∧
                  ms ≍
                    Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
                      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil f) ∨
            ∃ basis_hd f basis_tl exp coef tl,
              pred coef ∧
                Tactic.ComputeAsymptotics.Majorized f basis_hd exp ∧
                  pred (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk tl (f - basis_hd ^ exp * coef.toFun)) ∧
                    basis = basis_hd :: basis_tl ∧
                      ms ≍
                        Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
                          (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f) →
    ∀ {basis : Tactic.ComputeAsymptotics.Basis} (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion basis),
      pred ms → ms.Approximates
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.mul_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] (x y : MonoidAlgebra R M),
  x * y = x.coeff.sum fun m₁ r₁ => y.coeff.sum fun m₂ r₂ => MonoidAlgebra.single (m₁ * m₂) (r₁ * r₂)
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} {ys zs : Array β},
  xs.mapFinIdx f = ys ++ zs ↔
    ∃ ys' zs',
      ∃ (w : xs = ys' ++ zs'),
        (ys'.mapFinIdx fun i a h => f i a ⋯) = ys ∧ (zs'.mapFinIdx fun i a h => f (i + ys'.size) a ⋯) = zs
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_apply_zero : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) (n : ℕ),
  ((FormalMultilinearSeries.ofScalars E c n) fun x => 0) = Pi.single 0 (c 0 • 1) n
-- Plausible.Gen
Plausible.GenError.genError : String → Plausible.GenError
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Induction principle for `K⟮X⟯`: if `f p q : P (p / q)` for all `p q : K[X]`,
then `P` holds on all elements of `K⟮X⟯`.

See also `induction_on'`, which is a recursion principle defined in terms of `RatFunc.mk`.
 -/
RatFunc.induction_on : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : RatFunc K → Prop} (x : RatFunc K),
  (∀ (p q : Polynomial K),
      q ≠ 0 → P ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)) →
    P x
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {f : X ⟶ Y} (self : CategoryTheory.Abelian.AbelianStruct f),
  CategoryTheory.CategoryStruct.comp self.imageπ self.imageι = f
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {x : ↥X} {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
      (CategoryTheory.CategoryStruct.comp (Y.fromSpecStalk (f x)) h) =
    CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (CategoryTheory.CategoryStruct.comp f h)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.mk : String → Option ℕ → Lean.Lsp.FileSystemWatcher
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.exists_addMonoid_generator : ∀ {α : Type u_1} [inst : AddGroup α] [Finite α] [IsAddCyclic α], ∃ x, ∀ (y : α), y ∈ AddSubmonoid.multiples x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.inter_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ m₄ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∩ m₂).Equiv (m₃ ∩ m₄)
-- Mathlib.Data.Set.Image
Set.range_eq_empty_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Set.range f = ∅ ↔ IsEmpty ι
-- Init.Data.String.Lemmas.Slice
String.Slice.Pos.get?_eq_some_get : ∀ {s : String.Slice} {p : s.Pos} (h : p ≠ s.endPos), p.get? = some (p.get h)
-- Init.Data.String.Lemmas.Iterate
String.Model.map_get_positionsFrom_of_splits : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String},
  p.Splits t₁ t₂ → List.map (fun p => (↑p).get ⋯) (String.Model.positionsFrom p) = t₂.toList
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S) (mem₀ : toPreZeroHypercover.presieve₀ ∈ J.coverings S)
  (toPreZeroHypercover_1 : CategoryTheory.PreZeroHypercover S)
  (mem₀_1 : toPreZeroHypercover_1.presieve₀ ∈ J.coverings S),
  ({ toPreZeroHypercover := toPreZeroHypercover, mem₀ := mem₀ } =
      { toPreZeroHypercover := toPreZeroHypercover_1, mem₀ := mem₀_1 }) =
    (toPreZeroHypercover = toPreZeroHypercover_1)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_bot_right : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.relIndex ⊥ = 1
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Expressing uniform convergence using `dist`  -/
Metric.tendstoUniformlyOnFilter_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_1} [inst : PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι}
  {p' : Filter β}, TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
-- Mathlib.Algebra.Order.Sub.Basic
tsub_pos_iff_lt : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, 0 < a - b ↔ b < a
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.interior_nonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α), (interior ↑s).Nonempty
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value.
 -/
Std.Time.PlainDateTime.withMilliseconds : Std.Time.PlainDateTime → Std.Time.Millisecond.Ordinal → Std.Time.PlainDateTime
-- Lean.Setup
Lean.instInhabitedImport : Inhabited Lean.Import