mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Trie.node.inj : ∀ {α : Type} {values : Array α} {star : Option Lean.Meta.RefinedDiscrTree.TrieIndex}
  {labelledStars : Std.HashMap ℕ Lean.Meta.RefinedDiscrTree.TrieIndex}
  {children : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex}
  {pending : Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)} {values_1 : Array α}
  {star_1 : Option Lean.Meta.RefinedDiscrTree.TrieIndex}
  {labelledStars_1 : Std.HashMap ℕ Lean.Meta.RefinedDiscrTree.TrieIndex}
  {children_1 : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex}
  {pending_1 : Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)},
  { values := values, star := star, labelledStars := labelledStars, children := children, pending := pending } =
      { values := values_1, star := star_1, labelledStars := labelledStars_1, children := children_1,
        pending := pending_1 } →
    values = values_1 ∧ star = star_1 ∧ labelledStars = labelledStars_1 ∧ children = children_1 ∧ pending = pending_1
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- The quotient map from the free additive monoid on `α` to the presented additive
monoid with the same generators and the given relations `rels`  -/
PresentedAddMonoid.mk : {α : Type u_1} → (rels : FreeAddMonoid α → FreeAddMonoid α → Prop) → FreeAddMonoid α →+ PresentedAddMonoid rels
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMonObj.add =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Init.Data.List.Lemmas
List.filter_replicate_of_pos : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α}, p a = true → List.filter p (List.replicate n a) = List.replicate n a
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.Internal.List.getValueCast!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) [inst_2 : Inhabited (β a)]
  (l : List ((a : α) × β a)), Std.Internal.List.getValueCast! a l = (Std.Internal.List.getValueCast? a l).get!
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- If `σ` and `σ'` are mutually inverse, then one is `RingHomIsometric` if the other is. Not an
instance, as it would cause loops.  -/
RingHomIsometric.inv : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : SeminormedRing 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂)
  {σ' : 𝕜₂ →+* 𝕜₁} [RingHomInvPair σ σ'] [RingHomIsometric σ], RingHomIsometric σ'
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- A family of seminorms is separating iff it induces a T₁ topology.  -/
WithSeminorms.separating_iff_T1 : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p → ((∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0) ↔ T1Space E)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
/-- A surjective, quasi-compact, flat morphism is a quotient map.  -/
AlgebraicGeometry.Flat.isQuotientMap_of_surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.QuasiCompact f]
  [AlgebraicGeometry.Surjective f], Topology.IsQuotientMap ⇑f
-- Batteries.Data.String.Legacy
/-- Auxiliary definition for `String.Legacy.foldl`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.foldlAux`.
 -/
String.Legacy.foldlAux : {α : Type u} → (α → Char → α) → String → String.Pos.Raw → String.Pos.Raw → α → α
-- Std.Async.Basic
Std.Async.EAsync.instOrElse : {ε α : Type} → OrElse (Std.Async.EAsync ε α)
-- Mathlib.Order.SupClosed
SupClosed.preimage : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {s : Set α}
  [inst_2 : FunLike F β α] [SupHomClass F β α], SupClosed s → ∀ (f : F), SupClosed (⇑f ⁻¹' s)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is equicontinuous at some `x₀` within a set `S`, its closure for the
product topology is also equicontinuous at `x₀` within `S`. This would also be true for the coarser
topology of pointwise convergence on `S ∪ {x₀}`, see `Set.EquicontinuousWithinAt.closure'`.  -/
Set.EquicontinuousWithinAt.closure : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {A : Set (X → α)} {S : Set X} {x₀ : X},
  A.EquicontinuousWithinAt S x₀ → (closure A).EquicontinuousWithinAt S x₀
