mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.toList.isEmpty = t.isEmpty
-- Mathlib.Algebra.Order.BigOperators.Expect
/-- Let `{a | p a}` be a subsemigroup of a commutative monoid `M`. If `m` is a subadditive function
(`m (x + y) ≤ m x + m y`, `m 0 = 0`) preserved under division by a natural and `f` is a function
valued in that subsemigroup, then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`.  -/
Finset.le_expect_of_subadditive_on_pred : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M]
  [inst_2 : AddCommMonoid N] [inst_3 : PartialOrder N] [IsOrderedAddMonoid N] [inst_5 : Module ℚ≥0 N]
  [PosSMulMono ℚ≥0 N] {m : M → N} {p : M → Prop} {f : ι → M} {s : Finset ι},
  m 0 = 0 →
    (∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b) →
      (∀ (a b : M), p a → p b → p (a + b)) →
        (∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a) →
          (∀ i ∈ s, p (f i)) → m (s.expect fun i => f i) ≤ s.expect fun i => m (f i)
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.coe_frobeniusAlgEquivOfAlgebraic : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Algebra.IsAlgebraic K L], ⇑(FiniteField.frobeniusAlgEquivOfAlgebraic K L) = fun x => x ^ Fintype.card K
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Φ_zero : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Φ 0 = 1
-- Mathlib.CategoryTheory.Action.Continuous
CategoryTheory.Functor.mapContActionComp_inv : ∀ {V : Type u_5} {W : Type u_6} [inst : CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7}
  {CV : V → Type u_8} [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_2 : CategoryTheory.ConcreteCategory V FV] [inst_3 : CategoryTheory.HasForget₂ V TopCat]
  [inst_4 : CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10}
  [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [inst_6 : CategoryTheory.ConcreteCategory W FW]
  [inst_7 : CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [inst_8 : Monoid G] [inst_9 : TopologicalSpace G]
  {T : Type u_12} [inst_10 : CategoryTheory.Category.{v_4, u_12} T] {FT : T → T → Type u_13} {CT : T → Type u_14}
  [inst_11 : (X Y : T) → FunLike (FT X Y) (CT X) (CT Y)] [inst_12 : CategoryTheory.ConcreteCategory T FT]
  [inst_13 : CategoryTheory.HasForget₂ T TopCat] (F : CategoryTheory.Functor V W)
  (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (F' : CategoryTheory.Functor W T)
  (H' : ∀ (X : ContAction W G), ((F'.mapAction G).obj X.obj).IsContinuous),
  (CategoryTheory.Functor.mapContActionComp G F H F' H').inv =
    { app := fun X => CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mapContAction G (F.comp F') ⋯).obj X),
      naturality := ⋯ }
-- Init.Data.Fin.Iterate
/-- Applies an index-dependent function to all the values less than the given bound `n`, starting at
`0` with an accumulator.

Concretely, `Fin.hIterate P init f` is equal to
```lean
  init |> f 0 |> f 1 |> ... |> f (n-1)
