mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.le_of_natCast_le_natCast : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a b : ℕ), ↑a ≤ ↑b → a ≤ b
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubmonoid_union : ∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α] {s t : Set α},
  fixingAddSubmonoid M (s ∪ t) = fixingAddSubmonoid M s ⊓ fixingAddSubmonoid M t
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.finiteArchimedeanClassOrderIsoLex.eq_1 : ∀ (Γ : Type u_1) (R : Type u_2) [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R],
  HahnSeries.finiteArchimedeanClassOrderIsoLex Γ R =
    OrderIso.ofHomInv (HahnSeries.finiteArchimedeanClassOrderHomLex Γ R)
      (HahnSeries.finiteArchimedeanClassOrderHomInvLex Γ R) ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_nonneg : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) (i : ℕ), 0 ≤ T.singularValues i
-- Mathlib.Algebra.Order.Star.Real
instSelfAdjointDecomposeOfAddLeftMono : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : Lattice R] [AddLeftMono R] [inst_3 : Star R], SelfAdjointDecompose R
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_σ_succ : ∀ {n : ℕ} {i : Fin (n + 1)},
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.succ) (SimplexCategoryGenRel.σ i) =
    CategoryTheory.CategoryStruct.id (SimplexCategoryGenRel.mk n)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.as_ideal_lt_as_ideal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x y : ProjectiveSpectrum 𝒜), x.asHomogeneousIdeal < y.asHomogeneousIdeal ↔ x < y
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_span_singleton : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M), (R ∙ x).FG
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  (t : CategoryTheory.Limits.ColimitCocone F) (j : J) {Z : C} (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.cocone.ι.app j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.isoColimitCocone t).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) h
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurable_memPartitionSet : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (t n)) → ∀ (n : ℕ), Measurable (memPartitionSet t n)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_ciSup' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α]
  [inst_1 : ConditionallyCompleteLinearOrderBot β] (e : α ≃o β) (f : ι → α), e (⨆ i, f i) = ⨆ i, e (f i)
-- Init.Data.BitVec.Lemmas
BitVec.msb_ofBool : ∀ (b : Bool), (BitVec.ofBool b).msb = b
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Metric.controlled_of_isUniformEmbedding : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  IsUniformEmbedding f →
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality**, `ℝ≥0∞` version with real conjugate exponents.  -/
ENNReal.young_inequality : ∀ (a b : ENNReal) {p q : ℝ}, p.HolderConjugate q → a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphismClass.toRelHomClass : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Preorder α} {inst_1 : Preorder β}
  {inst_2 : FunLike F α β} [self : PseudoEpimorphismClass F α β],
  RelHomClass F (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Init.Data.Array.Lemmas
Array.getElem_push_eq : ∀ {α : Type u_1} {xs : Array α} {x : α}, (xs.push x)[xs.size] = x
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.hasLimit_of_reflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D)
  (R : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasLimit (F.comp R)] [CategoryTheory.Reflective R],
  CategoryTheory.Limits.HasLimit F
-- Init.Data.Array.Zip
Array.getElem?_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : Array α} {bs : Array β} {f : Option α → Option β → γ} {i : ℕ},
  (Array.zipWithAll f as bs)[i]? =
    match as[i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)
-- Mathlib.LinearAlgebra.Pi
/-- Transporting dependent functions through an equivalence of the base,
expressed as a "simplification".

This is `Equiv.piCongrLeft` as a `LinearEquiv`  -/
LinearEquiv.piCongrLeft : (R : Type u) →
  {ι : Type x} →
    {ι' : Type x'} →
      [inst : Semiring R] →
        (φ : ι → Type u_1) →
          [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_2 : (i : ι) → Module R (φ i)] → (e : ι' ≃ ι) → ((i' : ι') → φ (e i')) ≃ₗ[R] (i : ι) → φ i
-- Mathlib.FieldTheory.Perfect
coe_frobenius_comp_coe_frobeniusEquiv_symm : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  ⇑(frobenius R p) ∘ ⇑(frobeniusEquiv R p).symm = id
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.StronglyConnectedComponent.instCoe : {V : Type u_2} → [inst : Quiver V] → Coe V (Quiver.StronglyConnectedComponent V)
-- Mathlib.Order.WithBotTop
WithBotTop.rec_bot : ∀ {ι : Type u_1} {motive : WithBotTop ι → Sort u_2} (bot : motive ⊥) (coe : (a : ι) → motive (WithBotTop.coe a))
  (top : motive ⊤), WithBotTop.rec bot coe top ⊥ = bot
