mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_comp_subst : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] {υ : Type u_5} {T : Type u_6}
  [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] {a : PowerSeries S}
  {b : MvPowerSeries υ T} [IsScalarTower R S T],
  PowerSeries.HasSubst a →
    PowerSeries.HasSubst b → PowerSeries.subst b ∘ PowerSeries.subst a = PowerSeries.subst (PowerSeries.subst b a)
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- Any set `S` inside a monoid with a single unit contains the irreducible elements of the
submonoid it generates.  -/
irreducible_mem_submonoidClosure_subset : ∀ {M : Type u_1} [inst : CommMonoid M] [Subsingleton Mˣ] {S : Set M}, {p | p ∈ Submonoid.closure S ∧ Irreducible p} ⊆ S
-- Lean.Parser.Term
/-- A configuration item.  -/
Lean.Parser.Term.configItem : Lean.Parser.Parser
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- If `a` is an integer, then the coefficient sequence of its continued fraction is empty.
 -/
GenContFract.of_s_of_int : ∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K]
  (a : ℤ), (GenContFract.of ↑a).s = Stream'.Seq.nil
-- Mathlib.CategoryTheory.Skeletal
/-- The category `D` has isomorphic objects equal  -/
CategoryTheory.IsSkeletonOf.skel : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor D C}, CategoryTheory.IsSkeletonOf C D F → CategoryTheory.Skeletal D
-- Init.Data.Vector.Nat
Vector.sum_replicate_nat : ∀ {n a : ℕ}, (Vector.replicate n a).sum = n * a
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.mvars : Lean.Option Bool
-- Mathlib.Topology.Inseparable
specializingMap_iff_closure_singleton_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  SpecializingMap f ↔ ∀ (x : X), closure {f x} ⊆ f '' closure {x}
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toArray_insert_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : BEq α]
  [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (Std.DTreeMap.Raw.Const.toArray (t.insert k v)).Perm
        ((Array.filter (fun x => decide ¬(k == x.1) = true) (Std.DTreeMap.Raw.Const.toArray t)).push (k, v))
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.LeftRigidCategory.leftDual : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.LeftRigidCategory C] → (X : C) → CategoryTheory.HasLeftDual X
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : SizeOf α] (carrier : Set α)
  (isIrreducible' : IsIrreducible carrier) (isClosed' : IsClosed carrier),
  sizeOf { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' } =
    1 + sizeOf isIrreducible' + sizeOf isClosed'
-- Std.Data.HashMap.Lemmas
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `getElem_insertIfNew`.  -/
Std.HashMap.contains_of_contains_insertIfNew' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β},
  (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.Data.Set.Prod
Set.offDiag_eq_empty : ∀ {α : Type u_1} {s : Set α}, s.offDiag = ∅ ↔ s.Subsingleton
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Set.instMeasurableSingletonClass : ∀ {α : Type u_1} [Countable α], MeasurableSingletonClass (Set α)
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The `CommRing` instance for matrix entries  -/
Mathlib.Tactic.Determinant.ReifiedBirdDet.rα : (self : Mathlib.Tactic.Determinant.ReifiedBirdDet) → Q(CommRing unknown_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasColimit_of_domain_hasInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasInitial J] {F : CategoryTheory.Functor J C}
  [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)], CategoryTheory.Limits.HasColimit F
-- Init.Data.Rat.Lemmas
Rat.zpow_zero : ∀ (q : ℚ), q ^ 0 = 1
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.eraseMany : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type u_1} [inst_1 : ForIn Id ρ α]
  {t : Std.DTreeMap.Internal.Impl α β} {l : ρ} {h : t.Balanced}, t.WF → (↑(t.eraseMany l h)).WF
-- Mathlib.Tactic.Order.Preprocessing
/-- Supported order types: linear, partial, and preorder.  -/
Mathlib.Tactic.Order.OrderType : Type
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instReprMatcherInfo : Repr Lean.Meta.MatcherInfo
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeft_obj_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeft R l hl).obj X).hom =
    CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom
