mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.HahnBanach
/-- Corollary of the polynormable **Hahn-Banach theorem**: if `f : S → F` is a continuous
linear map with finite-dimensional range, then `f` extends to a continuous linear map on the whole
space.  -/
ContinuousLinearMap.exist_extension_of_finiteDimensional_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : NormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜 E] [PolynormableSpace 𝕜 E] {F : Type u_3} [inst_6 : AddCommGroup F]
  [inst_7 : TopologicalSpace F] [IsTopologicalAddGroup F] [inst_9 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F]
  {S : Submodule 𝕜 E} (f : ↥S →L[𝕜] F) [FiniteDimensional 𝕜 ↥(↑f).range], ∃ g, f = g ∘SL S.subtypeL
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X Y : C}
  (f : X ⟶ Y) (A B : CategoryTheory.Over Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Over.pullback f) A B).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom B.hom) A.hom) f)
        (CategoryTheory.Limits.pullback.fst A.hom B.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd A.hom f)
        (CategoryTheory.Limits.pullback.snd B.hom f))
      (CategoryTheory.Limits.pullback.fst A.hom f)
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.ext : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {k : ℕ}
  {N₁ N₂ : Module.Grassmannian R M k}, N₁.toSubmodule = N₂.toSubmodule → N₁ = N₂
-- Mathlib.Data.PNat.Equiv
/-- An equivalence between `ℕ+` and `ℕ` given by `PNat.natPred` and `Nat.succPNat`.  -/
Equiv.pnatEquivNat : ℕ+ ≃ ℕ
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.ext : ∀ {n : ℕ} {x y : CompositionAsSet n}, x.boundaries = y.boundaries → x = y
-- Init.Data.List.Lemmas
/-- Membership is preserved by `eraseDups`: an element is in the deduplicated list
iff it was in the original list.  -/
List.mem_eraseDups : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∈ l.eraseDups ↔ a ∈ l
-- Mathlib.CategoryTheory.Sites.Plus
/-- The diagram whose colimit defines the values of `plus`.  -/
CategoryTheory.GrothendieckTopology.diagram : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            CategoryTheory.Functor Cᵒᵖ D → (X : C) → CategoryTheory.Functor (J.Cover X)ᵒᵖ D
-- Mathlib.GroupTheory.Perm.Basic
Equiv.swap_smul_self_smul : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : MulAction (Equiv.Perm α) β] (i j : α) (x : β),
  Equiv.swap i j • Equiv.swap i j • x = x
-- Mathlib.RingTheory.Regular.Flat
/-- Let `R` be a commutative ring, `M` be an `R`-module, `S` be a faithfully flat `R`-algebra,
`N` be the base change of `M` to `S`. If `[r₁, …, rₙ]` is a regular `M`-sequence, then its image
in `N` is a regular `N`-sequence.  -/
RingTheory.Sequence.IsRegular.of_faithfullyFlat_of_isBaseChange : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] [Module.FaithfullyFlat R S] {f : M →ₗ[R] N},
  IsBaseChange S f →
    ∀ {rs : List R},
      RingTheory.Sequence.IsRegular M rs → RingTheory.Sequence.IsRegular N (List.map (⇑(algebraMap R S)) rs)
-- Mathlib.Data.Num.ZNum
PosNum.divMod_to_nat : ∀ (d n : PosNum), ↑n / ↑d = ↑(d.divMod n).1 ∧ ↑n % ↑d = ↑(d.divMod n).2
-- Std.Data.HashMap.Lemmas
Std.HashMap.keys_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {f : α → β → γ},
  (Std.HashMap.map f m).keys.Perm m.keys
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.instOneInfty : ENNReal.HolderConjugate 1 ⊤
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.instIsTruncLEOpOfIsTruncGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE],
  e.op.IsTruncLE
