mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Format.DateFormat
/-- Full PM marker (used by `aaaa`). Typically lowercase per CLDR ("post meridiem").
 -/
Std.Time.DateFormatSymbols.pmLong : Std.Time.DateFormatSymbols → String
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- **Alias** of `PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_le`.

---

Specialization of `exists_primeSpectrum_prod_le_and_ne_bot_of_domain` to Dedekind domains:
Let `I : Ideal A` be a nonzero ideal, where `A` is a Dedekind domain that is not a field.
Then `exists_primeSpectrum_prod_le_and_ne_bot_of_domain` states we can find a product of prime
ideals that is contained within `I`. This lemma extends that result by making the product minimal:
let `M` be a maximal ideal that contains `I`, then the product including `M` is contained within `I`
and the product excluding `M` is not contained within `I`.  -/
exists_multiset_prod_cons_le_and_prod_not_le : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A],
  ¬IsField A →
    ∀ {I M : Ideal A},
      I ≠ ⊥ →
        I ≤ M →
          ∀ [hM : M.IsMaximal],
            ∃ Z,
              (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regOfFamily_ne_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ},
  NumberField.Units.IsMaxRank u → NumberField.Units.regOfFamily u ≠ 0
-- Mathlib.Order.RelIso.Set
RelEmbedding.codRestrict_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : r ↪r s) (H : ∀ (a : α), f a ∈ p)
  (a : α), (RelEmbedding.codRestrict p f H) a = ⟨f a, ⋯⟩
-- Std.Time.Time.Unit.Nanosecond
/-- Creates a new `Offset` out of a `Span`.
 -/
Std.Time.Nanosecond.Span.toOffset : Std.Time.Nanosecond.Span → Std.Time.Nanosecond.Offset
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.int_ε : ∀ {D : Type u_5} [inst : CategoryTheory.Category.{v_5, u_5} D] [inst_1 : CategoryTheory.Preadditive D]
  [inst_2 : CategoryTheory.HasShift D ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] (p q : ℤ),
  CategoryTheory.CommShift₂Setup.int.ε p q = (-1) ^ (p * q)
-- Mathlib.Order.Antisymmetrization
instWellFoundedGTAntisymmetrizationLe : ∀ {α : Type u_1} [inst : Preorder α] [WellFoundedGT α], WellFoundedGT (Antisymmetrization α fun x1 x2 => x1 ≤ x2)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instAddGroup : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddGroup (β i)] → AddGroup (Π₀ (i : ι), β i)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.map_nhdsWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (s : Set H)
  (x : H), Filter.map (↑I) (nhdsWithin x s) = nhdsWithin (↑I x) (↑I '' s)
-- Mathlib.GroupTheory.Complement
AddSubgroup.instAddActionLeftTransversal : {G : Type u_1} →
  [inst : AddGroup G] →
    {H : AddSubgroup G} →
      {F : Type u_2} →
        [inst_1 : AddGroup F] →
          [inst_2 : AddAction F G] → [AddAction.QuotientAction F H] → AddAction F H.LeftTransversal
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_inf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S₁ S₂ : Subalgebra R A), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The unit of the tensor product on graded objects is `(single₀ I).obj (𝟙_ C)`.  -/
CategoryTheory.GradedObject.Monoidal.tensorUnit : {I : Type u} →
  [AddMonoid I] →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [CategoryTheory.MonoidalCategory C] →
          [DecidableEq I] → [CategoryTheory.Limits.HasInitial C] → CategoryTheory.GradedObject I C
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.mk.injEq : ∀ (matcherName : Lean.Name) (matchType : Lean.Expr) (discrInfos : Array Lean.Meta.Match.DiscrInfo)
  (lhss : List Lean.Meta.Match.AltLHS) (isSplitter : Option Lean.Meta.Match.Overlaps) (matcherName_1 : Lean.Name)
  (matchType_1 : Lean.Expr) (discrInfos_1 : Array Lean.Meta.Match.DiscrInfo) (lhss_1 : List Lean.Meta.Match.AltLHS)
  (isSplitter_1 : Option Lean.Meta.Match.Overlaps),
  ({ matcherName := matcherName, matchType := matchType, discrInfos := discrInfos, lhss := lhss,
        isSplitter := isSplitter } =
      { matcherName := matcherName_1, matchType := matchType_1, discrInfos := discrInfos_1, lhss := lhss_1,
        isSplitter := isSplitter_1 }) =
    (matcherName = matcherName_1 ∧
      matchType = matchType_1 ∧ discrInfos = discrInfos_1 ∧ lhss = lhss_1 ∧ isSplitter = isSplitter_1)
