mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M`, if an
`AddCommMonoid` map `g : M →+ P` induces a map `f.lift hg : N →+ P` then for all
`z : N, v : P`, we have `f.lift hg z = v ↔ g x = g y + v`, where `x : M, y ∈ S` are such that
`z + f y = f x`.  -/
AddSubmonoid.LocalizationMap.lift_spec : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N) (v : P),
  (f.lift hg) z = v ↔ g (f.sec z).1 = g ↑(f.sec z).2 + v
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.ExprPtr.mk.injEq : ∀ (expr expr_1 : Lean.Expr), ({ expr := expr } = { expr := expr_1 }) = (expr = expr_1)
-- Std.Time.Time.HourMarker
Std.Time.instLawfulEqOrdHourMarker : Std.LawfulEqOrd Std.Time.HourMarker
-- Init.GrindInstances.ToInt
Lean.Grind.instNegIntIi : Lean.Grind.ToInt.Neg ℤ Lean.Grind.IntInterval.ii
-- Init.Data.Array.Lemmas
Array.foldr_filter : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : α → β → β} {xs : Array α} {init : β},
  Array.foldr f init (Array.filter p xs) = Array.foldr (fun x y => if p x = true then f x y else y) init xs
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.xRep.eq_1 : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, WeierstrassCurve.Affine.Point.zero.xRep = ![1, 0]
-- Init.Data.List.Pairwise
List.Pairwise.take : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {i : ℕ}, List.Pairwise R l → List.Pairwise R (List.take i l)
-- Mathlib.Analysis.Convex.Extreme
Convex.mem_extremePoints_iff_convex_sdiff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E] {A : Set E} {x : E},
  Convex 𝕜 A → (x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ Convex 𝕜 (A \ {x}))
-- Mathlib.Logic.Equiv.Basic
Function.Involutive.toPerm_involutive : ∀ {α : Sort u_1} {f : α → α} (h : Function.Involutive f), Function.Involutive ⇑(Function.Involutive.toPerm f h)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Filter.Tendsto.rpow_const : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ} {x p : ℝ},
  Filter.Tendsto f l (nhds x) → x ≠ 0 ∨ 0 ≤ p → Filter.Tendsto (fun a => f a ^ p) l (nhds (x ^ p))
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mapGlueData_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i j : D.J), (D.mapGlueData F).f i j = F.map (D.f i j)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.const_vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {𝕜 : Type u_5} [inst_1 : VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.AEStronglyMeasurable (c +ᵥ f) μ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, (m₁ \ m₂).getKey? k = if k ∈ m₂ then none else m₁.getKey? k
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_natCast_cpow_le_norm_natCast_cpow_of_pos : ∀ {n : ℕ}, 0 < n → ∀ {w z : ℂ}, w.re ≤ z.re → ‖↑n ^ w‖ ≤ ‖↑n ^ z‖
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
continuousAt_jacobiTheta₂' : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_toReal_eq_two_mul_add_two_pi : ∀ {θ : Real.Angle}, (2 • θ).toReal = 2 * θ.toReal + 2 * Real.pi ↔ θ.toReal ≤ -Real.pi / 2
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The canonical isomorphism `S.opcycles ≅ cokernel S.f`.  -/
CategoryTheory.ShortComplex.opcyclesIsoCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasRightHomology] →
          [inst_3 : CategoryTheory.Limits.HasCokernel S.f] → S.opcycles ≅ CategoryTheory.Limits.cokernel S.f
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Mathlib.Tactic.DepRewrite
/-- Cast `e : te[p/x, rfl/h, ...]` to `h ▸ e : te`.  -/
Mathlib.Tactic.DepRewrite.castFwd : Lean.Expr →
  Lean.Expr →
    Lean.Expr → Lean.Expr → Lean.Expr → Array (Lean.FVarId × Lean.Expr) → Std.HashSet Lean.FVarId → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.GradedMonoid
One.gOne_one : ∀ (ι : Type u_1) {R : Type u_2} [inst : Zero ι] [inst_1 : One R], GradedMonoid.GOne.one = 1
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_comp : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : DecidableEq ι] [inst_8 : AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B}
  [inst_9 : GradedAlgebra 𝒜] [inst_10 : GradedAlgebra ℬ] (g : B →ₐ[R] C) (f : 𝒜 →ₐᵍ[R] ℬ), ⇑(g.comp ↑f) = ⇑g ∘ ⇑f
-- Mathlib.Algebra.BigOperators.Finprod
/-- A version of `one_le_finprod'` for `PosMulMono` in place of `MulLeftMono`.  -/
one_le_finprod : ∀ {α : Sort u_4} {M : Type u_7} [inst : CommMonoidWithZero M] [inst_1 : Preorder M] [ZeroLEOneClass M] [PosMulMono M]
  {f : α → M}, (∀ (i : α), 1 ≤ f i) → 1 ≤ ∏ᶠ (i : α), f i