-- Aesop.Forward.State
/-- Extract stats from a `VariableMap`.  -/
Aesop.VariableMap.stats : Aesop.VariableMap → Array Aesop.ForwardInstantiationStats
-- Mathlib.NumberTheory.Height.Projectivization
_private.Mathlib.NumberTheory.Height.Projectivization.0.Projectivization.mulHeight_aux : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι]
  (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → Height.mulHeight ↑a = Height.mulHeight ↑b
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- The non-units of the stalk at `x` of the sheaf of smooth functions from `M` to `𝕜`, considered
as a sheaf of commutative rings, are the functions whose values at `x` are zero.  -/
smoothSheafCommRing.nonunits_stalk : ∀ {𝕜 : 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] (x : M),
  nonunits ↑((smoothSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜).presheaf.stalk x) =
    ↑(RingHom.ker (smoothSheafCommRing.eval IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x))
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal.eq_1 : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] [inst_1 : DecidableEq δ]
  (μ : (i : δ) → MeasureTheory.Measure (X i)) (s : Finset δ) (f : ((i : δ) → X i) → ENNReal) (x : (i : δ) → X i),
  (∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (y : (i : ↥s) → X ↑i), f (Function.updateFinset x s y) ∂MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.cotangentEquivIdeal_apply : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (x : I.Cotangent),
  ↑(I.cotangentEquivIdeal x) = I.cotangentToQuotientSquare x
-- Aesop.Nanos
Aesop.Nanos.instOfNat : {n : ℕ} → OfNat Aesop.Nanos n
-- Lean.Parser.Term
Lean.Parser.Term.show.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Finite product of seminormed groups, using the sup norm.  -/
Pi.seminormedAddCommGroup : {ι : Type u_1} →
  {G : ι → Type u_4} → [Fintype ι] → [(i : ι) → SeminormedAddCommGroup (G i)] → SeminormedAddCommGroup ((i : ι) → G i)
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Clause.reify.prop : ∀ {v : Sat.Valuation} {c : Sat.Clause} {p : Prop}, Sat.Clause.reify v c p → ¬v.satisfies c → p
-- Mathlib.FieldTheory.Perfect
frobenius_apply_frobeniusEquiv_symm : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (frobenius R p) ((frobeniusEquiv R p).symm x) = x
-- Mathlib.Analysis.Calculus.Gradient.Basic
DifferentiableAt.hasGradientAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F}, DifferentiableAt 𝕜 f x → HasGradientAt f (gradient f x) x
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instIsCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsCancelAdd α], IsCancelAdd αᵃᵒᵖ
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedCommandInfo : Inhabited Lean.Elab.CommandInfo
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁.union m₂},
  Std.ExtDHashMap.Const.get (m₁.union m₂) k h' = Std.ExtDHashMap.Const.get m₂ k ⋯