-- Mathlib.Topology.Baire.BaireMeasurable
coborder_mem_residual : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsLocallyClosed s → coborder s ∈ residual α
-- Init.Data.SInt.Bitwise
Int32.shiftRight_or : ∀ {a b c : Int32}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- A constructor for continuous maps out of the one point compactification of `ℕ`, given a
sequence and a limit value at infinity.
 -/
OnePoint.continuousMapMkNat : {Y : Type u_3} →
  [inst : TopologicalSpace Y] → (f : ℕ → Y) → (y : Y) → Filter.Tendsto f Filter.atTop (nhds y) → C(OnePoint ℕ, Y)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_5 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a b : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx (a.mul b) =
    Lean.Grind.CommRing.Expr.denoteSAsRing ctx a * Lean.Grind.CommRing.Expr.denoteSAsRing ctx b
-- Lean.DocString.Syntax
/-- Inline mathematical notation (equivalent to LaTeX's `$` notation)  -/
Lean.Doc.Syntax.inline_math : Lean.ParserDescr
-- Mathlib.Algebra.Field.Basic
add_halves : ∀ {K : Type u_1} [inst : DivisionSemiring K] [NeZero 2] (a : K), a / 2 + a / 2 = a
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.smul_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : Group G]
  [inst_12 : MulAction G M] {n : WithTop ℕ∞} [inst_13 : ContMDiffSMul I I' n G M] (g : G),
  (Diffeomorph.smul I I' n g).symm = Diffeomorph.smul I I' n g⁻¹
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.uniformContinuous_snd : ∀ {𝕜 : Type u_3} {A : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A],
  UniformContinuous fun x => x.toProd.2
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.id_mapComp : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.LaxFunctor.id B).mapComp f g =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsPrestack.of_isPrestackFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C}, (∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows) → F.IsPrestack J
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_bot_right : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ : AddSubgroup G), ⁅H₁, ⊥⁆ = ⊥
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Icc_of_Ioc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun i => Set.Ioc (a i) (b i)
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.continuous_toCompl : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α],
  Continuous ⇑UniformSpace.Completion.toCompl
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_C_mul_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (r : R) (i : σ),
  (MvPolynomial.C r * MvPolynomial.X i).IsHomogeneous 1
