mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Basic
/-- Decides whether two 64-bit signed integers are equal. Usually accessed via the `DecidableEq Int64`
instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Int64.decEq 123 123 = .isTrue rfl`
 * `(if ((-7) : Int64) = 7 then "yes" else "no") = "no"`
 * `show (7 : Int64) = 7 by decide`
 -/
Int64.decEq : (a b : Int64) → Decidable (a = b)
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffOn.dist : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f g : G → E}
  {s : Set G} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → ContDiffOn ℝ n g s → (∀ x ∈ s, f x ≠ g x) → ContDiffOn ℝ n (fun y => dist (f y) (g y)) s
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_functor_obj_X : ∀ (X : Bipointed), (Bipointed.swapEquiv.functor.obj X).X = X.X
-- Mathlib.Algebra.FiveLemma
/-- A special case of one four lemma such that the right-most term is zero in terms
of additive groups. For a diagram explaining the variables, see the module docstring.  -/
AddMonoidHom.injective_of_surjective_of_injective_of_right_exact : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : AddGroup M₁]
  [inst_1 : AddGroup M₂] [inst_2 : AddGroup M₃] [inst_3 : AddGroup N₁] [inst_4 : AddGroup N₂] [inst_5 : AddGroup N₃]
  (f₁ : M₁ →+ M₂) (f₂ : M₂ →+ M₃) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂) (i₃ : M₃ →+ N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₁ → Function.Injective ⇑i₂ → Function.Surjective ⇑f₂ → Function.Injective ⇑i₃
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.dateFromModifier : {modifier : Std.Time.Modifier} → Std.Time.DateFormat → Std.Time.DateTime → Std.Time.TypeFormat modifier
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- Morphisms map the zero pseudoelement to the zero pseudoelement.  -/
CategoryTheory.Abelian.Pseudoelement.apply_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  CategoryTheory.Abelian.Pseudoelement.pseudoApply f 0 = 0
-- Lean.Elab.Parallel
/-- Runs a list of TacticM computations in parallel (without cancellation hook).

Returns an iterator that yields results in original order, wrapped in `Except Exception α`.
 -/
Lean.Elab.Tactic.TacticM.parIter : {α : Type} →
  List (Lean.Elab.Tactic.TacticM α) →
    Lean.Elab.Tactic.TacticM (Std.IterM Lean.Elab.Tactic.TacticM (Except Lean.Exception α))
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.quotientRangeInlEquivRight.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  (S : GroupExtension N E G), S.quotientRangeInlEquivRight = QuotientGroup.liftEquiv S.inl.range ⋯ ⋯
-- Mathlib.LinearAlgebra.RootSystem.Basic
_private.Mathlib.LinearAlgebra.RootSystem.Basic.0.RootPairing.choose_choose_eq_of_mapsTo : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) (root : ι ↪ M)
  (coroot : ι ↪ N) (i j : ι)
  (h :
    ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)),
  (∀ (i : ι), (p (root i)) (coroot i) = 2) → ⋯.choose = j
-- Mathlib.Topology.GDelta.Basic
IsGδ.empty : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsGδ ∅
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.brecOn.go : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        {motive : Turing.TM2.Stmt Γ Λ σ → Sort u} →
          (t : Turing.TM2.Stmt Γ Λ σ) →
            ((t : Turing.TM2.Stmt Γ Λ σ) → Turing.TM2.Stmt.below t → motive t) → motive t ×' Turing.TM2.Stmt.below t
-- Init.Data.Int.Linear
Int.Internal.Linear.not_le_of_le : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.not_le_of_le_cert p₁ p₂ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 → ¬Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0
-- Mathlib.Analysis.Complex.OpenMapping
/-- A function `f : ℂ → ℂ` which is analytic at a point `z₀` is either constant in a neighborhood
of `z₀`, or behaves locally like an open function (in the sense that the image of every neighborhood
of `z₀` is a neighborhood of `f z₀`, as in `isOpenMap_iff_nhds_le`). For a function `f : E → ℂ`
the same result holds, see `AnalyticAt.eventually_constant_or_nhds_le_map_nhds`.  -/
AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux : ∀ {f : ℂ → ℂ} {z₀ : ℂ}, AnalyticAt ℂ f z₀ → (∀ᶠ (z : ℂ) in nhds z₀, f z = f z₀) ∨ nhds (f z₀) ≤ Filter.map f (nhds z₀)
-- Mathlib.CategoryTheory.Abelian.Subobject
CategoryTheory.Subobject.lift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Sort u_1} {X : C}
  (F F_1 : ⦃A : C⦄ → (f : A ⟶ X) → [CategoryTheory.Mono f] → α) (e_F : F = F_1)
  (h :
    ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g] (i : A ≅ B),
      CategoryTheory.CategoryStruct.comp i.hom g = f → F f = F g)
  (a a_1 : CategoryTheory.Subobject X),
  a = a_1 → CategoryTheory.Subobject.lift F h a = CategoryTheory.Subobject.lift F_1 ⋯ a_1
-- Mathlib.CategoryTheory.Generator.Basic
/-- We say that `G` is a coseparator if the functor `C(-, G)` is faithful.  -/
CategoryTheory.IsCoseparator : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Prop
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- We have a bijection of homsets which will be used to construct the left adjoint to the comparison
functor.
 -/
CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (adj : F ⊣ G) →
              (A : adj.toMonad.Algebra) →
                (B : D) →
                  [inst_2 : CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] →
                    (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A ⟶ B) ≃
                      (A ⟶ (CategoryTheory.Monad.comparison adj).obj B)
-- Init.Data.Array.DecidableEq
Array.isEqv_eq_decide : ∀ {α : Type u_1} (xs ys : Array α) (r : α → α → Bool),
  xs.isEqv ys r = if h : xs.size = ys.size then decide (∀ (i : ℕ) (h' : i < xs.size), r xs[i] ys[i] = true) else false
-- Init.Prelude
/-- Create array `#[a₁, a₂, a₃, a₄]`  -/
Array.mkArray4 : {α : Type u} → α → α → α → α → Array α
-- Batteries.Util.Cache
/-- Access the cache. Calling this function for the first time will initialize the cache
with the function provided in the constructor.
 -/
