mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.rightUnitor_inv_app : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B),
  (CategoryTheory.Bicategory.rightUnitor F).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Grp.forget C = (CategoryTheory.Grp.forget₂Mon C).comp (CategoryTheory.Mon.forget C)
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
/-- Proving a fact about `a : adjoin R {x}` is the same as proving it for
`aeval x p` where `p`is an arbitrary polynomial.  -/
Algebra.adjoin_singleton_induction : ∀ (R : Type u) {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A)
  {M : ↥R[x] → Prop} (a : ↥R[x]), (∀ (p : Polynomial R), M ⟨(Polynomial.aeval x) p, ⋯⟩) → M a
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.lower_bound_le_one : ∀ {N : ℕ}, 1 ≤ N → N ≤ 4096 → ↑N * Real.exp (-4 * √(Real.log ↑N)) ≤ 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.distinct_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  List.Pairwise (fun a b => (a == b) = false) m.keys
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.sub : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f g : M → E'} {f' g' : TangentSpace I z →L[𝕜] E'},
  HasMFDerivAt% f z f' → HasMFDerivAt% g z g' → HasMFDerivAt% (f - g) z (f' - g')
-- Mathlib.CategoryTheory.Limits.Fubini
/-- A structure carrying a diagram of cocones over the functors `F.obj j`.
 -/
CategoryTheory.Limits.DiagramOfCocones : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            CategoryTheory.Functor J (CategoryTheory.Functor K C) → Type (max (max (max (max u_1 u_2) u_3) v_1) v_3)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdDiagnosticRelatedInformation : Ord Lean.Lsp.DiagnosticRelatedInformation
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `AddLECancellable.eq_tsub_of_add_eq'` for a version assuming that `b = a + c` itself is
cancellable rather than `c`.  -/
AddLECancellable.eq_tsub_of_add_eq : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable c → a + c = b → a = b - c
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
eval_det_add_X_smul : ∀ {n : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_3} [inst_2 : CommRing R]
  (A : Matrix n n (Polynomial R)) (M : Matrix n n R),
  Polynomial.eval 0 (A + Polynomial.X • M.map ⇑Polynomial.C).det = Polynomial.eval 0 A.det
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
tendsto_arithGeom_nhds_of_lt_one : ∀ {R : Type u_1} {a b u₀ : R} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R]
  [inst_4 : TopologicalSpace R] [OrderTopology R],
  0 ≤ a → a < 1 → Filter.Tendsto (arithGeom a b u₀) Filter.atTop (nhds (b / (1 - a)))
-- Plausible.Testable
Plausible.TestResult.toString : {p : Prop} → Plausible.TestResult p → String
-- Init.Control.EState
EStateM.instReprResult : {ε σ α : Type u} → [Repr ε] → [Repr α] → Repr (EStateM.Result ε σ α)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_coe_toMulEquiv_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  ⇑(↑e).symm = ⇑e.symm
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S) (M N : ↑(F.obj { as := Opposite.op S })),
  Function.Bijective (F.toDescentData f).map ↔
    CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N)
      (CategoryTheory.Presieve.ofArrows (fun i => CategoryTheory.Over.mk (f i)) fun i =>
        CategoryTheory.Over.homMk (f i) ⋯)
-- Mathlib.Algebra.Module.Bimodule
/-- A `Submodule` over `R ⊗[ℕ] S` is naturally also a `Submodule` over the canonically-isomorphic
ring `R ⊗[ℤ] S`.  -/
Subbimodule.toSubbimoduleInt : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Ring R] →
        [inst_1 : Ring S] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : Module S M] →
                [inst_5 : SMulCommClass R S M] → Submodule (TensorProduct ℕ R S) M → Submodule (TensorProduct ℤ R S) M
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup : ∀ {ι : Type u} [Small.{v, u} ι] {f : ι → Cardinal.{v}},
  Cardinal.aleph0 ≤ Cardinal.mk ι →
    Cardinal.lift.{v, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, v} (⨆ i, f i) →
      Cardinal.sum f = Cardinal.lift.{u, v} (⨆ i, f i)
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.SubmonoidPresheaf.mk.sizeOf_spec : ∀ {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (obj : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ↑(F.obj U))
  (map :
    ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
      obj U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (obj V)),
  sizeOf { obj := obj, map := map } = 1
-- Mathlib.Tactic.Linter.Header
/-- `parseUpToHere pos post` takes as input `pos : String.Pos` and the optional `post : String`.
It parses the current file from the beginning until `pos`, appending `post` at the end.
It returns a syntax node of kind `Lean.Parser.Module.module`.
The option of appending a final string to the text gives more control to avoid syntax errors,
for instance in the presence of `#guard_msgs in` or `set_option ... in`.

Note that this parsing will *not* be successful on every file.  However, if the linter is
parsing the file linearly, it will only need to parse
* the imports (that are always parseable) and
* the first non-import command that is supposed to be a module doc-string (so again always
  parseable).

In conclusion, either the parsing is successful, and the linter can continue with its analysis,
or the parsing is not successful and the linter will flag a missing module doc-string!
 -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.parseUpToHere : String.Pos.Raw → optParam String "" → Lean.Elab.Command.CommandElabM Lean.Syntax
-- Mathlib.Algebra.Algebra.Epi
/-- **Alias** of `Algebra.isEpi_iff_surjective_algebraMap_of_finite`. -/
RingHom.surjective_of_tmul_eq_tmul_of_finite : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Module.Finite R A],
  Algebra.IsEpi R A ↔ Function.Surjective ⇑(algebraMap R A)