-- Mathlib.Algebra.Order.Group.Defs
IsOrderedMonoid.toIsOrderedCancelMonoid : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α], IsOrderedCancelMonoid α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- `G` is a commutative additive group object if and only if the commutator map
`(x, y) ↦ x + y + (-x) + (-y)` is constant.  -/
CategoryTheory.isCommAddMonObj_iff_addCommutator_eq_toAddUnit_η : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsCommAddMonObj G ↔
    CategoryTheory.AddGrpObj.addCommutator G =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (CategoryTheory.MonoidalCategoryStruct.tensorObj G G))
        CategoryTheory.AddMonObj.zero
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.CompStruct.tensor_simplex_fst : ∀ {X Y : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (hx : e₀₁.CompStruct e₁₂ e₀₂)
  {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  {e'₀₁ : SSet.Truncated.Edge y₀ y₁} {e'₁₂ : SSet.Truncated.Edge y₁ y₂} {e'₀₂ : SSet.Truncated.Edge y₀ y₂}
  (hy : e'₀₁.CompStruct e'₁₂ e'₀₂), (hx.tensor hy).simplex.1 = hx.simplex
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.norm.sizeOf_spec : ∀ (post inv : Bool), sizeOf (Lean.Meta.Grind.AttrKind.norm post inv) = 1 + sizeOf post + sizeOf inv
-- Init.Data.Array.Lemmas
Array.flatten_append : ∀ {α : Type u_1} {xss₁ xss₂ : Array (Array α)}, (xss₁ ++ xss₂).flatten = xss₁.flatten ++ xss₂.flatten
-- Lean.Util.FoldConsts
Lean.Expr.getUsedConstants : Lean.Expr → Array Lean.Name
-- Std.Data.DTreeMap.Raw.Iterator
Std.DTreeMap.Raw.keysIter_toList : ∀ {α : Type u_1} {β : α → Type u_1} {cmp : α → α → Ordering} (m : Std.DTreeMap.Raw α β cmp), m.keysIter.toList = m.keys
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₂ = φ.unop.hom₂.op
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroUInt8UintOfNatNat : Lean.Grind.ToInt.Zero UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.map_zero : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (f : A →ₑ*[φ] B), f 1 = 1
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.IsSplittingField.instFiniteSplittingField : ∀ {K : Type v} [inst : Field K] [Finite K] (f : Polynomial K), Finite f.SplittingField
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.FactorSet.prod_eq_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] [Nontrivial α] (p : Associates.FactorSet α),
  p.prod = 0 ↔ p = ⊤
-- Mathlib.Data.Ordmap.Invariants
/-- Build a tree from three nodes, right associated (ignores the invariants).  -/
Ordnode.node3R : {α : Type u_1} → Ordnode α → α → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_sup : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Opens α} {x : α}, x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t
-- Lean.Declaration
Lean.RecursorVal.getFirstMinorIdx : Lean.RecursorVal → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- Flipping a pullback cone twice gives an isomorphic cone.  -/
CategoryTheory.Limits.PullbackCone.flipFlipIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → {f : X ⟶ Z} → {g : Y ⟶ Z} → (t : CategoryTheory.Limits.PullbackCone f g) → t.flip.flip ≅ t
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instGroup : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → Group (SeparationQuotient G)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instLatticeOfSeparatelyContinuousAdd : {G : Type u} →
  [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousAdd G] → Lattice (OpenNormalAddSubgroup G)
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.instCategoryCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (t : CategoryTheory.TwistShiftData C A) → CategoryTheory.Category.{v, u} t.Category
-- Mathlib.CategoryTheory.Category.KleisliCat
CategoryTheory.KleisliCat.ext_iff : ∀ {m : Type u → Type v} [inst : Monad m] {α β : CategoryTheory.KleisliCat m} {f g : α ⟶ β}, f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.IsTriangularizable.congr_simp : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [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],
  LieModule.IsTriangularizable R L M = LieModule.IsTriangularizable R L M
-- Mathlib.Logic.Equiv.Basic
/-- An equivalence that separates out the 0th fiber of `(Σ (n : ℕ), f n)`.  -/
Equiv.sigmaNatSucc : (f : ℕ → Type u) → (n : ℕ) × f n ≃ f 0 ⊕ (n : ℕ) × f (n + 1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k k' : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).getKey! k' =
    if cmp k k' = Ordering.eq then if (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true then k else default
    else t.getKey! k'
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.sub_sub_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b c d : X ⟶ Y), a - c - (b - d) = a - b - (c - d)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forM_eq_forM_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → m' PUnit.{w + 1}}, (forM m fun a => f a.fst) = m.keys.forM f
-- Mathlib.Topology.Order.Lattice
ContinuousAt.inf : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Min L]
  [ContinuousInf L] {f g : X → L} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun a => f a ⊓ g a) x
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
ChartedSpace.restrictLocallyRingedSpaceIso_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] (U : TopologicalSpace.Opens M),
  (ChartedSpace.restrictLocallyRingedSpaceIso U).inv =
    AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift ((ChartedSpace.locallyRingedSpace IM M).ofRestrict ⋯)
      (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mk.inj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {inst_2 : CategoryTheory.Category.{v₃, u₃} C₃}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  {pt : C₃} {inl : (F.obj Y₁).obj X₂ ⟶ pt} {inr : (F.obj X₁).obj Y₂ ⟶ pt}
  {isPushout : CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl inr} {ι : pt ⟶ (F.obj Y₁).obj Y₂}
  {inl_ι :
    autoParam (CategoryTheory.CategoryStruct.comp inl ι = (F.obj Y₁).map f₂)
      CategoryTheory.Functor.PushoutObjObj.inl_ι._autoParam}
  {inr_ι :
    autoParam (CategoryTheory.CategoryStruct.comp inr ι = (F.map f₁).app Y₂)
      CategoryTheory.Functor.PushoutObjObj.inr_ι._autoParam}
  {pt_1 : C₃} {inl_1 : (F.obj Y₁).obj X₂ ⟶ pt_1} {inr_1 : (F.obj X₁).obj Y₂ ⟶ pt_1}
  {isPushout_1 : CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl_1 inr_1}
  {ι_1 : pt_1 ⟶ (F.obj Y₁).obj Y₂}
  {inl_ι_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inl_1 ι_1 = (F.obj Y₁).map f₂)
      CategoryTheory.Functor.PushoutObjObj.inl_ι._autoParam}
  {inr_ι_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inr_1 ι_1 = (F.map f₁).app Y₂)
      CategoryTheory.Functor.PushoutObjObj.inr_ι._autoParam},
  { pt := pt, inl := inl, inr := inr, isPushout := isPushout, ι := ι, inl_ι := inl_ι, inr_ι := inr_ι } =
      { pt := pt_1, inl := inl_1, inr := inr_1, isPushout := isPushout_1, ι := ι_1, inl_ι := inl_ι_1,
        inr_ι := inr_ι_1 } →
    pt = pt_1 ∧ inl ≍ inl_1 ∧ inr ≍ inr_1 ∧ ι ≍ ι_1
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
/-- Computation of the `right.g'` field of `truncGE'.homologyData K e i j k hk hj' hj`.  -/
HomologicalComplex.truncGE'.homologyData_right_g' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i j k : ι) (hk : c.next j = k) {j' : ι'} (hj' : e.f j = j') (hj : e.BoundaryGE j),
  (HomologicalComplex.truncGE'.homologyData K e i j k hk hj' hj).right.g' = (K.truncGE' e).d j k
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.ofNat_eq_lift_iff : ∀ {a : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n = Cardinal.lift.{v, u} a ↔ OfNat.ofNat n = a
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.mul.eq_1 : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] (S' : A),
  MulMemClass.mul S' = { mul := fun a b => ⟨↑a * ↑b, ⋯⟩ }
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The distance between vertices is equal to `1` if and only if these vertices are adjacent.
 -/
SimpleGraph.dist_eq_one_iff_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.dist u v = 1 ↔ G.Adj u v
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ₀ : ∀ {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : AddCommMonoid β] [MeasurableAdd₂ β]
  {f : ℕ → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ℕ), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (n : ℕ), ProbabilityTheory.Kernel.IndepFun (∑ j ∈ Finset.range n, f j) (f n) κ μ
-- Mathlib.Logic.Encodable.Basic
/-- If `α` is encodable and `f : β → α` is invertible, then `β` is encodable as well.  -/
Encodable.ofLeftInverse : {α : Type u_1} →
  {β : Type u_2} → [Encodable α] → (f : β → α) → (finv : α → β) → (∀ (b : β), finv (f b) = b) → Encodable β
-- Mathlib.Algebra.Order.Kleene
Pi.instKleeneAlgebraForall : {ι : Type u_3} → {π : ι → Type u_4} → [(i : ι) → KleeneAlgebra (π i)] → KleeneAlgebra ((i : ι) → π i)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_zero_iff_closure_eq_closure`.

---

Two sets are at zero Hausdorff edistance if and only if they have the same closure.  -/
EMetric.hausdorffEdist_zero_iff_closure_eq_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α}, Metric.hausdorffEDist s t = 0 ↔ closure s = closure t
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const.eq_def : ∀ (basis_hd : ℝ → ℝ) (basis_tl : Tactic.ComputeAsymptotics.Basis) (c : ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl c =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons 0
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis_tl c)
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_zipWith.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a : α) (b : β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_1 : Option β) → motive x x_1),
  (match some a, some b with
    | some a, some b => h_1 a b
    | x, x_1 => h_2 x x_1) =
    h_1 a b
-- Mathlib.Topology.Specialization
/-- Type synonym for a topological space considered with its specialisation order.  -/
Specialization : Type u_1 → Type u_1
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieAlgebra.toModule : {R : Type u_1} →
  {inst : CommRing R} → {L : Type u_2} → {inst_1 : RightPreLieRing L} → [self : RightPreLieAlgebra R L] → Module R L
-- Mathlib.Algebra.Field.Defs
/-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

Do not use this lemma directly. Use `NNRat.smul_def` instead.  -/
Semifield.nnqsmul_def : ∀ {K : Type u_2} [self : Semifield K] (q : ℚ≥0) (a : K), Semifield.nnqsmul q a = ↑q * a
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for an open range `lo<...hi`.
This is an internal function.
Use `Roo.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Roo.Internal.iter : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Roo α → Std.Iter α
-- Init.Data.SInt.Lemmas
Int32.ofNat_mul : ∀ (a b : ℕ), Int32.ofNat (a * b) = Int32.ofNat a * Int32.ofNat b
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- The map of a Gaussian measure by a continuous linear map is Gaussian.  -/
ProbabilityTheory.isGaussian_map : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] (L : E →L[ℝ] F),
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (⇑L) μ)
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.fstₗ_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (p : Lex (α × β)), (OrderMonoidHom.fstₗ α β) p = (ofLex p).1
-- Mathlib.Algebra.Module.SpanRankOperations
TensorProduct.spanFinrank_top_le_of_fg : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (N : Submodule R M), N.FG → ⊤.spanFinrank ≤ N.spanFinrank