-- Mathlib.Order.Category.BoolAlg
/-- Turn a morphism in `BoolAlg` back into a `BoundedLatticeHom`.  -/
BoolAlg.Hom.hom : {X Y : BoolAlg} → X.Hom Y → BoundedLatticeHom ↑X ↑Y
-- Init.Data.List.MinMaxOn
List.maxOn?_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α}
  {xs : List α}, List.maxOn? f (x :: xs) = some ((List.maxOn? f xs).elim x (maxOn f x))
-- Mathlib.Util.DelabNonCanonical
/-- Returns `true` iff the given instance is defeq to the instance synthesized for its type, and
returns `false` otherwise (including if instance synthesis fails).  -/
Lean.Meta.isCanonicalInstance : Lean.Expr → Lean.MetaM Bool
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Given a function `f` supplied with arguments `args`, returns an array whose n-th element
is set to the kind of the n-th argument's associated parameter.
We do not assume the expression `mkAppN f args` is sensical,
and this function captures errors (except for panics) and returns the empty array in that case.

The returned array might be longer than the number of arguments.
It gives parameter kinds for the fully-applied function.
Note: the `defVal` expressions are only guaranteed to be valid for parameters associated to the supplied arguments;
after this, they might refer to temporary fvars.

This function properly handles "overapplied" functions.
For example, while `id` takes one explicit argument, it can take more than one explicit
argument when its arguments are specialized to function types, like in `id id 2`.
 -/
Lean.PrettyPrinter.Delaborator.getParamKinds : Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.PrettyPrinter.Delaborator.ParamKind)
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_nonpos : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f : α → M},
  (∀ a ∈ s, f a ≤ 0) → ∀ (a : α), s.indicator f a ≤ 0
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightUnitorEquivalence_unitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.prod.rightUnitorEquivalence C).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × CategoryTheory.Discrete PUnit.{w + 1}))
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Context.mk.sizeOf_spec : ∀ (config : Lean.Meta.Sym.Simp.Config) (initialLCtxSize dischargeDepth : ℕ),
  sizeOf { config := config, initialLCtxSize := initialLCtxSize, dischargeDepth := dischargeDepth } =
    1 + sizeOf config + sizeOf initialLCtxSize + sizeOf dischargeDepth
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalarsComp'_hom_app_hom_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T) (gf : R →+* T) (hfg : gf = g.comp f) (X : AlgCat T) (a : ↑X),
  (AlgCat.Hom.hom ((AlgCat.restrictScalarsComp' f g gf hfg).hom.app X)) a = a
-- Mathlib.Data.Set.Prod
Set.mapsTo_swap_prod : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), Set.MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_neg_eq_arg_sub_pi_iff : ∀ {x : ℂ}, (-x).arg = x.arg - Real.pi ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.instInhabitedSimpM : {α : Type} → Inhabited (Lean.Meta.SimpM α)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_assignments_size : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : ℕ),
  (f.deleteOne id).assignments.size = f.assignments.size
-- Mathlib.Analysis.Convex.Hull
convexHull_min : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E}, s ⊆ t → Convex 𝕜 t → (convexHull 𝕜) s ⊆ t
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.directLimitDiagram_obj_carrier : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : Preorder ι] (G : ι → Type v)
  [inst_2 : (i : ι) → AddCommGroup (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)] (i : ι), ↑((ModuleCat.directLimitDiagram G f).obj i) = G i
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_eq_zero : ∀ {α : Type u_1} [inst : Zero α] {a : Colex α}, ofColex a = 0 ↔ a = 0
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
mem_balancedCore_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E} {x : E},
  x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
-- Mathlib.Analysis.Analytic.Composition
/-- Formal composition of two formal multilinear series. The `n`-th coefficient in the composition
is defined to be the sum of `q.compAlongComposition p c` over all compositions of
`n`. In other words, this term (as a multilinear function applied to `v_0, ..., v_{n-1}`) is
`∑'_{k} ∑'_{i₁ + ... + iₖ = n} qₖ (p_{i_1} (...), ..., p_{i_k} (...))`, where one puts all variables
`v_0, ..., v_{n-1}` in increasing order in the dots.

In general, the composition `q ∘ p` only makes sense when the constant coefficient of `p` vanishes.
We give a general formula but which ignores the value of `p 0` instead.
 -/