Batteries.Tactic.DeclCache.get : {α : Type} → Batteries.Tactic.DeclCache α → Lean.MetaM α
-- Mathlib.Algebra.Algebra.Unitization
/-- A non-unital algebra homomorphism from `A` into a unital `R`-algebra `C` lifts to a unital
algebra homomorphism from the unitization into `C`. This is extended to an `Equiv` in
`Unitization.lift` and that should be used instead. This declaration only exists for performance
reasons.  -/
NonUnitalAlgHom.toAlgHom : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : SMulCommClass R A A] →
            [inst_4 : IsScalarTower R A A] →
              {C : Type u_5} → [inst_5 : Semiring C] → [inst_6 : Algebra R C] → (A →ₙₐ[R] C) → Unitization R A →ₐ[R] C
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.containsThenInsert_snd : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k},
  (m.containsThenInsert k v).2 = m.insert k v
-- Mathlib.Order.Ideal
Order.Ideal.isMaximal_iff : ∀ {P : Type u_1} [inst : LE P] (I : Order.Ideal P),
  I.IsMaximal ↔ I.IsProper ∧ ∀ ⦃J : Order.Ideal P⦄, I < J → ↑J = Set.univ
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.FinitaryExtensive C]
  {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inr
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.append_append : ∀ {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)},
  FreeAddGroup.Red L₁ L₃ → FreeAddGroup.Red L₂ L₄ → FreeAddGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.NonemptyCompacts.lipschitz_sup`. -/
EMetric.NonemptyCompacts.lipschitz_sup : ∀ {α : Type u_1} [inst : EMetricSpace α], LipschitzWith 1 fun p => p.1 ⊔ p.2
-- Mathlib.Order.Hom.WithTopBot
SupHom.withBot_id : ∀ {α : Type u_1} [inst : SemilatticeSup α], (SupHom.id α).withBot = SupBotHom.id (WithBot α)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- The continuous functional calculus commutes with integration.
This version assumes joint continuity of `f`, see `cfcₙ_setIntegral'` for a statement
with weaker assumptions.  -/
cfcₙ_setIntegral : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [CompleteSpace A] [inst_9 : NormedSpace ℝ A] [inst_10 : TopologicalSpace X] [OpensMeasurableSpace X] {s : Set X},
  MeasurableSet s →
    ∀ (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)],
      ContinuousOn (Function.uncurry f) (s ×ˢ quasispectrum 𝕜 a) →
        (∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0) →
          (∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
            MeasureTheory.HasFiniteIntegral bound (μ.restrict s) →
              autoParam (p a) cfcₙ_setIntegral._auto_1 →
                cfcₙ (fun r => ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfcₙ (f x) a ∂μ
-- Init.Data.SInt.Lemmas
Int32.cast_toNatClampNeg : ∀ (x : Int32), 0 ≤ x → ↑x.toNatClampNeg = x.toInt
-- Mathlib.RingTheory.Ideal.Colon
Submodule.mem_colon : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  {S : Set M} {r : R}, r ∈ N.colon S ↔ ∀ s ∈ S, r • s ∈ N
-- Init.Data.List.Lemmas
List.foldrM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β → β} {b : β}
  {l : List α}, List.foldrM (fun x1 x2 => pure (f x1 x2)) b l = pure (List.foldr f b l)
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.match_1.eq_2 : ∀ (motive : List String → Sort u_1) (a : String) (as : List String) (h_1 : Unit → motive [])
  (h_2 : (a : String) → (as : List String) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders.getBodyTerm? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.Order.Hom.Basic
OrderHom.coe_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), ↑f = f
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_neg : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (x : MonoidAlgebra R M), (-x).coeff = -x.coeff
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the second component element  -/
CategoryTheory.Limits.CategoricalPullback.snd : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} → CategoryTheory.Limits.CategoricalPullback F G → C
-- Mathlib.Algebra.Group.Even
/-- An element `a` of a type `α` with addition satisfies `Even a` if `a = r + r`,
for some `r : α`.  -/
Even : {α : Type u_2} → [Add α] → α → Prop
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Orbits in a `SubMulAction` coincide with orbits in the ambient space.  -/
SubMulAction.val_image_orbit : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : ↥p),
  Subtype.val '' MulAction.orbit R m = MulAction.orbit R ↑m