-- Mathlib.Order.Atoms
OrderDual.instIsAtomistic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] [h : IsCoatomistic α], IsAtomistic αᵒᵈ
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mk_of_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (x : N),
  AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr x)) = AddMonoid.Coprod.inr x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtComplexPlaces.eq_1 : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K) (w : NumberField.InfinitePlace K),
  NumberField.mixedEmbedding.normAtComplexPlaces x w =
    if hw : w.IsReal then x.1 ⟨w, hw⟩ else (NumberField.mixedEmbedding.normAtPlace w) x
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.extract : ∀ {l m r : List Char} {it₁ it₂ : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l (m ++ r) it₁ →
    String.Legacy.Iterator.ValidFor (m.reverse ++ l) r it₂ → it₁.extract it₂ = String.ofList m
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.centralMoment_zero_measure : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {p : ℕ}, ProbabilityTheory.centralMoment X p 0 = 0
-- Mathlib.Order.Filter.Map
Filter.disjoint_comap : ∀ {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β},
  Disjoint g₁ g₂ → Disjoint (Filter.comap m g₁) (Filter.comap m g₂)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality_assoc : ∀ {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] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (S₁.map F).HasHomology] [inst_8 : (S₂.map F).HasHomology]
  [inst_9 : F.PreservesLeftHomologyOf S₁] [inst_10 : F.PreservesLeftHomologyOf S₂] {Z : D}
  (h : (S₂.map F).homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapHomologyIso F).inv h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ)) h)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.inverse'.congr_simp : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : N → M} (f f_1 : X →ₑ[φ] Y) (e_f : f = f_1) (g g_1 : Y → X) (e_g : g = g_1) (k : Function.RightInverse φ' φ)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), f.inverse' g k h₁ h₂ = f_1.inverse' g_1 k ⋯ ⋯
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.toNonUnitalSubring_toSubring : ∀ {R : Type u} [inst : NonAssocRing R] (S : Subring R), S.toNonUnitalSubring.toSubring ⋯ = S
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.Over.mk : {S : AlgebraicGeometry.Scheme} →
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X : AlgebraicGeometry.Scheme} →
          [inst_2 : X.Over S] →
            {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X} →
              («over» : autoParam ((j : 𝒰.I₀) → (𝒰.X j).Over S) AlgebraicGeometry.Scheme.Cover.Over.over._autoParam) →
                autoParam (∀ (j : 𝒰.I₀), AlgebraicGeometry.Scheme.Hom.IsOver (𝒰.f j) S)
                    AlgebraicGeometry.Scheme.Cover.Over.isOver_map._autoParam →
                  AlgebraicGeometry.Scheme.Cover.Over S 𝒰
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.linearEquiv_symm_apply : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  [inst_3 : Semiring T] [inst_4 : Module R T] {v : AbsoluteValue T S} (x : T),
  (WithAbs.linearEquiv R v).symm x = WithAbs.toAbs v x
-- Mathlib.RingTheory.HopfAlgebra.Basic
CommSemiring.antipode_eq_id : ∀ (R : Type u) [inst : CommSemiring R], HopfAlgebraStruct.antipode R = LinearMap.id
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.toSmoothPartitionOfUnity_apply : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s)
  [inst_6 : T2Space M] [inst_7 : IsManifold I (↑⊤) M] (i : ι) (x : M),
  (fs.toSmoothPartitionOfUnity i) x = ↑(fs.toFun i) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - ↑(fs.toFun j) x)
-- Batteries.Tactic.PrintDependents
Batteries.Tactic.CollectDependents.State.mk.inj : ∀ {otherAxiom : Bool} {result : Lean.NameMap Bool} {otherAxiom_1 : Bool} {result_1 : Lean.NameMap Bool},
  { otherAxiom := otherAxiom, result := result } = { otherAxiom := otherAxiom_1, result := result_1 } →
    otherAxiom = otherAxiom_1 ∧ result = result_1
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_add_left_right : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime x (x * z + y)
-- Mathlib.Order.Interval.Finset.Defs
Finset.Icc_orderDual_def : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : αᵒᵈ),
  Finset.Icc a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Icc (OrderDual.ofDual b) (OrderDual.ofDual a))
-- Mathlib.Analysis.Normed.Group.Defs
toNNReal_enorm : ∀ {E : Type u_8} [inst : NNNorm E] (x : E), ‖x‖ₑ.toNNReal = ‖x‖₊
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciInf_eq_ite : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {p : Prop} [inst_1 : Decidable p] {f : p → α},
  ⨅ (h : p), f h = if h : p then f h else sInf ∅
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.semilatticeInf : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : SemilatticeInf β] →
        [inst_2 : Zero β] →
          [inst_3 : TopologicalSpace β] → [ContinuousInf β] → SemilatticeInf (CompactlySupportedContinuousMap α β)
-- Init.Data.Random
StdGen.mk.injEq : ∀ (s1 s2 s1_1 s2_1 : ℕ), ({ s1 := s1, s2 := s2 } = { s1 := s1_1, s2 := s2_1 }) = (s1 = s1_1 ∧ s2 = s2_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_of_isSome_minKey?_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α}, (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey?.isSome = true → t.minKey?.isSome = true
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.lift.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : M ⟶ K) (β : CochainComplex.HomComplex.Cochain M L (-1))
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0),
  CochainComplex.mappingCocone.lift φ α β hαβ =
    (CochainComplex.mappingCocone.liftCocycle φ (CochainComplex.HomComplex.Cocycle.ofHom α) β
        CochainComplex.mappingCocone.lift._proof_1 ⋯).homOf
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_inv : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α] (s : NonemptyInterval α),
  s⁻¹.toProd.2 = s.toProd.1⁻¹