```

Theorems about `Fin.hIterate` can be proven using the general theorem `Fin.hIterate_elim` or other more
specialized theorems.

`Fin.hIterateFrom` is a variant that takes a custom starting value instead of `0`.
  -/
Fin.hIterate : (P : ℕ → Sort u_1) → {n : ℕ} → P 0 → ((i : Fin n) → P ↑i → P (↑i + 1)) → P n
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The trivial seminorm on a ring `R` is the `RingSeminorm` taking value `0` at `0` and `1` at
every other element.  -/
RingSeminorm.instOneOfDecidableEq : {R : Type u_1} → [inst : NonUnitalRing R] → [DecidableEq R] → One (RingSeminorm R)
-- Mathlib.GroupTheory.FiniteAbelian.Basic
CommGroup.finite_of_fg_isMulTorsion : ∀ (G : Type u) [inst : CommGroup G] [Group.FG G], IsMulTorsion G → Finite G
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instLinearOrderedCommGroupWithZeroMultiplicativeInt : LinearOrderedCommGroupWithZero (WithZero (Multiplicative ℤ))
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.labellingStarEquiv_apply : ∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M)
  (x : Quiver.SchreierGraph V ι) (a : Quiver.Star x),
  (Quiver.SchreierGraph.labellingStarEquiv ι x) a = (Quiver.SchreierGraph.labelling V ι).star x a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₁₀_comp_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₁ A).inv ((groupHomology.inhomogeneousChains A).d 1 0) =
    CategoryTheory.CategoryStruct.comp (groupHomology.d₁₀ A) (groupHomology.chainsIso₀ A).inv
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.ProofInstArgInfo.mk : Bool → Bool → Lean.Meta.Sym.ProofInstArgInfo
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.EAdj.exists_vertex : ∀ {α : Type u_1} {e f : Set α} {H : Hypergraph α}, H.EAdj e f → ∃ x ∈ H.vertexSet, x ∈ e ∧ x ∈ f
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.le_totalDegree : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {s : σ →₀ ℕ},
  s ∈ p.support → (s.sum fun x e => e) ≤ p.totalDegree
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds_append_right : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {i : ℕ} {x : α},
  n ≤ i → (xs ++ ys).setIfInBounds i x = xs ++ ys.setIfInBounds (i - n) x
-- Mathlib.NumberTheory.ModularForms.Basic
/-- If `-1 ∈ Γ` and `k` is odd, then every modular form of weight `k` for `Γ` is zero.  -/
ModularForm.eq_zero_of_neg_one_mem : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne], -1 ∈ Γ → Odd k → ∀ (f : ModularForm Γ k), f = 0
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.instOrderHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β], OrderHomClass (α →*o β) α β
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TacticNode.mk.inj : ∀ {ctxI : Lean.Elab.ContextInfo} {tacI : Lean.Elab.TacticInfo} {mayFail : Bool} {ctxI_1 : Lean.Elab.ContextInfo}
  {tacI_1 : Lean.Elab.TacticInfo} {mayFail_1 : Bool},
  { ctxI := ctxI, tacI := tacI, mayFail := mayFail } = { ctxI := ctxI_1, tacI := tacI_1, mayFail := mayFail_1 } →
    ctxI = ctxI_1 ∧ tacI = tacI_1 ∧ mayFail = mayFail_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_iff_exists_nonneg_add : ∀ {α : Type u} [inst : AddZeroClass α] [inst_1 : Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftMono α]
  [AddLeftReflectLE α], a ≤ b ↔ ∃ c, 0 ≤ c ∧ a + c = b
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {V W : BialgCat R} {x y : V.Hom W}, x.toBialgHom' = y.toBialgHom' → x = y
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.prod : ∀ {𝕜 : 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] {z : M} {F' : Type u_21} [inst_6 : NormedCommRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {ι : Type} {t : Finset ι} {f : ι → M → F'},
  (∀ i ∈ t, MDiffAt (f i) z) → MDiffAt (∏ i ∈ t, f i) z
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Functor.instFaithfulQuotientHomRelLift : ∀ {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] (L : CategoryTheory.Functor C D),
  (CategoryTheory.Quotient.lift L.homRel L ⋯).Faithful
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.one_lt_order : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst_1 : Configuration.ProjectivePlane P L] [Finite P]
  [Finite L], 1 < Configuration.ProjectivePlane.order P L
-- Mathlib.Data.Matrix.Mul
Matrix.diagonal_mul_diagonal' : ∀ {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (d₁ d₂ : n → α), Matrix.diagonal d₁ * Matrix.diagonal d₂ = Matrix.diagonal fun i => d₁ i * d₂ i
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.op_Y' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.RightFraction X Y), φ.op.Y' = Opposite.op φ.X'
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.isoMk_inv_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber),
  (CategoryTheory.Grothendieck.isoMk e₁ e₂).inv.base = e₁.inv
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.DTreeMap.maxEntry! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap α β cmp → (a : α) × β a
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instZeroCoeOfZeroMemClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Zero (R i)] [inst_2 : ∀ (i : ι), ZeroMemClass (S i) (R i)],
  RestrictedProduct.instZeroCoeOfZeroMemClass R = { zero := ⟨fun x => 0, ⋯⟩ }
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- The extensive coverage on an extensive category `C`

TODO: use general colimit API instead of `IsIso (Sigma.desc π)`
 -/
CategoryTheory.extensiveCoverage : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.FinitaryPreExtensive C] → CategoryTheory.Coverage C
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- If a set `s` of semilinear functions is bounded and is closed in the weak-\* topology, then its
image under coercion to functions `E → F` is a compact set. We don't have a name for `E →SL[σ] F`
with weak-\* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`).
 -/
ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂] [ProperSpace F]
  {s : Set (E' →SL[σ₁₂] F)},
  Bornology.IsBounded s →
    (∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s) → IsCompact (DFunLike.coe '' s)
-- Mathlib.GroupTheory.Schreier
MonoidHom.transferCenterPow.congr_simp : ∀ (G : Type u_1) [inst : Group G] [inst_1 : (Subgroup.center G).FiniteIndex],
  MonoidHom.transferCenterPow G = MonoidHom.transferCenterPow G
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.le_centralizer_centralizer : ∀ (M : Type u_1) [inst : Monoid M] {s : Submonoid M}, s ≤ Submonoid.centralizer ↑(Submonoid.centralizer ↑s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_diff_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_comp_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (c : 𝕜),
  iteratedDerivWithin n (fun z => f (z - c)) s = fun x => iteratedDerivWithin n f (-c +ᵥ s) (x - c)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.r1_pos : ∀ (z : UpperHalfPlane), 0 < EisensteinSeries.r1 z
-- Init.Data.UInt.Lemmas
UInt16.sub_zero : ∀ (a : UInt16), a - 0 = a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.w_prod_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D') {A B : CategoryTheory.CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (S.map f.left.1) B.hom.1 = A.hom.1
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The action by an intermediate field is the action by the underlying field.  -/
IntermediateField.instMulDistribMulActionSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {X : Type u_4} →
            [inst_3 : Monoid X] → [MulDistribMulAction L X] → (F : IntermediateField K L) → MulDistribMulAction (↥F) X
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.mem_support_self : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (c : ↥g.cycleFactorsFinset), a c ∈ (↑c).support
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.coe_incidenceFinset : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : DecidableEq V],
  ↑(G.incidenceFinset v) = G.incidenceSet v
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_le : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ}
  {ω : Ω}, MeasureTheory.upperCrossingTime a b f N n ω ≤ N
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
_private.Mathlib.RingTheory.WittVector.FrobeniusFractionField.0.WittVector.termφ : Lean.ParserDescr
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
/-- If `α` has at least 5 elements, then any nontrivial
normal subgroup of `Equiv.Perm α` contains `alternatingGroup α`.  -/
Equiv.Perm.alternatingGroup_le_of_normal : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α],
  5 ≤ Nat.card α → ∀ {N : Subgroup (Equiv.Perm α)} [N.Normal], Nontrivial ↥N → alternatingGroup α ≤ N