-- Mathlib.Algebra.Module.SnakeLemma
SnakeLemma.δ.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  {N₃ : Type u_7} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Function.Exact ⇑g₁ ⇑g₂)
  (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) (σ : M₃ → M₂) (hσ : ⇑f₂ ∘ σ = id) (ρ : N₂ → N₁)
  (hρ : ρ ∘ ⇑g₁ = id) {K₃ : Type u_9} {C₁ : Type u_10} [inst_13 : AddCommGroup K₃] [inst_14 : Module R K₃]
  [inst_15 : AddCommGroup C₁] [inst_16 : Module R C₁] (ι₃ : K₃ →ₗ[R] M₃) (hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
  (π₁ : N₁ →ₗ[R] C₁) (hπ₁ : Function.Exact ⇑i₁ ⇑π₁),
  SnakeLemma.δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ =
    { toFun := fun x => π₁ (ρ (i₂ ⋯)), map_add' := ⋯, map_smul' := ⋯ }
-- Batteries.Util.LibraryNote
/-- A library note is identified by the name of its declaration, and its content should be contained
in its doc-string.  -/
Batteries.Util.LibraryNote : Type
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.self_iff_bijective : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_5) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  IsFractionRing R R ↔ Function.Bijective ⇑(algebraMap R K)
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.willInsert : Lean.Widget.DiffTag
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (μ : CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPost F)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁ μ).app X₁).app X₂).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight ((μ.app X₁).app X₂) (F.obj X₃)
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₀_snd_assoc : ∀ (X : TopCat) {Z : TopCat} (h : TopCat.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp TopCat.ι₀
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X TopCat.I) h) =
    CategoryTheory.CategoryStruct.comp (TopCat.const 0) h