FormalMultilinearSeries.comp : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        [inst : CommRing 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : AddCommGroup F] →
              [inst_3 : AddCommGroup G] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : Module 𝕜 G] →
                      [inst_7 : TopologicalSpace E] →
                        [inst_8 : TopologicalSpace F] →
                          [inst_9 : TopologicalSpace G] →
                            [inst_10 : IsTopologicalAddGroup E] →
                              [inst_11 : ContinuousConstSMul 𝕜 E] →
                                [inst_12 : IsTopologicalAddGroup F] →
                                  [inst_13 : ContinuousConstSMul 𝕜 F] →
                                    [inst_14 : IsTopologicalAddGroup G] →
                                      [inst_15 : ContinuousConstSMul 𝕜 G] →
                                        FormalMultilinearSeries 𝕜 F G →
                                          FormalMultilinearSeries 𝕜 E F → FormalMultilinearSeries 𝕜 E G
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.alter : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α}
  {f : Option (x k) → Option (x k)} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_faceOpposite_ssubset_closedInterior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [Nontrivial k] [ZeroLEOneClass k] {n : ℕ} [inst_7 : NeZero n]
  (s : Affine.Simplex k P n) (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊂ s.closedInterior
-- Batteries.Recycling.MonadSatisfying.Basic
SatisfiesM_StateRefT_eq : ∀ {m : Type → Type} {ω σ α : Type} {p : α → Prop} {x : StateRefT' ω σ m α} [inst : Monad m],
  SatisfiesM p x ↔ ∀ (s : ST.Ref ω σ), SatisfiesM p (x s)
-- Init.Data.String.OrderInstances
String.Slice.Pos.instLECoOfNatIntHAddCastUtf8ByteSize : ∀ {s : String.Slice}, Lean.Grind.ToInt.LE s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_length : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v), w.getVert w.length = v
-- Mathlib.Order.SupIndep
Finset.instPartialOrder.hcongr_1 : ∀ (α α' : Type u_1), α = α' → Finset.instPartialOrder ≍ Finset.instPartialOrder
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminator.mk.injEq : ∀ (induction : Bool) (typeNames : Array Lean.Name) (elimName : Lean.Name) (induction_1 : Bool)
  (typeNames_1 : Array Lean.Name) (elimName_1 : Lean.Name),
  ({ induction := induction, typeNames := typeNames, elimName := elimName } =
      { induction := induction_1, typeNames := typeNames_1, elimName := elimName_1 }) =
    (induction = induction_1 ∧ typeNames = typeNames_1 ∧ elimName = elimName_1)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
AlgHom.map_adjugate : ∀ {n : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_1} {A : Type u_2} {B : Type u_3}
  [inst_2 : CommSemiring R] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →ₐ[R] B) (M : Matrix n n A), f.mapMatrix M.adjugate = (f.mapMatrix M).adjugate
-- Init.Data.Int.Gcd
Int.gcd_add_mul_left_left : ∀ (m n k : ℤ), (n + m * k).gcd m = n.gcd m
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `pow k n = n ^ k`, except `pow 0 0 = 0`.  -/
ArithmeticFunction.pow : ℕ → ArithmeticFunction ℕ
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.mk.sizeOf_spec : ∀ {X : Type u_2} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} [inst_1 : SizeOf X]
  [inst_2 : (a a_1 : Set X) → SizeOf (P a a_1)] (C U : Set X) (P_C_U : P C U) (closed_C : IsClosed C)
  (open_U : IsOpen U) (subset : C ⊆ U)
  (hP :
    ∀ {c u : Set X},
      IsClosed c → P c u → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P c v ∧ P (closure v) u),
  sizeOf { C := C, U := U, P_C_U := P_C_U, closed_C := closed_C, open_U := open_U, subset := subset, hP := hP } =
    1 + sizeOf P_C_U + sizeOf closed_C + sizeOf open_U
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- **Alias** of `IsFractionRing.mulSemiringAction`. -/
FractionRing.mulSemiringAction_of_isGaloisGroup : (G : Type u_10) →
  (B : Type u_12) →
    (L : Type u_14) →
      [inst : Group G] →
        [inst_1 : CommRing B] →
          [MulSemiringAction G B] →
            [inst_3 : Field L] → [inst_4 : Algebra B L] → [IsFractionRing B L] → MulSemiringAction G L
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_mem_of_mem : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : DecidableEq M] {I : Ideal (MvPolynomial σ R)},
  Ideal.IsHomogeneous (MvPolynomial.weightedHomogeneousSubmodule R w) I →
    ∀ {p : MvPolynomial σ R}, p ∈ I → ∀ (m : M), (MvPolynomial.weightedHomogeneousComponent w m) p ∈ I
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofNatClamp_of_le : ∀ {n : ℕ}, UInt8.size ≤ n → (UInt8.ofNatClamp n).toBitVec = (UInt8.size - 1)#'UInt8.toBitVec_ofNatClamp_of_le._proof_1
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isConstructorTransition : Lean.Meta.Match.Problem → StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Bool
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply : ∀ {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α)
  (q : ↥H ⧸ (⨅ i, f i).addSubgroupOf H) (i : ι),
  (AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H) q i = AddSubgroup.quotientAddSubgroupOfMapOfLE H ⋯ q
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {Z : CategoryTheory.Functor C C}
  (h_1 : CategoryTheory.Functor.id C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.natTransTruncLTOfLE a b h)
      (CategoryTheory.CategoryStruct.comp (t.truncLTι b) h_1) =
    CategoryTheory.CategoryStruct.comp (t.truncLTι a) h_1
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C],
  CategoryTheory.IsSeparator G →
    (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G).rlp =
      (CategoryTheory.MorphismProperty.monomorphisms C).rlp