-- Init.Data.List.Basic
List.findIdx_nil : ∀ {α : Type u} {p : α → Bool}, List.findIdx p [] = 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Reinterpreting an `F`-structured arrow `X ⟶ F.obj d` as an arrow under `X` induces a functor
`StructuredArrow X F ⥤ Under X`.  -/
CategoryTheory.StructuredArrow.toUnder : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (X : T) →
          (F : CategoryTheory.Functor D T) →
            CategoryTheory.Functor (CategoryTheory.StructuredArrow X F) (CategoryTheory.Under X)
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.tensorHom_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable]
  {X₁ Y₁ X₂ Y₂ : CategoryTheory.WideSubcategory P} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.isClassified_of_normalize_isPrimitiveClassified : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z), ⋯.IsPrimitiveClassified → h.IsClassified
-- Mathlib.Data.List.Sort
List.SortedLT.eq_of_mem_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α},
  l₁.SortedLT → l₂.SortedLT → (∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) → l₁ = l₂
-- Mathlib.NumberTheory.ModularForms.DedekindEta
_private.Mathlib.NumberTheory.ModularForms.DedekindEta.0.term𝕢 : Lean.ParserDescr
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_toEquiv : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), ⇑e.toEquiv = ⇑e
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, a ∉ t → t.getKeyD a fallback = fallback
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] [inst_4 : SizeOf R] [inst_5 : SizeOf S] [inst_6 : SizeOf ι] [inst_7 : SizeOf σ]
  (toPreSubmersivePresentation : Algebra.PreSubmersivePresentation R S ι σ)
  (jacobian_isUnit : IsUnit toPreSubmersivePresentation.jacobian),
  sizeOf { toPreSubmersivePresentation := toPreSubmersivePresentation, jacobian_isUnit := jacobian_isUnit } =
    1 + sizeOf toPreSubmersivePresentation + sizeOf jacobian_isUnit
-- Mathlib.Order.Monotone.Defs
StrictAnti.antitone : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β}, StrictAnti f → Antitone f
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀]
  (x : MvPolynomial ι R₀),
  (P.tensorModelOfHasCoeffsInv R₀) ((MvPolynomial.aeval P.val) x) =
    1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀)))) x
-- Init.Data.Option.Lemmas
Option.mem_some_self : ∀ {α : Type u_1} (a : α), a ∈ some a
-- Lean.Meta.Sym.Canon
/-- See comments at `ShouldCanonResult`.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.shouldCanon : Array Lean.Meta.ParamInfo → ℕ → Lean.Expr → Lean.MetaM Lean.Meta.Sym.Canon.ShouldCanonResult✝
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_eq_foldr : ∀ {α : Type u_1} [inst : Semiring α] (b : α) (L : List ℕ), Nat.ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.default_def : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂}, default = 0
-- Mathlib.CategoryTheory.EqToHom
/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`.  -/
CategoryTheory.eqToHom_iso_hom_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b)
  {j j' : β} (w : j = j'),
  CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').hom
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.mk : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (pt : C) →
          (fst : pt ⟶ P) →
            (snd : pt ⟶ Q) →
              (inl : P ⟶ pt) →
                (inr : Q ⟶ pt) →
                  autoParam (CategoryTheory.CategoryStruct.comp inl fst = CategoryTheory.CategoryStruct.id P)
                      CategoryTheory.Limits.BinaryBicone.inl_fst._autoParam →
                    autoParam (CategoryTheory.CategoryStruct.comp inl snd = 0)
                        CategoryTheory.Limits.BinaryBicone.inl_snd._autoParam →
                      autoParam (CategoryTheory.CategoryStruct.comp inr fst = 0)
                          CategoryTheory.Limits.BinaryBicone.inr_fst._autoParam →
                        autoParam (CategoryTheory.CategoryStruct.comp inr snd = CategoryTheory.CategoryStruct.id Q)
                            CategoryTheory.Limits.BinaryBicone.inr_snd._autoParam →
                          CategoryTheory.Limits.BinaryBicone P Q
-- Mathlib.Algebra.Module.NatInt
instMulActionNatOfAddMonoid : {M : Type u_3} → [AddMonoid M] → MulAction ℕ M
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.containsThenInsert_snd : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α}, (m.containsThenInsert k).2 = m.insert k
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_subset_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ⊆ Set.Ioi b ↔ b < a
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `UniqueAdd` is preserved under additive maps that are injective.

See `UniqueAdd.addHom_map_iff` for a version with swapped bundling.  -/
UniqueAdd.addHom_image_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {A B : Finset G} {a0 b0 : G} [inst_2 : DecidableEq H]
  (f : G →ₙ+ H),
  Function.Injective ⇑f → (UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) ↔ UniqueAdd A B a0 b0)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.lt_iff_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {x y : R}, v₁ x < v₁ y ↔ v₂ x < v₂ y
-- Init.Tactics
/-- `expose_names` renames all inaccessible variables with accessible names, making them available
for reference in generated tactics. However, this renaming introduces machine-generated names
that are not fully under user control. `expose_names` is primarily intended as a preamble for
auto-generated end-game tactic scripts. It is also useful as an alternative to
`set_option tactic.hygienic false`. If explicit control over renaming is needed in the
middle of a tactic script, consider using structured tactic scripts with
`match .. with`, `induction .. with`, or `intro` with explicit user-defined names,
as well as tactics such as `next`, `case`, and `rename_i`.
 -/
Lean.Parser.Tactic.exposeNames : Lean.ParserDescr
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_eq_get_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅},
  t.max he = t.max?.get ⋯
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.ι_comp_colimitOpIsoOpLimit_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.op j)
      (CategoryTheory.Limits.colimitOpIsoOpLimit F).hom =
    (CategoryTheory.Limits.limit.π F (Opposite.unop j)).op
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.instNonempty : ∀ {α : Type u_1} [Nonempty α], Nonempty (Topology.WithLowerSet α)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.instGradedFunLikeSubmodule : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  GradedFunLike (𝒜 →ₐᵍ[R] ℬ) 𝒜 ℬ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ \ m₂).getKeyD k fallback = if k ∈ m₂ then fallback else m₁.getKeyD k fallback
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_sdiff`.