-- Mathlib.Order.Concept
Order.isIntent_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β}, Order.IsIntent r t ↔ upperPolar r (lowerPolar r t) = t
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.vaddCommClass_right : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass M'] [inst_1 : VAdd α β] [inst_2 : VAdd M' β]
  [VAddCommClass α M' β] (S : AddSubmonoid M'), VAddCommClass α (↥S) β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.map_fst_toList_eq_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  List.map Sigma.fst m.toList = m.keys
-- Init.Data.UInt.Bitwise
UInt32.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : UInt32}, (-1) <<< b &&& a <<< b = a <<< b
-- Batteries.Data.String.Legacy
String.Pos.Raw.get.eq_1 : ∀ (s : String) (p : String.Pos.Raw), String.Pos.Raw.get s p = String.Pos.Raw.utf8GetAux s.toList 0 p
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_two : Nat.sqrt 2 = 1
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.trans_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant A] (P P' : HomotopicalAlgebra.Cylinder A) [inst_3 : P'.IsGood],
  (P.trans P').i₁ = CategoryTheory.CategoryStruct.comp P'.i₁ (CategoryTheory.Limits.pushout.inr P.i₁ P'.i₀)
-- Mathlib.Analysis.Normed.Module.Complemented
ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_toLinearEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : CompleteSpace E] [inst_8 : CompleteSpace (F × G)]
  {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : (↑f).range = ⊤) (hg : (↑g).range = ⊤) (hfg : IsCompl (↑f).ker (↑g).ker),
  ↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) = (↑f).equivProdOfSurjectiveOfIsCompl (↑g) hf hg hfg
-- Mathlib.LinearAlgebra.CliffordAlgebra.Star
/-- Note that this not match the `star_smul` implied by `StarModule`; it certainly could if we
also conjugated all the scalars, but there appears to be nothing in the literature that advocates
doing this.  -/
CliffordAlgebra.star_smul : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (r : R) (x : CliffordAlgebra Q), star (r • x) = r • star x
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_self_pos_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s : Finset α}, 0 < s.mulEnergy s ↔ s.Nonempty
-- Init.Data.SInt.Basic
/-- Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the
`DecidableLE Int32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : Int32) ≤ 7 then "yes" else "no") = "yes"`
 * `(if (15 : Int32) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : Int32) ≤ 5 then "yes" else "no") = "no"`
 * `show (7 : Int32) ≤ 7 by decide`
 -/