-- Mathlib.Order.Hom.Lattice
InfHom.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : Min α], InfHom.instInhabited α = { default := InfHom.id α }
-- Init.Data.Rat.Basic
/-- Rational number strictly less than relation, as a `Bool`.  -/
Rat.blt : ℚ → ℚ → Bool
-- Mathlib.CategoryTheory.Monoidal.Conv
CategoryTheory.Conv.instMonoid : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : C} → [CategoryTheory.ComonObj M] → [CategoryTheory.MonObj N] → Monoid (CategoryTheory.Conv M N)
-- Std.Time.Date.Unit.Month
/-- Clips the day to be within the valid range.
 -/
Std.Time.Month.Ordinal.clipDay : Bool → Std.Time.Month.Ordinal → Std.Time.Day.Ordinal → Std.Time.Day.Ordinal
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearEquiv_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (a : A₁), ↑e a = e a
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.opOpEquivalence_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.opOpEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖᵒᵖ)
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Suppose `J ≤ I` are ideals of `R`, then `R / I` is the localization away from `r : R / J`
if `r - 1 ∈ I` and for some `n`, `r ^ n • I ≤ J`.
For sake of usability, we state this for surjective ring maps instead of ideals.  -/
IsLocalization.Away.of_surjective_of_isScalarTower : ∀ {S : Type u_4} {T : Type u_5} [inst : CommRing S] [inst_1 : CommRing T] [inst_2 : Algebra S T] {R : Type u_6}
  [inst_3 : CommRing R] [inst_4 : Algebra R S] [inst_5 : Algebra R T] [IsScalarTower R S T],
  Function.Surjective ⇑(algebraMap S T) →
    Function.Surjective ⇑(algebraMap R S) →
      ∀ (r : R),
        IsUnit ((algebraMap R T) r) →
          ∀ {n : ℕ},
            r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S) →
              IsLocalization.Away ((algebraMap R S) r) T
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.etaleTopology_le_proetaleTopology : AlgebraicGeometry.Scheme.etaleTopology ≤ AlgebraicGeometry.Scheme.proetaleTopology
-- Mathlib.Order.SuccPred.Limit
WithTop.isSuccLimit_iff : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [NoMaxOrder α] {x : WithTop α},
  Order.IsSuccLimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ Order.IsSuccLimit y
-- Mathlib.Analysis.Convex.Strict
strictConvex_Ici : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β), StrictConvex 𝕜 (Set.Ici r)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instRingOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : Ring Mᵐᵒᵖ], DomMulAct.instRingOfMulOpposite = inst
-- Mathlib.Analysis.Convex.Basic
Directed.convex_iUnion : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E},
  Directed (fun x1 x2 => x1 ⊆ x2) s → (∀ ⦃i : ι⦄, Convex 𝕜 (s i)) → Convex 𝕜 (⋃ i, s i)
-- Mathlib.Probability.Kernel.Disintegration.Unique
/-- A finite kernel which satisfies the disintegration property is almost everywhere equal to the
disintegration kernel.  -/
ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {ρ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel ρ] {κ : ProbabilityTheory.Kernel (α × β) Ω}
  [ProbabilityTheory.IsFiniteKernel κ],
  ρ.fst.compProd κ = ρ → ∀ (a : α), ∀ᵐ (x : β) ∂ρ.fst a, κ (a, x) = ρ.condKernel (a, x)
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_mul : ∀ {M : Type u_10} {F : Type u_11} [inst : Mul M] [inst_1 : FunLike F M M] [MulHomClass F M M] (f : F) (n : ℕ) (x y : M),
  (⇑f)^[n] (x * y) = (⇑f)^[n] x * (⇑f)^[n] y
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
  (z₃ : W.LeftFraction z₁.Y' z₂.Y'),
  CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁)
        (CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂) =
      CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (z₁.comp₀ z₂ z₃)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Composition of `OrderMonoidHom`s as an `OrderMonoidHom`.  -/
OrderMonoidHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : Preorder γ] →
            [inst_3 : MulOneClass α] →
              [inst_4 : MulOneClass β] → [inst_5 : MulOneClass γ] → (β →*o γ) → (α →*o β) → α →*o γ
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.commProb_odd : ∀ {n : ℕ}, Odd n → commProb (DihedralGroup n) = (↑n + 3) / (4 * ↑n)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.liminf_sub_const : ∀ {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) (c : ENNReal),
  Filter.liminf (fun i => f i - c) F = Filter.liminf f F - c
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ofRingHom_coe_ringHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S) (g : S →+* R)
  (h₁ : (↑f).comp g = RingHom.id S) (h₂ : g.comp ↑f = RingHom.id R), RingEquiv.ofRingHom (↑f) g h₁ h₂ = f
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] (f : LocallyBoundedMap α β),
  (LocallyBoundedMap.id β).comp f = f
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- **Equational criterion for vanishing**
[A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term].