-- Mathlib.Tactic.Translate.Reorder
/-- `Reorder` represents a permutation of arguments and universe levels for translating
a given constant.  -/
Mathlib.Tactic.Translate.Reorder : Type
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_reflect : ∀ {δ : Type u_4} [inst : AddCommMonoid δ] (f : ℕ → δ) (k : ℕ) {m n : ℕ},
  m ≤ n + 1 → ∑ j ∈ Finset.Ico k m, f (n - j) = ∑ j ∈ Finset.Ico (n + 1 - m) (n + 1 - k), f j
-- Batteries.Lean.EStateM
EStateM.run'_modifyGet : ∀ {σ α ε : Type u_1} (f : σ → α × σ) (s : σ), (modifyGet f).run' s = some (f s).1
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.genLt.inj : ∀ {n n_1 : ℕ},
  Lean.Meta.Grind.EMatchTheoremConstraint.genLt n = Lean.Meta.Grind.EMatchTheoremConstraint.genLt n_1 → n = n_1
-- Mathlib.Data.Option.NAry
Option.mem_map₂_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} {c : γ},
  c ∈ Option.map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c
-- Lean.Meta.CongrTheorems
/-- Create a congruence theorem for `f`. The theorem is used in the simplifier.

If `subsingletonInstImplicitRhs = true`, the `rhs` corresponding to `[Decidable p]` parameters
is marked as instance implicit. It forces the simplifier to compute the new instance when applying
the congruence theorem.
For the `congr` tactic we set it to `false`.
 -/
Lean.Meta.mkCongrSimp? : Lean.Expr → optParam Bool true → optParam (Option ℕ) none → Lean.MetaM (Option Lean.Meta.CongrTheorem)
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_exists_orderOf_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G], IsPGroup p G ↔ ∃ k, ∀ (g : G), orderOf g ∣ p ^ k
-- Mathlib.Tactic.Translate.ToDual
/-- The global `do_translate`/`dont_translate` attributes specify whether operations on
a given type should be translated. `dont_translate` can be used for types that are translated,
such as `MonoidAlgebra` -> `AddMonoidAlgebra`, or for fixed types, such as `Fin n`/`ZMod n`.
`do_translate` is for types without arguments, like `Unit` and `Empty`, where the structure on it
can be translated.

Note: The name generation is not aware of `dont_translate`, so if some part of a lemma is not
  translated thanks to this, you generally have to specify the translated name manually.
 -/
Mathlib.Tactic.ToDual.doTranslateAttr : Lean.NameMapExtension Bool
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- Integrating `f` against `partialTraj κ a (a + 1)` is the same as integrating against `κ a`.  -/
ProbabilityTheory.Kernel.lmarginalPartialTraj_succ : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsSFiniteKernel (κ n)] (a : ℕ) {f : ((n : ℕ) → X n) → ENNReal},
  Measurable f →
    ∀ (x₀ : (n : ℕ) → X n),
      ProbabilityTheory.Kernel.lmarginalPartialTraj κ a (a + 1) f x₀ =
        ∫⁻ (x : X (a + 1)), f (Function.update x₀ (a + 1) x) ∂(κ a) (Preorder.frestrictLe a x₀)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encode_lt_comp : ∀ (cf cg : Nat.Partrec.Code),
  Encodable.encode cf < Encodable.encode (cf.comp cg) ∧ Encodable.encode cg < Encodable.encode (cf.comp cg)
-- Mathlib.Computability.Reduce
ManyOneDegree.of.eq_1 : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] (p : α → Prop),
  ManyOneDegree.of p = Quotient.mk'' (toNat p)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- The projection from `Y` to the explicit cokernel of `X ⟶ Y`.  -/