-- Mathlib.Data.Bool.Count
List.IsChain.two_mul_count_bool_eq_ite : ∀ {l : List Bool},
  List.IsChain (fun x1 x2 => x1 ≠ x2) l →
    ∀ (b : Bool),
      2 * List.count b l =
        if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integrable_cexp_neg_sum_mul_add : ∀ {ι : Type u_2} [inst : Fintype ι] {b : ι → ℂ},
  (∀ (i : ι), 0 < (b i).re) →
    ∀ (c : ι → ℂ),
      MeasureTheory.Integrable (fun v => Complex.exp (-∑ i, b i * ↑(v i) ^ 2 + ∑ i, c i * ↑(v i))) MeasureTheory.volume
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Conjugation in `ℤ√d`. The conjugate of `a + b √d` is `a - b √d`.  -/
Zsqrtd.instStar : {d : ℤ} → Star (ℤ√d)
-- Mathlib.RingTheory.Congruence.Hom
/-- Given ring congruence relations `c, d` on an algebra such that `d`
contains `c`, `d`'s quotient map induces an algebra homomorphism from
the quotient by `c` to the quotient by `d`.  -/
RingCon.factorₐ : {M : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring M] → [inst_2 : Algebra R M] → {c d : RingCon M} → c ≤ d → c.Quotient →ₐ[R] d.Quotient
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_add : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (x y : ↥s), ↑(x + y) = ↑x + ↑y
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_3.splitter : {α₂ β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α₂ m β] →
      (it₂ : Std.IterM m β) →
        (motive : it₂.Step → Sort u_3) →
          (x : it₂.Step) →
            ((it₂' : Std.IterM m β) →
                (out : β) →
                  (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩) →
              ((it₂' : Std.IterM m β) →
                  (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩) →
                ((h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.eq_3 : ∀ (motive : Nat.Partrec.Code → Sort u_1) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match Nat.Partrec.Code.left with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_3 ()
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_index_single_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (s t : σ),
  (MvPowerSeries.coeff fun₀ | t => 1) (MvPowerSeries.X s) = if t = s then 1 else 0
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_def : ∀ {R : Type u_5} [inst : CommRing R] (S : Submonoid R) {P : Type u_6} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x : P), FractionalIdeal.spanSingleton S x = ⟨R ∙ x, ⋯⟩
-- Std.Time.Format.Modifier
/-- `DayPeriod` extends `HourMarker` with exact noon and midnight values, used by the `b` pattern.
 -/
Std.Time.DayPeriod : Type
-- Lean.Compiler.IR.Basic
Lean.IR.mkDummyExternDecl : Lean.IR.FunId → Array Lean.IR.Param → Lean.IR.IRType → Lean.IR.Decl
-- Init.SimpLemmas
implies_congr_left : ∀ {p₁ p₂ : Sort u} {q : Sort v}, p₁ = p₂ → (p₁ → q) = (p₂ → q)
-- Mathlib.Order.Interval.Finset.Defs
Set.toFinset_Iio : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α) [inst_2 : Fintype ↑(Set.Iio a)],
  (Set.Iio a).toFinset = Finset.Iio a
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` and `β` are arbitrary types and there is an injection between them,
then the induced map on their additive free groups is also injective.  -/
FreeAddGroup.map_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective f → Function.Injective ⇑(FreeAddGroup.map f)
-- Init.Data.ByteArray.Lemmas
ByteArray.append_left_inj : ∀ {xs₁ xs₂ : ByteArray} (ys : ByteArray), xs₁ ++ ys = xs₂ ++ ys ↔ xs₁ = xs₂
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The injection into the free product of any `1 : A i` is the 1 of the free product.  -/
LinearAlgebra.FreeProduct.identify_one : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] (i : I),
  (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) 1) = 1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective.  -/
AddSubsemigroup.gciMapComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] →
      [inst_1 : Add N] →
        {f : M →ₙ+ N} → Function.Injective ⇑f → GaloisCoinsertion (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxcHasSize_eq : Int32.instRxcHasSize = HasModel.instRxcHasSize✝
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_map_eq_of_injective : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂},
  Function.Injective ⇑f → ∀ (s : AffineSubspace k P₁), AffineSubspace.comap f (AffineSubspace.map f s) = s
-- Init.Data.SInt.Lemmas
Int16.zero_add : ∀ (a : Int16), 0 + a = a
-- Mathlib.Algebra.Notation.Defs
SDiv.ext_iff : ∀ {G : outParam (Type u_1)} {P : Type u_2} {x y : SDiv G P}, x = y ↔ SDiv.sdiv = SDiv.sdiv
-- Mathlib.RingTheory.Ideal.Maps
Ideal.le_comap_mul : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F) {K L : Ideal S}, Ideal.comap f K * Ideal.comap f L ≤ Ideal.comap f (K * L)
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.mk : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}, m.inner.WF → m.WF
-- Mathlib.RingTheory.Ideal.HasGoingUp
/-- An `R`-algebra `S` satisfies `Algebra.HasGoingUp R S` if for every pair of
prime ideals `p ≤ q` of `R` with `P` a prime of `S` lying above `p`, there exists a
prime `P ≤ Q` of `S` lying above `q`.

The condition only asks for `<` which is easier to prove, use
`Ideal.exists_ideal_ge_liesOver_of_le` for applying it.  -/
Algebra.HasGoingUp : (R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Mathlib.NumberTheory.NumberField.House
NumberField.house_prod_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (s : Finset K),
  NumberField.house (∏ x ∈ s, x) ≤ ∏ x ∈ s, NumberField.house x
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadLift_ReaderT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α ρ : Type u}
  {post : α → ρ → Pred} {epost : EPred} (x : m α),
  Std.Internal.Do.wp (MonadLift.monadLift x) post epost = fun r => Std.Internal.Do.wp x (fun a => post a r) epost
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- `affineSpan` is monotone.  -/
affineSpan_mono : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : Set P}, s₁ ⊆ s₂ → affineSpan k s₁ ≤ affineSpan k s₂
-- Mathlib.FieldTheory.Separable
AlgEquiv.Algebra.isSeparable_iff : ∀ {F : Type u_1} {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] {E : Type u_4}
  [inst_3 : Ring E] [inst_4 : Algebra F E] (e : K ≃ₐ[F] E), Algebra.IsSeparable F K ↔ Algebra.IsSeparable F E
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_nonneg_of_nonneg_of_le_pi : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi → 0 ≤ Real.sin x
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.toCocone_pt_coe : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] {A : Type w} [inst_2 : AddCommGroup A] (f : AddCommGrpCat.Colimits.Quot F →+ A),
  ↑(AddCommGrpCat.Colimits.toCocone F f).pt = A
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union_add_inter₀ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet t μ →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_union_add_inter₀._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_union_add_inter₀._auto_3 →
        μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
-- Init.Data.List.Lemmas
List.forall_mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {P : β → Prop}, (∀ i ∈ List.map f l, P i) ↔ ∀ j ∈ l, P (f j)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The pushout of `f` and `g` in `C` is isomorphic to the pullback of
`f.op` and `g.op` in `Cᵒᵖ`.  -/
CategoryTheory.Limits.pushoutIsoUnopPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : X ⟶ Y) →
          [h : CategoryTheory.Limits.HasPushout f g] →
            CategoryTheory.Limits.pushout f g ≅ Opposite.unop (CategoryTheory.Limits.pullback f.op g.op)
-- Mathlib.Algebra.Group.Commute.Defs
Commute.symm_iff : ∀ {S : Type u_3} [inst : Mul S] {a b : S}, Commute a b ↔ Commute b a
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_eq_get!_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {a : α}, m.get! a = (m.get? a).get!
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.μ_pullback_left_fst_snd' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk g₁)
          (CategoryTheory.Over.mk g₂)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g₁ g₂) g₁) f)
        (CategoryTheory.Limits.pullback.snd g₁ g₂)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₁)).hom
        ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₂)).hom)
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Over.mk g₂).hom f)
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfShape CategoryTheory.Limits.WalkingSpan F],
  F.ReflectsEpimorphisms
-- Std.Sync.Channel
/-- Closes the channel, returns `Except.ok` when called the first time, otherwise `Except.error`.
When a channel is closed:
- no new values can be sent successfully anymore
- all blocked consumers are resolved to `none` (as no new messages can be sent they will never
  resolve)
- if there are already values waiting to be received they can still be received by subsequent `recv`
  calls
 -/
Std.CloseableChannel.Sync.close : {α : Type} → Std.CloseableChannel.Sync α → EIO Std.CloseableChannel.Error Unit
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNClique_bot_iff : ∀ {α : Type u_1} {n : ℕ} {s : Finset α}, ⊥.IsNClique n s ↔ n ≤ 1 ∧ s.card = n
-- Mathlib.Data.Stream.Init
Stream'.tail_cons : ∀ {α : Type u} (a : α) (s : Stream' α), (Stream'.cons a s).tail = s
-- Init.Data.List.ToArray
List.toArray_cons : ∀ {α : Type u_1} (a : α) (l : List α), (a :: l).toArray = #[a] ++ l.toArray
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.brecOn_1.go : {α : Type u} →
  {motive_1 : Lean.PersistentArrayNode α → Sort u_1} →
    {motive_2 : Array (Lean.PersistentArrayNode α) → Sort u_1} →
      {motive_3 : List (Lean.PersistentArrayNode α) → Sort u_1} →
        (t : Array (Lean.PersistentArrayNode α)) →
          ((t : Lean.PersistentArrayNode α) → t.below → motive_1 t) →
            ((t : Array (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_1 t → motive_2 t) →
              ((t : List (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_2 t → motive_3 t) →
                motive_2 t ×' Lean.PersistentArrayNode.below_1 t
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- Auxiliary definition for the `X` field of `HomologicalComplex.extend`.  -/
HomologicalComplex.extend.X : {ι : Type u_1} →
  {c : ComplexShape ι} →
    {C : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_3} C] →
        [CategoryTheory.Limits.HasZeroObject C] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → HomologicalComplex C c → Option ι → C
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.CommGrp C)
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.ByteSlice.forM.loop : {m : Type v → Type w} → [Monad m] → (UInt8 → m PUnit.{v + 1}) → ByteSlice → ℕ → m PUnit.{v + 1}
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
MulAction.IsBlock.subsingleton_of_stabilizer_lt_of_subset : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s B : Set α} {G : Subgroup M}
  [MulAction.IsPreprimitive ↥(MulAction.stabilizer (↥G) s) ↑s],
  MulAction.IsBlock (↥G) B →
    (∀ (B : Set α), MulAction.IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton) →
      MulAction.stabilizer M s < G → B ⊆ s → B.Subsingleton
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.instSupSetLexForall : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedLT ι] → SupSet (Lex ((i : ι) → (fun i => α i) i))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Right.inv_pos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a : G₀}, 0 < a⁻¹ ↔ 0 < a
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Functor.LocallyCoverDense.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D},
  (∀ ⦃X : C⦄ (T : ↑(K (G.obj X))),
      CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPullback G ↑T) ∈ K (G.obj X)) →
    G.LocallyCoverDense K
-- Init.Data.Array.Lemmas
Array.flatten_toArray_map_toArray : ∀ {α : Type u_1} {L : List (List α)}, (List.map List.toArray L).toArray.flatten = L.flatten.toArray