-- Mathlib.Algebra.Group.Equiv.Opposite
MonoidHom.op_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (a : Mᵐᵒᵖ),
  (MonoidHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
-- Init.Data.Int.Linear
Int.Internal.Linear.orOver_one : ∀ {p : ℕ → Prop}, Int.Internal.Linear.OrOver 1 p → p 0
-- Init.Grind.Order
Lean.Grind.Order.le_trans : ∀ {α : Type u_1} [inst : LE α] [Std.IsPreorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Topology.Algebra.Monoid.Defs
/-- Eta-expanded form of `ContinuousAt.mul` -/
ContinuousAt.fun_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {x : X},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun i => f i * g i) x
-- Init.Data.Array.Lemmas
/-- Variant of `replicate_succ` that prepends `a` at the beginning of the array.  -/
Array.replicate_succ' : ∀ {n : ℕ} {α : Type u_1} {a : α}, Array.replicate (n + 1) a = #[a] ++ Array.replicate n a
-- Init.Data.Vector.Range
Vector.count_range' : ∀ {a s n step : ℕ},
  autoParam (0 < step) Vector.count_range'._auto_1 →
    Vector.count a (Vector.range' s n step) = if ∃ i < n, a = s + step * i then 1 else 0
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.State.equalMVarIds : Aesop.EqualUpToIdsM.State → Std.HashMap Lean.MVarId Lean.MVarId
-- Mathlib.GroupTheory.Perm.Sign
/-- An induction principle for permutations. If `P` holds for the identity permutation, and
is preserved under composition with a non-trivial swap, then `P` holds for all permutations.  -/
Equiv.Perm.swap_induction_on : ∀ {α : Type u} [inst : DecidableEq α] [Finite α] {motive : Equiv.Perm α → Prop} (f : Equiv.Perm α),
  motive 1 → (∀ (f : Equiv.Perm α) (x y : α), x ≠ y → motive f → motive (Equiv.swap x y * f)) → motive f
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.alias.inj : ∀ {p p_1 : Lean.Parser.ParserAliasValue},
  Lean.Parser.ParserResolution.alias p = Lean.Parser.ParserResolution.alias p_1 → p = p_1
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iio_insert : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : DecidableEq α] (b : α),
  insert b (Finset.Iio b) = Finset.Iic b
-- Mathlib.Algebra.Star.Module
skewAdjointPart_apply_coe : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] (x : A), ↑((skewAdjointPart R) x) = ⅟2 • (x - star x)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_injective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Injective ⇑f → Function.Injective (Subgroup.map f)
-- Mathlib.Analysis.Matrix.Spectrum
/-- The eigenvalues of a Hermitian matrix, reusing the index `n` of the matrix entries.  -/
Matrix.IsHermitian.eigenvalues : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] → {n : Type u_2} → [Fintype n] → {A : Matrix n n 𝕜} → [DecidableEq n] → A.IsHermitian → n → ℝ
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.isProgressive : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β}
  [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β],
  MeasureTheory.IsStronglyProgressive f u → MeasureTheory.IsProgressive f u
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.d₁_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  ¬c₁.Rel i₁ (c₁.next i₁) → HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.mk.inj : ∀ {α : Type u_7} {β : Type u_8} {inst : MulZeroOneClass α} {inst_1 : MulZeroOneClass β} {toZeroHom : ZeroHom α β}
  {map_one' : toZeroHom.toFun 1 = 1}
  {map_mul' : ∀ (x y : α), toZeroHom.toFun (x * y) = toZeroHom.toFun x * toZeroHom.toFun y} {toZeroHom_1 : ZeroHom α β}
  {map_one'_1 : toZeroHom_1.toFun 1 = 1}
  {map_mul'_1 : ∀ (x y : α), toZeroHom_1.toFun (x * y) = toZeroHom_1.toFun x * toZeroHom_1.toFun y},
  { toZeroHom := toZeroHom, map_one' := map_one', map_mul' := map_mul' } =
      { toZeroHom := toZeroHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 } →
    toZeroHom = toZeroHom_1
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.findIdxNth.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 x_2 : ℕ) →
        ((x s : ℕ) → motive [] x s) →
          ((a : α) → (xs : List α) → (s : ℕ) → motive (a :: xs) 0 s) →
            ((a : α) → (xs : List α) → (n s : ℕ) → motive (a :: xs) n.succ s) → motive x x_1 x_2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_1 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.not with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_1 ()
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.ennrealRatEmbed.eq_1 : ∀ (n : ℕ), MeasureTheory.SimpleFunc.ennrealRatEmbed n = ENNReal.ofReal ↑((Encodable.decode n).getD 0)
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.replaceRecApps.processRec : (recFnName : Lean.Name) → ℕ → Lean.Expr → Lean.Expr → Lean.Elab.WF.RecM✝ recFnName Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.addY P Q = (P 0 * Q 2) ^ 3 * Q 1
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D))
  (X_1 : C),
  (((CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso C D).hom.app X).app X_1).f =
    (X.obj X_1).p
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.mapBaseChange_surjective : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B],
  Function.Surjective ⇑(algebraMap A B) → Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)
