mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.PiSystem
/-- Every element of the π-system generated by an indexed union of a family of π-systems
is a finite intersection of elements from the π-systems.
For a total union version, see `mem_generatePiSystem_iUnion_elim`.  -/
mem_generatePiSystem_iUnion_elim' : ∀ {α : Type u_3} {β : Type u_4} {g : β → Set (Set α)} {s : Set β},
  (∀ b ∈ s, IsPiSystem (g b)) →
    ∀ t ∈ generatePiSystem (⋃ b ∈ s, g b), ∃ T f, ↑T ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries.card_image_eq_of_le_nilpotencyClass`. -/
upperCentralSeries.card_image_eq_of_le_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] {a : ℕ},
  a ≤ Group.nilpotencyClass G → (Subgroup.upperCentralSeries G '' Set.Iic a).ncard = a + 1
-- Mathlib.Logic.Function.Basic
Function.injective_of_isPartialInv_right : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α},
  Function.IsPartialInv f g → ∀ (x y : β), ∀ b ∈ g x, b ∈ g y → x = y
-- Mathlib.RingTheory.Ideal.Operations
Ideal.one_eq_top : ∀ {R : Type u} [inst : Semiring R], 1 = ⊤
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.instEssSurjCompObjPostOfFull : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : C) [G.Full], (CategoryTheory.CostructuredArrow.post F G S).EssSurj
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coeFn_mk : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] (s : (x : M) → V x)
  (hs : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, s x⟩), ⇑{ toFun := s, contMDiff_toFun := hs } = s
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
/-- The AGM is also the supremum of the geometric means.  -/
NNReal.agm_eq_ciSup : ∀ {x y : NNReal}, x.agm y = ⨆ n, (x.agmSequences y n).1
-- Init.Data.Fin.Iterate
Fin.hIterateFrom.congr_simp : ∀ (P : ℕ → Sort u_1) {n : ℕ} (f f_1 : (i : Fin n) → P ↑i → P (↑i + 1)),
  f = f_1 →
    ∀ (i : ℕ) (ubnd : i ≤ n) (a a_1 : P i), a = a_1 → Fin.hIterateFrom P f i ubnd a = Fin.hIterateFrom P f_1 i ubnd a_1
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.instContinuousMapClass : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  ContinuousMapClass (A →A[R] B) A B
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul_single_eq_coeff_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ : M} [inst_1 : Mul M]
  (m₂ : M), (∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂) → (x * MonoidAlgebra.single m r).coeff m₁ = x.coeff m₂ * r
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} [inst_4 : Inhabited β] {f : Option β → Option β},
  m.WF → Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.alter m k f) k = (f (Std.DHashMap.Raw.Const.get? m k)).get!
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : Set α → Prop} {U : Set α},
  μ.InnerRegularWRT p q → q U → μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- `AffineSubspace.subtype` as an `AffineIsometry`.  -/
AffineSubspace.subtypeₐᵢ : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : PseudoMetricSpace P] →
              [inst_4 : NormedAddTorsor V P] → (s : AffineSubspace 𝕜 P) → [inst_5 : Nonempty ↥s] → ↥s →ᵃⁱ[𝕜] P
-- Mathlib.Algebra.Order.ToIntervalMod
/-- `toIocMod` as an equiv from the quotient.  -/
QuotientAddGroup.equivIocMod : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] →
      [IsOrderedAddMonoid α] →
        [hα : Archimedean α] → {p : α} → 0 < p → (a : α) → α ⧸ AddSubgroup.zmultiples p ≃ ↑(Set.Ioc a (a + p))
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq'.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.AC.Expr → Sort u_1) (e : Lean.Grind.AC.Expr)
  (h_1 : (x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Expr.var x))
  (h_2 : (a b : Lean.Grind.AC.Expr) → motive (a.op b)) (x : Lean.Grind.AC.Var),
  e = Lean.Grind.AC.Expr.var x →
    (match e with
      | Lean.Grind.AC.Expr.var x => h_1 x
      | a.op b => h_2 a b) ≍
      h_1 x
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.Array.getElem?_zipWith.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a : α) (b : β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_1 : Option β) → motive x x_1),
  (match some a, some b with
    | some a, some b => h_1 a b
    | x, x_1 => h_2 x x_1) =
    h_1 a b
-- Mathlib.Order.DirSupClosed
DirSupClosed.of_isEmpty : ∀ {α : Type u_1} [inst : Preorder α] [IsEmpty α] {s : Set α}, DirSupClosed s
-- Mathlib.Topology.Constructions
Prod.indiscreteTopology : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [h : IndiscreteTopology X]
  [hY : IndiscreteTopology Y], IndiscreteTopology (X × Y)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.mk.injEq : ∀ {R : Type u_1} [inst : CommRing R] (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime) (ne_bot : asIdeal ≠ ⊥)
  (asIdeal_1 : Ideal R) (isPrime_1 : asIdeal_1.IsPrime) (ne_bot_1 : asIdeal_1 ≠ ⊥),
  ({ asIdeal := asIdeal, isPrime := isPrime, ne_bot := ne_bot } =
      { asIdeal := asIdeal_1, isPrime := isPrime_1, ne_bot := ne_bot_1 }) =
    (asIdeal = asIdeal_1)
-- Init.System.IO
/-- Reads the entire contents of the binary file at the given path as an array of bytes.
 -/
IO.FS.readBinFile : System.FilePath → IO ByteArray
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.hasPullbacks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenPullbacks C],
  CategoryTheory.Limits.HasPullbacks C
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_a : ∀ (u : PNat.XgcdType), u.flip.a = u.b
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The linear map version of `ContinuousLinearMap.mem_invtSubmodule_adjoint_iff`
in a finite-dimensional space.  -/
Module.End.mem_invtSubmodule_adjoint_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {U : Submodule 𝕜 E},
  U ∈ Module.End.invtSubmodule (LinearMap.adjoint T) ↔ Uᗮ ∈ Module.End.invtSubmodule T
-- Mathlib.Util.Notation3
/-- Matches pi types. The name `n` should be unique, and `matchBody` should use `n`
as the `userName` of its fvar.  -/
Mathlib.Notation3.matchForall : Mathlib.Notation3.Matcher → (Lean.Expr → Mathlib.Notation3.Matcher) → Mathlib.Notation3.Matcher
-- Lean.Meta.Tactic.Grind.Types
/-- Active theorems that we have performed ematching at least once.  -/
Lean.Meta.Grind.EMatch.State.thms : Lean.Meta.Grind.EMatch.State → Lean.PArray Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Geometry.Manifold.Instances.Icc
mfderivWithin_projIcc_one : ∀ {x y : ℝ} [h : Fact (x < y)] {z : ℝ}, z ∈ Set.Icc x y → (mfderiv[Set.Icc x y] (Set.projIcc x y ⋯) z) 1 = 1
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dShortComplex_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_7),
  (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).f = X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Homology.Homotopy
/-- Equal chain maps are homotopic.  -/
Homotopy.ofEq : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → {f g : C ⟶ D} → f = g → Homotopy f g
-- Init.Grind.ToInt
Lean.Grind.IntInterval.ci.inj : ∀ {lo lo_1 : ℤ}, Lean.Grind.IntInterval.ci lo = Lean.Grind.IntInterval.ci lo_1 → lo = lo_1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier.eq_1 : ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier =
  {
    forget₂ :=
      { obj := fun P => AddGrpCat.of ↑P.toProfinite.toTop,
        map := fun {X Y} f => AddGrpCat.ofHom (ProfiniteAddGrp.Hom.hom f).toAddMonoidHom,
        map_id :=
          ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier._proof_1,
        map_comp :=
          @ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier._proof_2 },
    forget_comp :=
      ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier._proof_4 }
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Range.mk.inj : ∀ {start «end» start_1 end_1 : Lean.Lsp.Position},
  { start := start, «end» := «end» } = { start := start_1, «end» := end_1 } → start = start_1 ∧ «end» = end_1
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.left_distrib : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y z : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (x.mul (y.add z)) ((x.mul y).add (x.mul z))
-- Mathlib.RingTheory.Ideal.Height
PrimeSpectrum.height_eq_orderHeight : ∀ {R : Type u_1} [inst : CommRing R] (p : PrimeSpectrum R), p.asIdeal.height = Order.height p
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instPow : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → {G : Type u_6} → [Pow G M] → Pow (l.Germ G) M
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.instUniqueHom : (V : Type u_2) →
  [inst : CategoryTheory.ReflQuiver V] →
    [Unique V] → [(x y : V) → Unique (x ⟶ y)] → (x y : CategoryTheory.Cat.FreeRefl V) → Unique (x ⟶ y)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.id_insert : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  {x : V}, LinearIndepOn K id s → x ∉ Submodule.span K s → LinearIndepOn K id (insert x s)
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.support_of : ∀ {X : Type u_1} (x : X), (FreeAbelianGroup.of x).support = {x}
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.independent : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (self : Affine.Simplex k P n), AffineIndependent k self.points
-- Mathlib.Topology.Separation.Regular
T25Space.t2Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T25Space X], T2Space X
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.symm : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β}, m₁.Equiv m₂ → m₂.Equiv m₁
-- Std.Http.Data.URI.Basic
/-- Joins two paths. If the second path is absolute, it is returned as-is. Otherwise, the second path's
segments are appended to the first path.
 -/
Std.Http.URI.Path.join : Std.Http.URI.Path → Std.Http.URI.Path → Std.Http.URI.Path
-- Init.Data.UInt.Bitwise
Bool.toBitVec_toUInt8 : ∀ {b : Bool}, b.toUInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_add_right₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Add β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) → ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.IndepFun (f i) (f j + f k) μ
-- Mathlib.MeasureTheory.Measure.Restrict
map_comap_subtype_coe : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {s : Set α},
  MeasurableSet s →
    ∀ (μ : MeasureTheory.Measure α),
      MeasureTheory.Measure.map Subtype.val (MeasureTheory.Measure.comap Subtype.val μ) = μ.restrict s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
IsCompact.measurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [T2Space α], IsCompact s → MeasurableSet s
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.FibrantObject.mk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.FibrantObject C),
  ∃ Y, ∃ (x : HomotopicalAlgebra.IsFibrant Y), X = HomotopicalAlgebra.FibrantObject.mk Y
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.qr₁_mod : ∀ (a b ab : ℕ) (r : ℤ),
  a % 4 = 1 →
    b % 2 = 1 → b % a = ab → Mathlib.Meta.NormNum.jacobiSymNat ab a = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE.eq_1 : ∀ {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 : C) (a b : ℤ) (h : a ≤ b),
  CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE✝ t A a b h =
    { hom₁ := ⋯.choose.hom₁,
      hom₂ := CategoryTheory.CategoryStruct.id (CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t a A).obj₂,
      hom₃ := ⋯.choose.hom₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_of_contains_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.insert k).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Init.Ext
Thunk.ext_iff : ∀ {α : Type u_1} {a b : Thunk α}, a = b ↔ a.get = b.get
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.eq_0_of_lt : ∀ (x : ℕ), x < 2 ^ 0 ↔ x = 0
-- Mathlib.Algebra.Group.Equiv.Finite
Fintype.decidableEqMulEquivFintype.eq_1 : ∀ {α : Type u_4} {β : Type u_5} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Mul α] [inst_3 : Mul β]
  (a b : α ≃* β), Fintype.decidableEqMulEquivFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t[k]? = some v ↔ ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ t.toList
-- Mathlib.Algebra.Ring.GeomSum
/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs.  -/
Commute.geom_sum₂_mul_add : ∀ {R : Type u_1} [inst : Semiring R] {x y : R},
  Commute x y → ∀ (n : ℕ), (∑ i ∈ Finset.range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.invEquivalence_unitIso : ∀ (C : Type u) [inst : CategoryTheory.Groupoid C],
  (CategoryTheory.Groupoid.invEquivalence C).unitIso =
    CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).obj x)) ⋯
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : LeftCancelSemigroup α],
  MulOpposite.instRightCancelSemigroup = { toSemigroup := MulOpposite.instSemigroup, toIsRightCancelMul := ⋯ }
-- Mathlib.Data.List.Forall2
List.forall₂_cons_left_iff : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {l : List α} {u : List β},
  List.Forall₂ R (a :: l) u ↔ ∃ b u', R a b ∧ List.Forall₂ R l u' ∧ u = b :: u'
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_monomial : ∀ {R : Type u} [inst : CommSemiring R] (p q : ℕ) (r : R),
  (Polynomial.expand R p) ((Polynomial.monomial q) r) = (Polynomial.monomial (q * p)) r
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntryD.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3)
  (fallback : α × β) (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (fallback : α × β) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_1 fallback
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instDeterministicComul : ∀ {X : SFinKer}, CategoryTheory.Deterministic CategoryTheory.ComonObj.comul
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_finset_sdiff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s t : Finset β}
  {a : α}, a • (s \ t) = a • s \ a • t
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_mapWithPostcondition : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {o : Type u₁ → Type u_2} {β₂ γ : Type u₁} {m : Type u₁ → Type u_3}
  {β : Type u₁} {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n]
  [inst_4 : Monad o] [LawfulMonad o] [inst_6 : Std.Do.WPMonad o ps] [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_9 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_11 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_13 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        g __do_lift acc ⦃Q⦄ →
    ⦃P⦄ forIn (Std.IterM.mapWithPostcondition f it) init g ⦃Q⦄
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_mono_of_hom : ∀ {V : Type u} {G : SimpleGraph V} {V' : Type u_4} {G' : SimpleGraph V'} (f : G →g G'),
  G.chromaticNumber ≤ G'.chromaticNumber
-- Mathlib.Analysis.Real.Sqrt
/-- **Alias** of the reverse direction of `NNReal.sqrt_pos`. -/
NNReal.sqrt_pos_of_pos : ∀ {x : NNReal}, 0 < x → 0 < NNReal.sqrt x
-- Mathlib.Data.FP.Basic
FP.ofRatUp : [C : FP.FloatCfg] → ℚ → FP.Float
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective : ∀ {R : Type u_1} [inst : CommSemiring R],
  DiscreteTopology (PrimeSpectrum R) ↔ Function.Bijective ⇑(PrimeSpectrum.toPiLocalization R)
-- Lean.Compiler.IR.Basic
Lean.IR.modifyJPsM : {m : Type → Type} → [Monad m] → Array Lean.IR.FnBody → (Lean.IR.FnBody → m Lean.IR.FnBody) → m (Array Lean.IR.FnBody)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsMultiplicativeDiagonalOfIsStableUnderBaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {P : CategoryTheory.MorphismProperty C} [P.IsMultiplicative] [P.IsStableUnderBaseChange], P.diagonal.IsMultiplicative
-- Mathlib.GroupTheory.FiniteAbelian.Duality
/-- **Alias** of `CommGroup.card_domRestrictHom_ker`. -/
CommGroup.card_restrictHom_ker : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G),
  Nat.card ↥(MonoidHom.domRestrictHom H Mˣ).ker = Nat.card (G ⧸ H)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_sum_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_4} (f : α → ENNReal) (μ : ι → MeasureTheory.Measure α),
  ∫⁻ (a : α), f a ∂MeasureTheory.Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
/-- If `M` satisfies `HasEnoughRootsOfUnity`, then the group of `n`th roots of unity
in `M` (is cyclic and) has order `n`.  -/
HasEnoughRootsOfUnity.natCard_rootsOfUnity : ∀ (M : Type u_1) [inst : CommMonoid M] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity M n], Nat.card ↥(rootsOfUnity n M) = n
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- An object from `C`  -/
CategoryTheory.RegularEpi.W : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.RegularEpi f → C
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.pre_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)),
  ((CategoryTheory.StructuredArrow.pre S F G).obj X).left = X.left
-- Mathlib.Analysis.Complex.Order
Complex.re_eq_neg_norm : ∀ {z : ℂ}, z.re = -‖z‖ ↔ z ≤ 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.instInhabitedWalkingPair.default : CategoryTheory.Limits.WalkingPair
-- Std.Http.Data.Headers.Basic
/-- Serializes a content length header back to a name-value pair.
 -/
Std.Http.Header.ContentLength.serialize : Std.Http.Header.ContentLength → Std.Http.Header.Name × Std.Http.Header.Value
-- Mathlib.Data.Stream.Init
Stream'.tail_interleave : ∀ {α : Type u} (s₁ s₂ : Stream' α), (s₁ ⋈ s₂).tail = s₂ ⋈ s₁.tail