SemiNormedGrp.explicitCokernelπ : {X Y : SemiNormedGrp} → (f : X ⟶ Y) → Y ⟶ SemiNormedGrp.explicitCokernel f
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The seminorm is invariant under negation.  -/
NonarchAddGroupSeminorm.neg' : ∀ {G : Type u_6} [inst : AddGroup G] (self : NonarchAddGroupSeminorm G) (r : G), self.toFun (-r) = self.toFun r
-- Mathlib.Algebra.Order.Ring.Abs
pow_abs_two_mul : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] {n : ℕ} (a : α), |a| ^ (2 * n) = a ^ (2 * n)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instCoeSubgroup.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenNormalSubgroup.instCoeSubgroup = { coe := fun H => ↑H.toOpenSubgroup }
-- Init.Data.List.Attach
/-- This lemma identifies maps over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
List.map_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → β} {g : α → β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.map f l = List.map g l.unattach
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.of_separable_splitting_field_aux : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {p : Polynomial F}
  [hFE : FiniteDimensional F E] [sp : Polynomial.IsSplittingField F E p],
  p.Separable →
    ∀ (K : Type u_3) [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra K E] [inst_6 : IsScalarTower F K E]
      {x : E},
      x ∈ p.aroots E →
        Nat.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Nat.card (K →ₐ[F] E) * Module.finrank K ↥K⟮x⟯
-- Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Module.End.maxGenEigenspace.eq_1 : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R), f.maxGenEigenspace μ = (f.genEigenspace μ) ⊤
-- Mathlib.Order.Filter.Pointwise
Filter.addMonoid.eq_1 : ∀ {α : Type u_2} [inst : AddMonoid α],
  Filter.addMonoid =
    { toAdd := Filter.addZeroClass.toAdd, add_assoc := ⋯, toZero := Filter.addZeroClass.toZero, zero_add := ⋯,
      add_zero := ⋯, toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.Eval.Result.mk.inj : ∀ {expr : Mathlib.Tactic.BicategoryLike.NormalExpr} {proof : Lean.Expr}
  {expr_1 : Mathlib.Tactic.BicategoryLike.NormalExpr} {proof_1 : Lean.Expr},
  { expr := expr, proof := proof } = { expr := expr_1, proof := proof_1 } → expr = expr_1 ∧ proof = proof_1
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.instContinuousConstSMul : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (M : Type u_6) [inst_7 : Monoid M] [inst_8 : DistribMulAction M 𝕜] [inst_9 : SMulCommClass 𝕜 M 𝕜]
  [inst_10 : ContinuousConstSMul M 𝕜], ContinuousConstSMul M (WeakDual 𝕜 E)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.subset_extend : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : LinearIndepOn K id s), s ⊆ hs.extend ⋯
-- Init.GetElem
Array.instGetElem?NatLtSize : {α : Type u_1} → GetElem? (Array α) ℕ α fun xs i => i < xs.size
-- Init.Data.SInt.Lemmas
Int16.toBitVec_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toBitVec = OfNat.ofNat n
-- Lean.Elab.Tactic.Simp
/-- `simpLocation ctx discharge? varIdToLemmaId loc`
runs the simplifier at locations specified by `loc`,
using the simp theorems collected in `ctx`
optionally running a discharger specified in `discharge?` on generated subgoals.

Its primary use is as the implementation of the
`simp [...] at ...` and `simp only [...] at ...` syntaxes,
but can also be used by other tactics when a `Syntax` is not available.

For many tactics other than the simplifier,
one should use the `withLocation` tactic combinator
when working with a `location`.
 -/
Lean.Elab.Tactic.simpLocation : Lean.Meta.Simp.Context →
  Lean.Meta.Simp.SimprocsArray →
    optParam (Option Lean.Meta.Simp.Discharge) none →
      Lean.Elab.Tactic.Location → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Stats
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.emptyOn_ground : ∀ {α : Type u_1}, (Matroid.emptyOn α).E = ∅
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.chainSupCarrier.eq_1 : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (c : Set (ShrinkingLemma.PartialRefinement u s p)),
  ShrinkingLemma.PartialRefinement.chainSupCarrier c = ⋃ v ∈ c, v.carrier
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        k ∉ m₂ → Std.DTreeMap.Raw.Const.getD (m₁ \ m₂) k fallback = Std.DTreeMap.Raw.Const.getD m₁ k fallback