Assume that the $m_i$ generate $M$. Then the expression $\sum_i m_i \otimes n_i$ vanishes
trivially if and only if it vanishes.  -/
TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι : Type u_4} [inst_5 : Fintype ι] {m : ι → M} {n : ι → N},
  Submodule.span R (Set.range m) = ⊤ → (TensorProduct.VanishesTrivially R m n ↔ ∑ i, m i ⊗ₜ[R] n i = 0)
-- Mathlib.Algebra.CharP.Defs
ExpChar.exists : ∀ (R : Type u_1) [inst : Ring R] [IsDomain R], ∃ q, ExpChar R q
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.prop_map_iff : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) (Y : D),
  P.map F Y ↔ ∃ X, P X ∧ Nonempty (F.obj X ≅ Y)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_mono : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : Associates α},
  a ≤ b → a.factors ≤ b.factors
-- Mathlib.Geometry.Manifold.BumpFunction
/-- If `f : SmoothBumpFunction I c` is a smooth bump function and `g : M → G` is a function smooth
on the source of the chart at `c`, then `f • g` is smooth on the whole manifold.  -/
SmoothBumpFunction.contMDiff_smul : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {G : Type u_1}
  [inst_8 : NormedAddCommGroup G] [inst_9 : NormedSpace ℝ G] {g : M → G},
  ContMDiffOn I (modelWithCornersSelf ℝ G) (↑⊤) g (chartAt H c).source →
    ContMDiff I (modelWithCornersSelf ℝ G) ↑⊤ fun x => ↑f x • g x
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.tensorTensorTensorAssoc_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P] (m : M) (n : N) (p : P)
  (q : Q), (TensorProduct.tensorTensorTensorAssoc R M N P Q) (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)) = m ⊗ₜ[R] (n ⊗ₜ[R] p) ⊗ₜ[R] q
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_pred_of_le : ∀ {n : ℕ} (p i : Fin (n + 1)) (h : p ≤ i) (hp : p ≠ 0), (p.pred hp).predAbove i = i.pred ⋯
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype : ∀ (k : Type u) {G : Type v} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G) [S.FiniteIndex],
  (Rep.indFunctor k S.subtype).IsRightAdjoint
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- `X` and `Y` are birational if there exists a partial isomorphism between them.  -/
AlgebraicGeometry.Scheme.Birational : AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Prop
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.cons_eq_zero_iff : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] {v : Fin n → α} {x : α}, Matrix.vecCons x v = 0 ↔ x = 0 ∧ v = 0
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableOn_congr : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M},
  (∀ y ∈ s, f₁ y = f y) → (MDiff[s] f₁ ↔ MDiff[s] f)
-- Mathlib.RingTheory.AdjoinRoot
/-- The elements `1, root f, ..., root f ^ (d - 1)` form a basis for `AdjoinRoot f`,
where `f` is an irreducible polynomial over a field of degree `d`.  -/
AdjoinRoot.powerBasisAux : {K : Type u_5} → [inst : Field K] → {f : Polynomial K} → f ≠ 0 → Module.Basis (Fin f.natDegree) K (AdjoinRoot f)
-- Mathlib.CategoryTheory.Limits.Filtered
/-- Class for having all cofiltered limits of a given size.  -/
CategoryTheory.Limits.HasCofilteredLimitsOfSize : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Logic.Equiv.Fin.Basic
Fin.preimage_apply_01_prod' : ∀ {α : Type u} (s t : Set α), (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi ![s, t]
-- Init.Data.Array.Lemmas
Array.replicate_succ : ∀ {n : ℕ} {α : Type u_1} {a : α}, Array.replicate (n + 1) a = (Array.replicate n a).push a
-- Std.Http.Server.Handler
/-- Builds a `StatelessHandler` from a request function and a continue callback
 -/
Std.Http.Server.Handler.withContinue : Std.Http.Server.StatelessHandler → (Std.Http.Request.Head → Std.Async.Async Bool) → Std.Http.Server.StatelessHandler
-- Init.Data.Order.PackageFactories
Std.LinearPreorderPackage.toOrd : {α : Type u} → [self : Std.LinearPreorderPackage α] → Ord α
-- Mathlib.Data.List.SplitBy
List.splitBy_ne_nil : ∀ {α : Type u_1} {r : α → α → Bool} {l : List α}, List.splitBy r l ≠ [] ↔ l ≠ []
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : DecidableEq β] {f : α → β}, Finset.image f 0 = {f 0}