Int32.decLe : (a b : Int32) → Decidable (a ≤ b)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_tsum : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_5} [Countable ι] {f : ι → α → E},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
    ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤ → μ[fun a => ∑' (i : ι), f i a | m] =ᵐ[μ] fun a => ∑' (i : ι), μ[f i | m] a
-- Init.Data.List.Sublist
List.infix_cons_iff : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.condition : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S : CategoryTheory.ShortComplex C} [self : S.HasRightHomology], Nonempty S.RightHomologyData
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.map_comp : ∀ {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] {G H : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  (f : F ⟶ G) (g : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.map f) (CategoryTheory.Limits.chosenEnd.map g) =
    CategoryTheory.Limits.chosenEnd.map (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `Field` instance for `type` if available.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.fieldInst? : Lean.Meta.Grind.Arith.CommRing.CommRing → Option Lean.Expr
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH2_τ₃ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  (groupHomology.mapShortComplexH2 f φ).τ₃ = groupHomology.chainsMap₁ f φ
-- Init.Prelude
/-- Characters are Unicode [scalar values](http://www.unicode.org/glossary/#unicode_scalar_value).
 -/
Char : Type
-- Mathlib.CategoryTheory.Sites.Sieves
/-- When `F` is fully faithful, the Galois connection is a Galois coinsertion.  -/
CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Full] →
            [F.Faithful] →
              (X : C) →
                GaloisCoinsertion (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The ring homomorphism from a given ring in the diagram to the colimit
ring.  -/
RingCat.Colimits.coconeMorphism : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → (j : J) → F.obj j ⟶ RingCat.Colimits.colimit F
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_aleph0 : Cardinal.aleph0.IsRegular
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [h : μ.InnerRegular] (c : ENNReal), (c • μ).InnerRegular
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Under a continuous linear map, the image of the `TopologicalClosure` of a submodule is
contained in the `TopologicalClosure` of its image.  -/
Submodule.topologicalClosure_map : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : RingHomSurjective σ₁₂]
  [inst_9 : TopologicalSpace R₁] [inst_10 : TopologicalSpace R₂] [inst_11 : ContinuousSMul R₁ M₁]
  [inst_12 : ContinuousAdd M₁] [inst_13 : ContinuousSMul R₂ M₂] [inst_14 : ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂)
  (s : Submodule R₁ M₁), Submodule.map (↑f) s.topologicalClosure ≤ (Submodule.map (↑f) s).topologicalClosure
-- Init.Data.Iterators.Consumers.Total
Std.Iter.Total.mk.injEq : ∀ {α β : Type w} (it it_1 : Std.Iter β), ({ it := it } = { it := it_1 }) = (it = it_1)
-- Mathlib.Logic.Function.Basic
Function.eq_update_iff : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {a : α} {b : β a} {f g : (a : α) → β a},
  g = Function.update f a b ↔ g a = b ∧ ∀ (x : α), x ≠ a → g x = f x
-- Mathlib.LinearAlgebra.Matrix.DualNumber
Matrix.dualNumberEquiv_symm_apply : ∀ {R n : Type} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (d : DualNumber (Matrix n n R)),
  Matrix.dualNumberEquiv.symm d = Matrix.of fun i j => (TrivSqZeroExt.fst d i j, TrivSqZeroExt.snd d i j)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_add : ∀ (x y : ℂ), Complex.sinh (x + y) = Complex.sinh x * Complex.cosh y + Complex.cosh x * Complex.sinh y
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.smul_apply : ∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} [inst : AddZeroClass A] [inst_1 : AddZeroClass B]
  [inst_2 : DistribSMul M B] (m : M) (f : A →+ B) (a : A), (m • f) a = m • f a
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.of_subsingleton_cod : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [Subsingleton α], HasSum f 0 L
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_mem : ∀ {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} [self : G.LocallyCoverDense K] ⦃X : C⦄ (T : ↑(K (G.obj X))),
  CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPullback G ↑T) ∈ K (G.obj X)
-- Mathlib.Data.Fintype.Sets
Fintype.finsetEquivSet_apply : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), Fintype.finsetEquivSet s = ↑s
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instFunLikeForallProp.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddCon.instFunLikeForallProp = { coe := fun c => ⇑c.toSetoid, coe_injective := ⋯ }
-- Lean.DocString.Markdown
/-- Renderers registered in imported modules.  -/
Lean.Doc.MdRendererState.imported : Lean.Doc.MdRendererState → Lean.NameMap Lean.Name
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.isGLB_sInf : ∀ {s : Set ℝ}, s.Nonempty → BddBelow s → IsGLB s (sInf s)
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanLocationLink.mk.injEq : ∀ (toLocationLink : Lean.Lsp.LocationLink) (ident? : Option Lean.Lsp.LeanDeclIdent) (isDefault : Bool)
  (toLocationLink_1 : Lean.Lsp.LocationLink) (ident?_1 : Option Lean.Lsp.LeanDeclIdent) (isDefault_1 : Bool),
  ({ toLocationLink := toLocationLink, ident? := ident?, isDefault := isDefault } =
      { toLocationLink := toLocationLink_1, ident? := ident?_1, isDefault := isDefault_1 }) =
    (toLocationLink = toLocationLink_1 ∧ ident? = ident?_1 ∧ isDefault = isDefault_1)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.range_le_iff_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N}
  {p : L.Substructure N}, f.range ≤ p ↔ FirstOrder.Language.Substructure.comap f p = ⊤
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f` is
continuous at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b`.  -/
intervalIntegral.integral_hasDerivAt_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
      ContinuousAt f b → HasDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int8.toBitVec_ite : ∀ {c : Prop} {t e : Int8} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.Order.InitialSeg