---

This is the same as `ncard_sdiff'` but we require `s` to be finite instead.  -/
Set.ncard_diff : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → autoParam s.Finite Set.ncard_sdiff._auto_1 → (t \ s).ncard = t.ncard - s.ncard
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.mk.inj : ∀ {R : Type u} {S : Type v} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} {Ring : Type w}
  {commRing : CommRing Ring} {algebra₁ : Algebra R Ring} {algebra₂ : Algebra Ring S}
  {isScalarTower : IsScalarTower R Ring S} {σ : S → Ring} {algebraMap_σ : ∀ (x : S), (algebraMap Ring S) (σ x) = x}
  {Ring_1 : Type w} {commRing_1 : CommRing Ring_1} {algebra₁_1 : Algebra R Ring_1} {algebra₂_1 : Algebra Ring_1 S}
  {isScalarTower_1 : IsScalarTower R Ring_1 S} {σ_1 : S → Ring_1}
  {algebraMap_σ_1 : ∀ (x : S), (algebraMap Ring_1 S) (σ_1 x) = x},
  { Ring := Ring, commRing := commRing, algebra₁ := algebra₁, algebra₂ := algebra₂, isScalarTower := isScalarTower,
        σ := σ, algebraMap_σ := algebraMap_σ } =
      { Ring := Ring_1, commRing := commRing_1, algebra₁ := algebra₁_1, algebra₂ := algebra₂_1,
        isScalarTower := isScalarTower_1, σ := σ_1, algebraMap_σ := algebraMap_σ_1 } →
    Ring = Ring_1 ∧ commRing ≍ commRing_1 ∧ algebra₁ ≍ algebra₁_1 ∧ algebra₂ ≍ algebra₂_1 ∧ σ ≍ σ_1
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_iff : ∀ (𝕜 : Type u_1) {α : Type u_2} {E : Type u_3} {F : Type u_4} [inst : ENorm 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : TopologicalSpace F] [inst_3 : Zero E] [inst_4 : Zero F] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 F]
  (l : Filter α) (f : α → E) (g : α → F),
  f =O[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => egauge 𝕜 V (g x)
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.Model.revMatchAt?.eq_def : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} (endPos : s.Pos),
  String.Slice.Pattern.Model.revMatchAt? pat endPos =
    if h : ∃ startPos, String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos then some h.choose else none
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).size = if t.contains k = true then t.size else t.size + 1
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_indep_iff_exists : ∀ {α : Type u_1} {M : Matroid α} {I : Set α},
  autoParam (I ⊆ M.E) Matroid.dual_indep_iff_exists._auto_1 → (M✶.Indep I ↔ ∃ B, M.IsBase B ∧ Disjoint I B)