-- Init.Data.UInt.Lemmas
UInt64.toNat_lt_size : ∀ (a : UInt64), a.toNat < UInt64.size
-- Mathlib.NumberTheory.Divisors
Nat.Prime.properDivisors : ∀ {p : ℕ}, Nat.Prime p → p.properDivisors = {1}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.toList_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a},
  (Std.ExtDTreeMap.map f t).toList = List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- We say that a collection of sets is countably spanning if a countable subset spans the
whole type. This is a useful condition in various parts of measure theory. For example, it is
a needed condition to show that the product of two collections generate the product sigma algebra,
see `generateFrom_prod_eq`.  -/
IsCountablySpanning : {α : Type u_1} → Set (Set α) → Prop
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.match_1.eq_2 : ∀ (motive : Lean.Name → Lean.Name → Sort u_1) (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String)
  (h_1 : Unit → motive Lean.Name.anonymous Lean.Name.anonymous)
  (h_2 : (p₁ : Lean.Name) → (s₁ : String) → (p₂ : Lean.Name) → (s₂ : String) → motive (p₁.str s₁) (p₂.str s₂))
  (h_3 : (p₁ : Lean.Name) → (n₁ : ℕ) → (p₂ : Lean.Name) → (n₂ : ℕ) → motive (p₁.num n₁) (p₂.num n₂))
  (h_4 : (x x_1 : Lean.Name) → motive x x_1),
  (match p₁.str s₁, p₂.str s₂ with
    | Lean.Name.anonymous, Lean.Name.anonymous => h_1 ()
    | p₁.str s₁, p₂.str s₂ => h_2 p₁ s₁ p₂ s₂
    | p₁.num n₁, p₂.num n₂ => h_3 p₁ n₁ p₂ n₂
    | x, x_1 => h_4 x x_1) =
    h_2 p₁ s₁ p₂ s₂
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.Ordering.swap.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Mathlib.Topology.Path
Path.ext_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {γ₁ γ₂ : Path x y}, γ₁ = γ₂ ↔ ⇑γ₁ = ⇑γ₂
-- Mathlib.Order.Bounds.Basic
isGreatest_top_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : OrderTop α], IsGreatest s ⊤ ↔ ⊤ ∈ s
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.ext : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {φ ψ : ρ.Equiv σ}, ⇑φ = ⇑ψ → φ = ψ
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.add` -/
AnalyticAt.fun_add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → AnalyticAt 𝕜 (fun i => f i + g i) x
-- Mathlib.RingTheory.Unramified.Basic
Algebra.Unramified.formallyUnramified : ∀ {R : Type u_1} {inst : CommRing R} {A : Type u_2} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.Unramified R A], Algebra.FormallyUnramified R A
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.one_le_iff_ne_zero : ∀ {c : Cardinal.{u_1}}, 1 ≤ c ↔ c ≠ 0
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- `s.IsDiameter p₁ p₂` says that `p₁` and `p₂` are the two endpoints of a diameter of `s`.  -/
EuclideanGeometry.Sphere.IsDiameter : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [NormedSpace ℝ V] → [inst_2 : MetricSpace P] → [NormedAddTorsor V P] → EuclideanGeometry.Sphere P → P → P → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `b₄` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.b₄ : {R : Type u} → [CommRing R] → WeierstrassCurve R → R
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp.eq_1 : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R),
  x.cardSupp = Cardinal.mk ↑x.support
-- Lean.Expr
/-- Remove metadata annotations and `outParam`, `optParam`, and `autoParam` applications/annotations from `e`.
Note that it does not remove nested annotations.
Examples:
- Given `e` of the form `outParam (optParam Nat b)`, `cleanupAnnotations e = b`.
- Given `e` of the form `Nat → outParam (optParam Nat b)`, `cleanupAnnotations e = e`.
 -/
Lean.Expr.cleanupAnnotations : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- The converse is true if `J` is filtered, see `finallySmall_of_small_weakly_terminal_set`.  -/
CategoryTheory.FinallySmall.exists_small_weakly_terminal_set : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J],
  ∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)