-- Mathlib.Algebra.Notation.Defs
/-- `a +ᵥ b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+ᵥ` in identifiers is `vadd`. -/
«term_+ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.Order.Filter.AtTopBot.Finite
Nat.eventually_pow_lt_factorial_sub : ∀ (c d : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, c ^ n < (n - d).factorial
-- Init.Data.List.Scan.Lemmas
List.scanr_cons : ∀ {α : Type u_1} {β : Type u_2} {b : β} {a : α} {l : List α} {f : α → β → β},
  List.scanr f b (a :: l) = List.foldr f b (a :: l) :: List.scanr f b l
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go.aux₂ : ∀ {α β : Type w} {m : Type w → Type w'} {it : Std.IterM m β} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Std.Iterator α m β] [Std.Iterators.Finite α m] {acc : Array β},
  Std.IterM.toArray.go it acc = (fun x => acc ++ x) <$> it.toArray
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.coe_comp : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (g : B.Copy C) (f : A.Copy B), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.RingTheory.Localization.Defs
Localization.mk_multiset_sum : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (l : Multiset R) (b : ↥M),
  Localization.mk l.sum b = (Multiset.map (fun a => Localization.mk a b) l).sum
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.whiskerLeft_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C) {Y₁ Y₂ : CategoryTheory.Center C} (f : Y₁ ⟶ Y₂) (U : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.fst f.f)
        U)
      ((X.tensorObj Y₂).snd.β U).hom =
    CategoryTheory.CategoryStruct.comp ((X.tensorObj Y₁).snd.β U).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.fst f.f))
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- In an additive group action, the points fixed by `g` are also fixed by `g⁻¹`  -/
AddAction.fixedBy_neg : ∀ (α : Type u_1) {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G),
  AddAction.fixedBy α (-g) = AddAction.fixedBy α g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.map_id_equiv : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp},
  (Std.DTreeMap.Raw.map (fun x v => v) t).Equiv t
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When both `S.f` and `S.g` are zero, the middle object `S.X₂`
gives a right homology data on S  -/
CategoryTheory.ShortComplex.RightHomologyData.ofZeros : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → S.f = 0 → S.g = 0 → S.RightHomologyData
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, m.getKeyD a fallback = (m.getKey? a).getD fallback
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_congr : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {f : α →₀ M}
  {g1 g2 : α → M → N}, (∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) → f.sum g1 = f.sum g2
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool} {k : α},
  k ∈ Std.ExtTreeSet.filter f t ↔ ∃ (h : k ∈ t), f (t.get k h) = true
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableAt.mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸},
  DifferentiableAt 𝕜 a x → ∀ (b : 𝔸), DifferentiableAt 𝕜 (fun y => a y * b) x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF →
    ∀ {k a : α} {v : β k},
      (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ m.contains k = false then k else m.getKey! a
-- Mathlib.RingTheory.Jacobson.Ring
/-- [Stacks Tag 0CY7](https://stacks.math.columbia.edu/tag/0CY7) (See also https://en.wikipedia.org/wiki/Zariski%27s_lemma.) -/
finite_of_finite_type_of_isJacobsonRing : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : Field S] [inst_2 : Algebra R S] [IsJacobsonRing R]
  [Algebra.FiniteType R S], Module.Finite R S
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃_le : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (pq : κ)
  (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃_le._auto_1)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃_le._auto_3),
  data.i₃ r pq ⋯ ≤ data.i₃ r' pq ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.all_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice}, s.copy = t.copy → s.all pat = t.all pat
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K], (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = 1
-- Mathlib.Algebra.Group.Action.Defs
/-- Let `Q / P / N / M` be a tower. If `P / N / M`, `Q / P / M` and `Q / P / N` are
scalar towers, then `Q / N / M` is also a scalar tower.
 -/
IsScalarTower.to₁₂₄ : ∀ (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [inst : SMul M N] [inst_1 : SMul M P]
  [inst_2 : SMul M Q] [inst_3 : SMul N P] [inst_4 : SMul N Q] [inst_5 : Monoid P] [inst_6 : MulAction P Q]
  [IsScalarTower M N P] [IsScalarTower M P Q] [IsScalarTower N P Q], IsScalarTower M N Q
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_rcc : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_rcc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
    List.filter (fun e => decide ((cmp e lowerBound).isGE = true ∧ (cmp e upperBound).isLE = true)) t.toList
-- Mathlib.Computability.NFA
NFA.reverse_accept : ∀ {α : Type u} {σ : Type v} (M : NFA α σ), M.reverse.accept = M.start
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_succ_of_mono : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < Order.succ o → Ordinal.{max u v}},
  (∀ {i j : Ordinal.{u}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj) →
    (Order.succ o).blsub f = Order.succ (f o ⋯)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.instProdCompleteSpace : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : UniformSpace α] [inst_1 : UniformSpace β] [CompleteSpace α]
  [CompleteSpace β], CompleteSpace (WithLp p (α × β))
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withBotCongr_symm : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), e.withBotCongr.symm = e.symm.withBotCongr
-- Mathlib.Tactic.FunProp.Types
/-- `fun_prop` context  -/
Mathlib.Meta.FunProp.Context : Type
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instSMul : {Γ : Type u_1} →
  {R : Type u_3} →
    {β : Type u_6} →
      [inst : PartialOrder Γ] →
        [inst_1 : AddCommMonoid R] → {M : Type u_7} → [SMulZeroClass M R] → SMul M (HahnSeries.SummableFamily Γ R β)