-- Init.Tactics
/-- Apply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ f as ≍ f bs`.
The optional parameter is the depth of the recursive applications.
This is useful when `congr` is too aggressive in breaking down the goal.
For example, given `⊢ f (g (x + y)) = f (g (y + x))`,
`congr` produces the goals `⊢ x = y` and `⊢ y = x`,
while `congr 2` produces the intended `⊢ x + y = y + x`.
 -/
Lean.Parser.Tactic.congr : Lean.ParserDescr
-- Batteries.Data.Array.Match
/-- Make prefix table from a pattern array  -/
Array.mkPrefixTable : {α : Type u_1} → [BEq α] → Array α → Array.PrefixTable α
-- Mathlib.Algebra.Group.Defs
IsCancelMul.toIsRightCancelMul : ∀ {G : Type u} {inst : Mul G} [self : IsCancelMul G], IsRightCancelMul G
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- `FreeAbelianGroup.of` is a `MonoidHom` when `α` is a `Monoid`.  -/
FreeAbelianGroup.ofMulHom : {α : Type u} → [inst : Monoid α] → α →* FreeAbelianGroup α
-- Mathlib.NumberTheory.ModularForms.Bounds
ModularGroup.exists_bound_fundamental_domain_of_isBigO : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    ∀ {t : ℝ}, (f =O[UpperHalfPlane.atImInfty] fun z => z.im ^ t) → ∃ F, ∀ τ ∈ ModularGroup.fd, ‖f τ‖ ≤ F * τ.im ^ t
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.hasZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → {P : C} → Zero (CategoryTheory.Abelian.Pseudoelement P)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_coe : ∀ (r : NNReal), ⌈↑r⌉ₑ = ↑⌈r⌉₊
-- Lean.Meta.Tactic.Grind.Action
/-- Executes `x`, but behaves like a `skip` if it is not applicable.
 -/
Lean.Meta.Grind.Action.skipIfNA : Lean.Meta.Grind.Action → Lean.Meta.Grind.Action
-- Mathlib.Order.Heyting.Hom
HeytingHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] {f g : HeytingHom α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insert! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {fallback v : β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.insert! k v t) a fallback =
        if compare k a = Ordering.eq then v else Std.DTreeMap.Internal.Impl.Const.getD t a fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.instCoeTypeForall_2 : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- When a vector is in `Kᗮ`, with the inner product the
other way round.  -/
Submodule.mem_orthogonal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) (v : E), v ∈ Kᗮ ↔ ∀ u ∈ K, inner 𝕜 v u = 0
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqPublishDiagnosticsParams : BEq Lean.Lsp.PublishDiagnosticsParams
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasPluralDefaults : Sort u_1 → Sort (max 1 u_1)
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_apply_of_squarefree : ∀ {n : ℕ}, Squarefree n → ArithmeticFunction.moebius n = (-1) ^ ArithmeticFunction.cardFactors n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.filterMap_equiv_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {f : (a : α) → β a → Bool},
  t.WF → (Std.DTreeMap.Raw.filterMap (fun k => Option.guard fun v => f k v) t).Equiv (Std.DTreeMap.Raw.filter f t)
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.ofMapAddNeg.eq_1 : ∀ {G : Type u_5} [inst : AddGroup G] {H : Type u_8} [inst_1 : AddGroup H] (f : G → H)
  (map_div : ∀ (a b : G), f (a + -b) = f a + -f b), AddMonoidHom.ofMapAddNeg f map_div = AddMonoidHom.mk' f ⋯
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.MonicDegreeEq.freeMonic_coe : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ), ↑(Polynomial.MonicDegreeEq.freeMonic R n) = Polynomial.freeMonic R n
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U)
  (V : TopologicalSpace.Opens ↑Y) (hV : U ≤ (TopologicalSpace.Opens.map f).obj V),
  CategoryTheory.CategoryStruct.comp
      (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op V))
      (CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op)
        (TopCat.Presheaf.germToPullbackStalk C f F U x hx)) =
    F.germ V ((CategoryTheory.ConcreteCategory.hom f) x) ⋯
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.permutationsAux.rec.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (is : List α) (h_1 : (is : List α) → motive [] is)
  (h_2 : (t : α) → (ts is : List α) → motive (t :: ts) is),
  (match [], is with
    | [], is => h_1 is
    | t :: ts, is => h_2 t ts is) =
    h_1 is
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toList_eq_nil_iff : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], r.toList = [] ↔ ¬r.lower < r.upper
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.order.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] (x : HahnSeries Γ R),
  x.order = if h : x = 0 then 0 else ⋯.min ⋯