InitialSeg.lt_iff_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a a' : α} [inst_1 : PartialOrder α] (f : α ≤i β),
  f a < f a' ↔ a < a'
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?_eq_getEntryGT?ₘ' : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGT? k t = Std.DTreeMap.Internal.Impl.getEntryGT?ₘ' k t
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
AntitoneOn.memLp_top : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E},
  AntitoneOn f s → ∀ {a b : X}, IsLeast s a → IsGreatest s b → MeasurableSet s → MeasureTheory.MemLp f ⊤ (μ.restrict s)
-- Mathlib.Data.ZMod.Defs
_private.Mathlib.Data.ZMod.Defs.0.Fin.left_distrib_aux : ∀ (n : ℕ) (a b c : Fin n), a * (b + c) = a * b + a * c
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.post_map : ∀ {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) {X Y : CategoryTheory.CostructuredArrow F S} (f : X ⟶ Y),
  (CategoryTheory.CostructuredArrow.post F G S).map f = CategoryTheory.CostructuredArrow.homMk f.left ⋯
-- Mathlib.GroupTheory.ResiduallyFinite
/-- A group `G` is residually finite if the intersection of all finite index normal subgroups is
trivial.  -/
Group.ResiduallyFinite : (G : Type u_1) → [Group G] → Prop
-- Mathlib.Analysis.Calculus.TangentCone.Real
Convex.span_tangentConeAt : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  {s : Set E} {x : E} [IsTopologicalAddGroup E],
  Convex ℝ s → (interior s).Nonempty → x ∈ closure s → Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.mk.injEq : ∀ (funId : Lean.Ident) (ctorVal? : Option Lean.ConstructorVal) (explicit ellipsis : Bool)
  (paramDecls : Array (Lean.Name × Lean.BinderInfo)) (paramDeclIdx : ℕ) (namedArgs : Array Lean.Elab.Term.NamedArg)
  (usedNames : Std.HashSet Lean.Name) (args : List Lean.Elab.Term.Arg) (newArgs : Array Lean.Term)
  (funId_1 : Lean.Ident) (ctorVal?_1 : Option Lean.ConstructorVal) (explicit_1 ellipsis_1 : Bool)
  (paramDecls_1 : Array (Lean.Name × Lean.BinderInfo)) (paramDeclIdx_1 : ℕ)
  (namedArgs_1 : Array Lean.Elab.Term.NamedArg) (usedNames_1 : Std.HashSet Lean.Name) (args_1 : List Lean.Elab.Term.Arg)
  (newArgs_1 : Array Lean.Term),
  ({ funId := funId, ctorVal? := ctorVal?, explicit := explicit, ellipsis := ellipsis, paramDecls := paramDecls,
        paramDeclIdx := paramDeclIdx, namedArgs := namedArgs, usedNames := usedNames, args := args,
        newArgs := newArgs } =
      { funId := funId_1, ctorVal? := ctorVal?_1, explicit := explicit_1, ellipsis := ellipsis_1,
        paramDecls := paramDecls_1, paramDeclIdx := paramDeclIdx_1, namedArgs := namedArgs_1, usedNames := usedNames_1,
        args := args_1, newArgs := newArgs_1 }) =
    (funId = funId_1 ∧
      ctorVal? = ctorVal?_1 ∧
        explicit = explicit_1 ∧
          ellipsis = ellipsis_1 ∧
            paramDecls = paramDecls_1 ∧
              paramDeclIdx = paramDeclIdx_1 ∧
                namedArgs = namedArgs_1 ∧ usedNames = usedNames_1 ∧ args = args_1 ∧ newArgs = newArgs_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_one_sub' : ∀ {x y : ℝ}, 0 ≤ x → 1 - y ≠ 0 → x ^ (1 - y) = x / x ^ y
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_to_volumeForm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.areaForm x) y = o.volumeForm ![x, y]
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_empty : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} [Nonempty α],
  (Fintype.piFinset fun x => ∅) = ∅
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.any : (Lean.FVarId → Lean.Expr → Bool) → Lean.Meta.FVarSubst → Bool
-- Mathlib.Algebra.Ring.Parity
even_iff_exists_two_mul : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a ↔ ∃ b, a = 2 * b
-- Mathlib.NumberTheory.AbelSummation
/-- Specialized version of `sum_mul_eq_sub_integral_mul` when `c 0 = c 1 = 0`.  -/
sum_mul_eq_sub_integral_mul₁ : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  c 0 = 0 →
    c 1 = 0 →
      ∀ (b : ℝ),
        (∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t) →
          MeasureTheory.IntegrableOn (deriv f) (Set.Icc 2 b) MeasureTheory.volume →
            ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, f ↑k * c k =
              f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k