-- Mathlib.Topology.Defs.Induced
Topology.IsCoherentWith.mk : ∀ {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)},
  (∀ (u : Set X), (∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u) → Topology.IsCoherentWith S
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_iSizeToInt : ∀ (x : ISize) {h₁ : Int16.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int16.maxValue.toInt},
  Int16.ofIntLE x.toInt h₁ h₂ = x.toInt16
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.one_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : MulOneClass R] (x : n → R),
  Matrix.vecMulVec 1 x = Matrix.replicateRow m x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapGrp_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal],
  e.mapGrp.counitIso =
    CategoryTheory.Functor.mapGrpCompIso.symm ≪≫
      CategoryTheory.Functor.mapGrpNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapGrpIdIso
-- Init.MetaTypes
/-- Configures how to determine definitional equality between two structure instances.
See documentation for `Lean.Meta.EtaStructMode`.
 -/
Lean.Meta.DSimp.Config.etaStruct : Lean.Meta.DSimp.Config → Lean.Meta.EtaStructMode
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_modify_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [Inhabited α] {k : α} {f : β k → β k}, m.WF → ∀ {hc : k ∈ m.modify k f}, (m.modify k f).getKey k hc = k
-- Std.Http.Protocol.H1
/-- Handles transitions after a writer message completes.

Depending on reader state and keep-alive, this either resets for next message
or closes the writer/connection.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processCompleteStep : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- **Alias** of `sub_apply`. -/
ContinuousMultilinearMap.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State.grindState : Lean.Elab.Tactic.Grind.State → Lean.Meta.Grind.State
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionParams.toJson : Lean.Lsp.CompletionParams → Lean.Json
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- `norm` as a `MonoidHom`.  -/
Zsqrtd.normMonoidHom : {d : ℤ} → ℤ√d →* ℤ
-- Mathlib.RingTheory.Derivation.Basic
/-- A noncomputable version of `liftOfRightInverse` for surjective homomorphisms.
 -/
