mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Constructor for `IsOneHypercoverDense.{w} F J₀ J` for a dense subsite
when the functor `F : C₀ ⥤ C` is fully faithful, `C` has pullbacks, and
any object in `C` admits a `w`-small covering family consisting of objects in `C₀`.  -/
CategoryTheory.Functor.IsOneHypercoverDense.of_hasPullbacks : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.Functor.IsDenseSubsite J₀ J F]
  [CategoryTheory.Limits.HasPullbacks C] [F.Full] [F.Faithful],
  (∀ (S : C), ∃ ι U f, CategoryTheory.Sieve.ofArrows (fun i => F.obj (U i)) f ∈ J S) → F.IsOneHypercoverDense J₀ J
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_zero : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A}, ↑0 = 0
-- Mathlib.Order.Fin.Tuple
Fin.insertNthOrderIso_symm_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1))
  (f : (i : Fin (n + 1)) → α i), (RelIso.symm (Fin.insertNthOrderIso α p)) f = (f p, p.removeNth f)
-- Mathlib.Data.NNReal.Defs
NNReal.coe_sInf : ∀ (s : Set NNReal), ↑(sInf s) = sInf (NNReal.toReal '' s)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Measurable.of_discrete : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [DiscreteMeasurableSpace α]
  {f : α → β}, Measurable f
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsInvApply.inv_apply`. -/
inv_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Inv β}
  {inst_2 : Inv F} [self : IsInvApply F α β] (f : F) (x : α), f⁻¹ x = (f x)⁻¹
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
/-- Construct a continuous linear equivalence from a linear equivalence together with
bounds in both directions.  -/
LinearEquiv.toContinuousLinearEquivOfBounds : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [inst : Ring 𝕜] →
          [inst_1 : Ring 𝕜₂] →
            [inst_2 : SeminormedAddCommGroup E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜₂ F] →
                    {σ : 𝕜 →+* 𝕜₂} →
                      {σ₂₁ : 𝕜₂ →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ] →
                            (e : E ≃ₛₗ[σ] F) →
                              (C_to C_inv : ℝ) →
                                (∀ (x : E), ‖e x‖ ≤ C_to * ‖x‖) → (∀ (x : F), ‖e.symm x‖ ≤ C_inv * ‖x‖) → E ≃SL[σ] F
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_eq_one_iff : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.relfinrank B = 1 ↔ B ≤ A
-- Mathlib.Topology.UniformSpace.Equiv
/-- `Equiv.piCongrRight` as a uniform isomorphism: this is the natural isomorphism
`Π i, β₁ i ≃ᵤ Π j, β₂ i` obtained from uniform isomorphisms `β₁ i ≃ᵤ β₂ i` for each `i`.  -/
UniformEquiv.piCongrRight : {ι : Type u_4} →
  {β₁ : ι → Type u_5} →
    {β₂ : ι → Type u_6} →
      [inst : (i : ι) → UniformSpace (β₁ i)] →
        [inst_1 : (i : ι) → UniformSpace (β₂ i)] → ((i : ι) → β₁ i ≃ᵤ β₂ i) → ((i : ι) → β₁ i) ≃ᵤ ((i : ι) → β₂ i)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isAffine_affineBasisCover : ∀ (X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.I₀), AlgebraicGeometry.IsAffine (X.affineBasisCover.X i)
-- Init.Data.Array.Lemmas
/-- Variant of `append_inj_left` instead requiring equality of the sizes of the second arrays.  -/
Array.append_inj_left' : ∀ {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → ys₁.size = ys₂.size → xs₁ = xs₂
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- If a measure `μ` on the quotient `G ⧸ Γ` of an additive group `G` by a discrete
normal subgroup `Γ` having fundamental domain, satisfies `AddQuotientMeasureEqMeasurePreimage`
relative to a standardized choice of Haar measure on `G`, and assuming `μ` is finite, then `μ` is
itself Haar.  -/
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G)
  [ν.IsAddHaarMeasure] [ν.IsAddRightInvariant] [LocallyCompactSpace G]
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] [i : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν]
  [MeasureTheory.IsFiniteMeasure μ], μ.IsAddHaarMeasure
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_of_not_integrable : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], ¬MeasureTheory.Integrable f μ → μ[f | m] = 0
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The indexing diagram.  -/
LightDiagram.diagram : LightDiagram → CategoryTheory.Functor ℕᵒᵖ FintypeCat
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Matrix.toLin_finTwoProd_toContinuousLinearMap : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] [inst : CompleteSpace 𝕜] (a b c d : 𝕜),
  LinearMap.toContinuousLinearMap
      ((Matrix.toLin (Module.Basis.finTwoProd 𝕜) (Module.Basis.finTwoProd 𝕜)) !![a, b; c, d]) =
    (a • ContinuousLinearMap.fst 𝕜 𝕜 𝕜 + b • ContinuousLinearMap.snd 𝕜 𝕜 𝕜).prod
      (c • ContinuousLinearMap.fst 𝕜 𝕜 𝕜 + d • ContinuousLinearMap.snd 𝕜 𝕜 𝕜)
-- Init.Data.SInt.Lemmas
Int16.toBitVec_add : ∀ {a b : Int16}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableAt.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'}, DifferentiableAt 𝕜 c x → ∀ (f : F), DifferentiableAt 𝕜 (fun y => c y • f) x
-- Mathlib.Order.InitialSeg
/-- The order embedding is an initial segment  -/
InitialSeg.mem_range_of_rel' : ∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} (self : InitialSeg r s) (a : α) (b : β),
  s b (self.toRelEmbedding a) → b ∈ Set.range ⇑self.toRelEmbedding
-- Std.Data.DHashMap.Internal.Defs
Std.DHashMap.Internal.List.HashesTo.mk : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List ((a : α) × β a)} {i size : ℕ},
  (∀ (h : 0 < size), ∀ p ∈ l, (↑(Std.DHashMap.Internal.mkIdx size h (hash p.fst))).toNat = i) →
    Std.DHashMap.Internal.List.HashesTo l i size
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_of_isEmpty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {a : α} {fallback : β}, m.isEmpty = true → Std.DHashMap.Raw.Const.getD m a fallback = fallback
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.PullbackShift.adjunction_counit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  (CategoryTheory.PullbackShift.adjunction φ adj).counit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.PullbackShift.natIsoComp φ G F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.PullbackShift.natTrans φ adj.counit)
        (CategoryTheory.NatTrans.PullbackShift.natIsoId D φ).inv)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  (x : CategoryTheory.SmallObject.FunctorObjIndex f πX) {Z : C} (h : CategoryTheory.SmallObject.functorObj f πX ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f x.i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πX) x)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX) h)) =
    CategoryTheory.CategoryStruct.comp x.t
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) h)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- **Alias** of the reverse direction of `ContinuousLinearMap.IsIdempotentElem.ext_iff`.

---

Idempotent operators are equal iff their range and kernels are.  -/
ContinuousLinearMap.IsIdempotentElem.ext : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : M →L[R] M},
  IsIdempotentElem p → IsIdempotentElem q → (↑p).range = (↑q).range ∧ (↑p).ker = (↑q).ker → p = q
-- Mathlib.LinearAlgebra.RootSystem.Basic
/-- In characteristic zero if there is no torsion, a finite root system is determined entirely by
its roots.  -/
RootPairing.IsRootSystem.ext : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Finite ι] [CharZero R] [IsDomain R]
  [Module.IsTorsionFree R M] {P₁ P₂ : RootPairing ι R M N} [P₁.IsRootSystem] [P₂.IsRootSystem],
  P₁.toLinearMap = P₂.toLinearMap → P₁.root = P₂.root → P₁ = P₂
-- Mathlib.Data.ULift
ULift.forall : ∀ {α : Type u} {p : ULift.{u_1, u} α → Prop}, (∀ (x : ULift.{u_1, u} α), p x) ↔ ∀ (x : α), p { down := x }
-- Mathlib.Algebra.Group.Action.Hom
/-- If the multiplicative action of `M` on `N` is compatible with multiplication on `N`, then
`fun x ↦ x • 1` is a monoid homomorphism from `M` to `N`.  -/
MonoidHom.smulOneHom : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Monoid M] → [inst_1 : MulOneClass N] → [inst_2 : MulAction M N] → [IsScalarTower M N N] → M →* N
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.Action.hugeNumber : ℕ
-- Init.Prelude
/-- The mutable state for the `MacroM` monad.  -/
Lean.Macro.State : Type
-- Mathlib.Data.List.Basic
List.perm_reverse : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.Perm l₂.reverse ↔ l₁.Perm l₂
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_hom_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).hom
      (CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)) =
    G.map (CategoryTheory.Limits.pullback.fst f g)
-- Lean.Meta.Basic
/-- Add the local declaration `<name> : <type> := <val>` to the local context and execute `k x`, where `x` is a new
free variable corresponding to the `let`-declaration. After executing `k x`, the local context is restored.
 -/
Lean.Meta.withLetDecl : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        Lean.Name →
          Lean.Expr →
            Lean.Expr →
              (Lean.Expr → n α) → optParam Bool false → optParam Lean.LocalDeclKind Lean.LocalDeclKind.default → n α
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The cosine of the angle between two vectors.  -/
InnerProductGeometry.cos_angle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  Real.cos (InnerProductGeometry.angle x y) = inner ℝ x y / (‖x‖ * ‖y‖)
-- Mathlib.Order.GaloisConnection.Basic
/-- If `α` is a partial order with bottom element (e.g., `ℕ`, `ℝ≥0`), then `WithBot.unbot' ⊥` and
coercion form a Galois insertion.  -/
WithBot.giUnbotDBot : {α : Type u} → [inst : Preorder α] → [inst_1 : OrderBot α] → GaloisInsertion (WithBot.unbotD ⊥) WithBot.some
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_algebraMap : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [inst_3 : P.LiesOver p], p.inertiaDeg' P = Module.finrank (R ⧸ p) (S ⧸ P)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.orderIsoMapComap_apply' : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] [inst_7 : RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂)
  (p : Submodule R M), (Submodule.orderIsoMapComap e) p = Submodule.comap (↑e.symm) p