-- Mathlib.CategoryTheory.Limits.Preserves.Yoneda
CategoryTheory.instPreservesColimitFunctorOppositeTypeObjCoyonedaOpYoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  [CategoryTheory.Limits.HasColimitsOfShape J (Type v₁)] [CategoryTheory.Limits.HasColimitsOfShape J (Type (max u₁ v₁))]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor Cᵒᵖ (Type v₁))) {X : C},
  CategoryTheory.Limits.PreservesColimit F (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.yoneda.obj X)))
-- Batteries.Data.Vector.Lemmas
Vector.scanrM_empty : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m] {f : α → β → m β},
  Vector.scanrM f init #v[] = pure #v[init]
-- Mathlib.Topology.Constructions.SumProd
IsClosed.prod : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s₁ : Set X} {s₂ : Set Y},
  IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ×ˢ s₂)
-- Mathlib.Data.Finset.Prod
Finset.mem_offDiag : ∀ {α : Type u_1} {s : Finset α} {x : α × α}, x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_eq_ofIntClamp : ∀ {x : ℤ} {h₁ : Int32.minValue.toInt ≤ x} {h₂ : x ≤ Int32.maxValue.toInt}, Int32.ofIntLE x h₁ h₂ = Int32.ofIntClamp x
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntryD.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (fallback : (a : α) × β a) (x : List ((a : α) × β a)),
  Std.Internal.List.getEntryD a fallback x =
    match x with
    | [] => fallback
    | ⟨k, v⟩ :: l => bif k == a then ⟨k, v⟩ else Std.Internal.List.getEntryD a fallback l