Derivation.liftOfSurjective : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R M] →
                {F : Type u_4} →
                  [inst_5 : FunLike F A M] →
                    [AlgHomClass F R A M] →
                      {f : F} →
                        Function.Surjective ⇑f →
                          ⦃d : Derivation R A A⦄ → (∀ (x : A), f x = 0 → f (d x) = 0) → Derivation R M M
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.lift_π : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j))
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.lift f hf)
      (CategoryTheory.Limits.chosenEnd.π F j) =
    f j
-- Mathlib.RingTheory.Ideal.Over
Ideal.eq_top_iff_of_liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [P.LiesOver p], P = ⊤ ↔ p = ⊤
-- Mathlib.CategoryTheory.Opposites
/-- An equivalence between `C` and `Dᵒᵖ` gives an equivalence between `Cᵒᵖ` and `D`.  -/
CategoryTheory.Equivalence.leftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ Dᵒᵖ) → (Cᵒᵖ ≌ D)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), |a| = a ⊔ -a
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).unop =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.unop X)).symm
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.uniqueHomToTrivial_default_hom : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (A : CategoryTheory.Mon D), default.hom = CategoryTheory.SemiCartesianMonoidalCategory.toUnit A.X
-- Aesop.Forward.RuleInfo
/-- Information about the decomposed type of a forward rule.  -/
Aesop.ForwardRuleInfo : Type
-- Mathlib.Data.EReal.Operations
EReal.top_sub_bot : ⊤ - ⊥ = ⊤
-- Lean.Expr
Lean.Expr.Data.hasExprMVar : Lean.Expr.Data → Bool
-- Init.Data.Nat.Lemmas
Nat.add_lt_iff_lt_sub_right : ∀ {a b c : ℕ}, a + b < c ↔ a < c - b
-- Mathlib.Order.SetNotation
/-- Notation for `Set.iUnion`. Indexed union of a family of sets  -/
Set.«term⋃_,_» : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- Given a presheaf of modules `M`, this is the coproduct of
all free Yoneda presheaves `m.freeYoneda` for all `m : M.Elements`.  -/
PresheafOfModules.freeYonedaCoproduct : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → PresheafOfModules R → PresheafOfModules R
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.isoMk_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G : CategoryTheory.LaxBraidedFunctor C D} (e : F.toFunctor ≅ G.toFunctor)
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom],
  (CategoryTheory.LaxBraidedFunctor.isoMk e).inv = CategoryTheory.LaxBraidedFunctor.homMk e.inv
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_cyclesMap'_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  CategoryTheory.IsIso φ.τ₂ →
    CategoryTheory.Mono φ.τ₃ →
      ∀ (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
        CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a `CommSemigroup` under pointwise operations if `α` is.  -/
Finset.commSemigroup : {α : Type u_2} → [DecidableEq α] → [CommSemigroup α] → CommSemigroup (Finset α)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop.arrowIso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C}
  {f : X ⟶ Y} (hf : Φ.prop f), hf.arrowIso.hom.right = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Quaternion
Quaternion.coe_one : ∀ {R : Type u_3} [inst : CommRing R], ↑1 = 1
-- Lean.Util.InstantiateLevelParams
_private.Lean.Util.InstantiateLevelParams.0.Lean.Expr.instantiateLevelParamsCore.replaceFn : (Lean.Name → Option Lean.Level) → Lean.Expr → Option Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- `spineToSimplex` is a right inverse to `spine X m`.  -/
SSet.Truncated.StrictSegal.spine_spineToSimplex : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (self : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1),
  X.spine m h ∘ self.spineToSimplex m ⋯ = id
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.dist_set_exists : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C