-- Mathlib.GroupTheory.Submonoid.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` forms an additive
commutative monoid.  -/
AddSubmonoid.isAddCommutative_closure : ∀ (M : Type u_1) [inst : AddMonoid M] {s : Set M},
  (∀ a ∈ s, ∀ b ∈ s, a + b = b + a) → IsAddCommutative ↥(AddSubmonoid.closure s)
-- Mathlib.LinearAlgebra.DFinsupp
/-- `DFinsupp.equivFunOnFintype` as a linear equivalence.

This is the `DFinsupp` version of `Finsupp.linearEquivFunOnFintype`.  -/
DFinsupp.linearEquivFunOnFintype : {ι : Type u_1} →
  {R : Type u_3} →
    {M : ι → Type u_5} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → [Fintype ι] → (Π₀ (i : ι), M i) ≃ₗ[R] (i : ι) → M i
-- Init.Data.UInt.Bitwise
UInt16.toUInt32_and : ∀ (a b : UInt16), (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
-- Mathlib.Order.Atoms
IsStronglyCoatomic.of_wellFounded_gt : ∀ {α : Type u_2} [inst : PartialOrder α], (WellFounded fun x1 x2 => x1 > x2) → IsStronglyCoatomic α
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a},
  p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ (a_1 : α), List.count a_1 p.support.tail = 1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- In a space with second countable topology, strongly measurable and measurable are equivalent.  -/
aestronglyMeasurable_iff_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β]
  [SecondCountableTopology β], MeasureTheory.AEStronglyMeasurable f μ ↔ AEMeasurable f μ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
IsUnit.finset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {a : α}, IsUnit a → IsUnit {a}
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Add β] [ContinuousAdd β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : β), MeasureTheory.AEStronglyMeasurable (fun x => f x + c) μ
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffWithinAt_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {x : E}
  {n : WithTop ℕ∞} {c : F}, ContDiffWithinAt 𝕜 n (fun x => c) s x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_inter_add_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasurableSet t → μ (s ∩ t) + μ (s \ t) = μ s
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_succ : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ), ↑n.succ = ↑n + 1
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.hom_ext_iff : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} {f g : Monoid.PushoutI φ →* K},
  f = g ↔
    (∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)) ∧
      f.comp (Monoid.PushoutI.base φ) = g.comp (Monoid.PushoutI.base φ)
-- Mathlib.Data.List.Sort
List.decidableSortedGE : {α : Type u_1} → [inst : Preorder α] → [DecidableLE α] → DecidablePred List.SortedGE
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.pow_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N)
  [CategoryTheory.IsMonHom g], CategoryTheory.CategoryStruct.comp (f ^ n) g = CategoryTheory.CategoryStruct.comp f g ^ n
-- Mathlib.GroupTheory.Nilpotent
/-- Any descending central series for a group is bounded below by the lower central series.  -/
Subgroup.descending_central_series_ge_lower : ∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
  Subgroup.IsDescendingCentralSeries H → ∀ (n : ℕ), ⊤.lowerCentralSeries n ≤ H n
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_le_span_content : ∀ {R : Type u_3} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R},
  p.contentIdeal ≤ Ideal.span {p.content}
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.Kind.hypothesis.sizeOf_spec : sizeOf Mathlib.Tactic.LibraryRewrite.Kind.hypothesis = 1
-- Mathlib.Data.Set.Pairwise.Basic
exists_ne_mem_inter_of_not_pairwise_disjoint : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → Set α},
  ¬Pairwise (Function.onFun Disjoint f) → ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_sum_apply : ∀ {ι : Type u_1} (f : ι → ℕ → ℂ) (S : Finset ι) (s : ℂ) (n : ℕ),
  LSeries.term (∑ i ∈ S, f i) s n = ∑ i ∈ S, LSeries.term (f i) s n
-- Mathlib.Algebra.GroupWithZero.Defs
CommGroupWithZero.toGroupWithZero : {G₀ : Type u_2} → [self : CommGroupWithZero G₀] → GroupWithZero G₀
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α}, ∅.contains k = false
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
/-- Tensor products of copies equal copies of tensor products.  -/
CategoryTheory.CopyDiscardCategory.copy_tensor : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.CopyDiscardCategory C] (X Y : C),
  CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.MonoidalCategory.tensorμ X X Y Y)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.collect : Lean.MVarId → Lean.Try.Config → Lean.MetaM Lean.Meta.Try.Info
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.toLowerSet_symm : ∀ {α : Type u_1}, Topology.WithLowerSet.toLowerSet.symm = Topology.WithLowerSet.ofLowerSet
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.Generators.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : IsFreeAddGroup G], IsFreeAddGroup.Generators G = ⋯.choose
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.eq_empty_iff_size_eq_zero : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.TransCmp cmp],
  t = ∅ ↔ t.size = 0
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F)
  (γ : Path a b), curveIntegralFun ω γ.symm = fun x => (-curveIntegralFun ω γ) (1 - x)
-- Init.Data.Nat.Lemmas
Nat.mul_ne_mul_left : ∀ {a b c : ℕ}, a ≠ 0 → (b * a ≠ c * a ↔ b ≠ c)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Graded ring homomorphisms map one to one.  -/
GradedRingHom.map_one : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ), f 1 = 1
-- Mathlib.Data.Multiset.ZeroCons
Multiset.ssubset_singleton_iff : ∀ {α : Type u_1} {s : Multiset α} {a : α}, s ⊂ {a} ↔ s = 0
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.completeLattice : {α : Type u_1} → [inst : LE α] → CompleteLattice (UpperSet α)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {x : M},
  x ∈ f.source → ∀ {s : Set M}, s ∈ nhds x → ↑(f.extend I) '' s ∈ nhds (↑(f.extend I) x)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toList_zip_of_finite_right : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Productive α₁ Id] [Std.Iterators.Finite α₂ Id],
  (it₁.zip it₂).toList = (Std.Iter.take it₂.toList.length it₁).toList.zip it₂.toList
-- Mathlib.Data.Set.Function
Set.BijOn.surjOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → Set.SurjOn f s t
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A measure is called finite at filter `f` if it is finite at some set `s ∈ f`.
Equivalently, it is eventually finite at `s` in `f.small_sets`.  -/
MeasureTheory.Measure.FiniteAtFilter : {α : Type u_1} → {_m0 : MeasurableSpace α} → MeasureTheory.Measure α → Filter α → Prop
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.leftRight.sizeOf_spec : sizeOf Lean.Meta.Grind.EMatchTheoremKind.leftRight = 1
-- Lean.Parser.Basic
Lean.Parser.nameLitFn : Lean.Parser.ParserFn
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
/-- For each nonempty, directed set `s` which is bounded below, `sInf s` is
the greatest lower bound of `s`.  -/
ConditionallyCompletePartialOrderInf.isGLB_csInf_of_directed : ∀ {α : Type u_3} [self : ConditionallyCompletePartialOrderInf α] (s : Set α),
  DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An action is `1`-pretransitive iff it is pretransitive.  -/
MulAction.is_one_pretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsMultiplyPretransitive G α 1 ↔ MulAction.IsPretransitive G α