mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Complex.Basic
Complex.equivRealProdAddHom_symm_apply_re : ∀ (p : ℝ × ℝ), (Complex.equivRealProdAddHom.symm p).re = p.1
-- Std.Do.Triple.SpecLemmas
List.Cursor.pos_at : ∀ {α : Type u_1} {l : List α} {n : ℕ}, n < l.length → (List.Cursor.at l n).pos = n
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_iff_uncurry : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {T : Type v''} [inst_3 : TopologicalSpace T]
  [∀ (i : ι), LocallyCompactSpace (X i)] (g : Z → Topology.ContinuousMapGeneratedBy X Y T),
  Topology.ContinuousGeneratedBy X g ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : C(X i₁, Z)) ⦃i₂ : ι⦄ (f₂ : C(X i₂, Y)),
      Continuous fun x =>
        match x with
        | (x₁, x₂) => (g (f₁ x₁)) (f₂ x₂)
-- Mathlib.GroupTheory.Sylow
Sylow.normal_of_normalizer_normal : ∀ {G : Type u} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  (Subgroup.normalizer ↑P).Normal → (↑P).Normal
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.splitMany_le_split : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) {s : Finset (ι × ℝ)} {p : ι × ℝ},
  p ∈ s → BoxIntegral.Prepartition.splitMany I s ≤ BoxIntegral.Prepartition.split I p.1 p.2
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPPiBinderNamesHygienic : Lean.Options → Bool
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_range_diag_flip : ∀ {M : Type u_3} [inst : AddCommMonoid M] (n : ℕ) (f : ℕ → ℕ → M),
  ∑ m ∈ Finset.range n, ∑ k ∈ Finset.range (m + 1), f k (m - k) =
    ∑ m ∈ Finset.range n, ∑ k ∈ Finset.range (n - m), f m k
-- Init.Data.UInt.Lemmas
UInt64.zero_add : ∀ (a : UInt64), 0 + a = a
-- Mathlib.Algebra.Algebra.Operations
/-- `1 : Submodule R A` is the submodule `R ∙ 1` of `A`.
 -/
Submodule.one : {R : Type u} → [inst : Semiring R] → {A : Type v} → [inst_1 : Semiring A] → [inst_2 : Module R A] → One (Submodule R A)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec : ∀ (R S : CommRingCatᵒᵖ), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison AlgebraicGeometry.Scheme.Spec R S)
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.Std.Iter.intercalateString.match_1.splitter : (motive : Option String → String → Sort u_1) →
  (x : Option String) →
    (x_1 : String) → ((sl : String) → motive none sl) → ((str sl : String) → motive (some str) sl) → motive x x_1
-- Mathlib.Algebra.Lie.Basic
LieRingModule.toEnd_apply_apply : ∀ (L : Type v) (M : Type w) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m : M),
  ((LieRingModule.toEnd L M) x) m = ⁅x, m⁆
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
DiscreteUniformity.mk : ∀ {X : Type u_1} [u : UniformSpace X], u = ⊥ → DiscreteUniformity X
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.normForwardRule.sizeOf_spec : ∀ (r₁ : Aesop.ForwardRule) (r₂ : Aesop.NormRule),
  sizeOf (Aesop.BaseRuleSetMember.normForwardRule r₁ r₂) = 1 + sizeOf r₁ + sizeOf r₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_zero : ∀ (x : ℂ), x ^ 0 = 1
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.other.injEq : ∀ (message message_1 : String),
  (Std.Http.Protocol.H1.Error.other message = Std.Http.Protocol.H1.Error.other message_1) = (message = message_1)
-- Mathlib.RepresentationTheory.Basic
/-- The representation on `α →₀ A` defined pointwise by a representation on `A`.  -/
Representation.finsupp : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommSemiring k] →
      [inst_1 : Monoid G] →
        {A : Type u_4} →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : Module k A] → Representation k G A → (α : Type u_6) → Representation k G (α →₀ A)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {km : α}, t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.root_right_of_root_gcd : ∀ {R : Type u} {k : Type y} [inst : Field R] [inst_1 : CommSemiring k] [inst_2 : DecidableEq R] {ϕ : R →+* k}
  {f g : Polynomial R} {α : k}, Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0 → Polynomial.eval₂ ϕ α g = 0
-- Mathlib.Data.Stream.Init
Stream'.get_map : ∀ {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (s : Stream' α), (Stream'.map f s).get n = f (s.get n)
-- Init.Data.Char.Lemmas
Char.toString_eq_singleton : ∀ {c : Char}, c.toString = String.singleton c
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- All the `Ideal.ramificationIdx` over a fixed maximal ideal are the same.  -/
Ideal.ramificationIdx_eq_of_isGaloisGroup : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (P Q : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] [hQp : Q.IsPrime] [Q.LiesOver p] (G : Type u_3)
  [inst_4 : Group G] [Finite G] [inst_6 : MulSemiringAction G B] [IsGaloisGroup G A B],
  P.ramificationIdx A = Q.ramificationIdx A
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.isAffineMap : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  (f : Convexity.ConvexSpace.AffineMap R X Y), Convexity.IsAffineMap R ⇑f
-- Mathlib.Data.Set.Card
Set.finite_iff_finite_of_encard_eq_encard : ∀ {α : Type u_1} {s t : Set α}, s.encard = t.encard → (s.Finite ↔ t.Finite)
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- If `f` and `g` are Lipschitz on `s`, so is the induced map `f × g` to the product type.  -/
LipschitzOnWith.prodMk : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {s : Set α} {f : α → β} {g : α → γ} {Kf Kg : NNReal},
  LipschitzOnWith Kf f s → LipschitzOnWith Kg g s → LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s
-- Lean.Elab.Coinductive
/-- Ref from the original `InductiveView` -/
Lean.Elab.Command.CoinductiveElabData.ref : Lean.Elab.Command.CoinductiveElabData → Lean.Syntax
-- Lean.Meta.Hint
/-- A widget for rendering code action suggestions in error messages. Generally, this widget should not
be used directly; instead, use `MessageData.hint`. Note that this widget is intended only for use
within message data; it may not display line breaks properly if rendered as a panel widget.

The props to this widget are of the following form:
```json
{
  "diff": [
    {"type": "unchanged", "text": "h"},
    {"type": "deletion", "text": "ello"},
    {"type": "insertion", "text": "i"}
  ],
  "suggestion": "hi",
  "range": {
    "start": {"line": 100, "character": 0},
    "end":   {"line": 100, "character": 5}
  }
}
```

Note: we cannot add the `builtin_widget_module` attribute here because that would require importing
`Lean.Widget.UserWidget`, which in turn imports much of `Lean.Elab` -- the module where we want to
be able to use this widget. Instead, we register the attribute post-hoc when we declare the regular
"Try This" widget in `Lean.Meta.Tactic.TryThis`.
 -/
Lean.Meta.Hint.tryThisDiffWidget : Lean.Widget.Module
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Range.mk.sizeOf_spec : ∀ (start «end» : Lean.Lsp.Position), sizeOf { start := start, «end» := «end» } = 1 + sizeOf start + sizeOf «end»
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.coe_iSup_apply : ∀ {E : Type u_3} [inst : AddGroup E] {ι : Type u_6} (f : ι → NonarchAddGroupSeminorm E),
  BddAbove (Set.range f) → ∀ {x : E}, (⨆ i, f i) x = ⨆ i, (f i) x
-- Mathlib.Order.Interval.Set.Image
Monotone.mapsTo_Icc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  Monotone f → Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFrameAndOfSimpAnd_1 : ∀ {φ : Prop} (σs : List (Type u_1)) (P P' Q' PQ : Std.Do.SPred σs) [Std.Do.SPred.Tactic.HasFrame P' Q' φ]
  [Std.Do.SPred.Tactic.SimpAnd P Q' PQ], Std.Do.SPred.Tactic.HasFrame spred(P ∧ P') PQ φ
-- Mathlib.RingTheory.SimpleModule.Basic
instIsSemisimpleModuleOfIsSimpleModule : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M],
  IsSemisimpleModule R M
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.SymmetricCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [toBraidedCategory : CategoryTheory.BraidedCategory C] →
        autoParam
            (∀ (X Y : C),
              CategoryTheory.CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom =
                CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
            CategoryTheory.SymmetricCategory.symmetry._autoParam →
          CategoryTheory.SymmetricCategory C
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.forall_mem_sup : ∀ {C : Type u_2} [inst : AddCommGroup C] {s t : AddSubgroup C} {P : C → Prop},
  (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ + x₂)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_eq_of_dvd_sub : ∀ {R : Type u} [inst : CommRing R] {p₁ p₂ q : Polynomial R}, q.Monic → q ∣ p₁ - p₂ → p₁ %ₘ q = p₂ %ₘ q
-- Init.Data.String.Decode
Char.utf8Size_eq_one_iff : ∀ {c : Char}, c.utf8Size = 1 ↔ c.val ≤ 127
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSort.State.mk : Std.HashSet Lean.Expr → Std.HashSet Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.TopSort.State
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_smul : ∀ {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {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₂} [inst_6 : DistribSMul S M₂] [inst_7 : SMulCommClass R₂ S M₂] (a : S)
  (f : M →ₛₗ[σ₁₂] M₂), ⇑(a • f) = a • ⇑f
-- Mathlib.LinearAlgebra.Complex.Module
Complex.equivRealProdLm_symm_apply_im : ∀ (a : ℝ × ℝ), (Complex.equivRealProdLm.symm a).im = a.2
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M M' : CategoryTheory.Functor C MonCat} (p p_1 : M ⟶ M')
  (e_p : p = p_1) (S' : CategoryTheory.SubmonoidFunctor M') (hp : CategoryTheory.SubmonoidFunctor.image p ⊤ ≤ S'),
  CategoryTheory.SubmonoidFunctor.lift p S' hp = CategoryTheory.SubmonoidFunctor.lift p_1 S' ⋯
-- Mathlib.Algebra.Exact.Basic
Function.Exact.of_ladder_linearEquiv_of_exact : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {N' : Type u_5} {P : Type u_6} {P' : Type u_7}
  [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid N'] [inst_5 : AddCommMonoid P] [inst_6 : AddCommMonoid P'] [inst_7 : Module R M]
  [inst_8 : Module R M'] [inst_9 : Module R N] [inst_10 : Module R N'] [inst_11 : Module R P] [inst_12 : Module R P']
  {f₁₂ : M →ₗ[R] N} {f₂₃ : N →ₗ[R] P} {g₁₂ : M' →ₗ[R] N'} {g₂₃ : N' →ₗ[R] P'} {e₁ : M ≃ₗ[R] M'} {e₂ : N ≃ₗ[R] N'}
  {e₃ : P ≃ₗ[R] P'},
  g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂ → g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃ → Function.Exact ⇑f₁₂ ⇑f₂₃ → Function.Exact ⇑g₁₂ ⇑g₂₃
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν), ν h.nullSetᶜ = 0
-- Mathlib.Topology.Algebra.Group.Basic
Topology.IsClosedEmbedding.units_map : ∀ {α : Type u} {β : Type v} [inst : Monoid α] [inst_1 : TopologicalSpace α] [inst_2 : Monoid β]
  [inst_3 : TopologicalSpace β] [ContinuousMul α] [T1Space α] {f : α →* β},
  Topology.IsClosedEmbedding ⇑f → Topology.IsClosedEmbedding ⇑(Units.map f)
-- Mathlib.RingTheory.KrullDimension.Regular
/-- If `r` is a nonzerodivisor contained in an ideal of maximal height,
`dim (R / (r)) + 1 = dim R`.  -/
Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {r : R},
  r ∈ nonZeroDivisors R →
    ∀ {p : Ideal R} [p.IsPrime],
      ↑p.height = ringKrullDim R → r ∈ p → ringKrullDim (R ⧸ Ideal.span {r}) + 1 = ringKrullDim R
-- Mathlib.Topology.Compactness.CountablyCompact
isSeqCompact_iff_seqCompactSpace : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E}, IsSeqCompact A ↔ SeqCompactSpace ↑A
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.instInhabitedAlgebra : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (T : CategoryTheory.Monad C) → [Inhabited C] → Inhabited T.Algebra
-- Mathlib.Data.Nat.Factorization.Defs
Nat.prod_factorization_pow_eq_self : ∀ {n : ℕ}, n ≠ 0 → (n.factorization.prod fun x1 x2 => x1 ^ x2) = n
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] (abv : β → α) [inst_4 : IsAbsoluteValue abv] (x x_1 : β),
  x = x_1 → CauSeq.const abv x = CauSeq.const abv x_1
-- Mathlib.Data.Sym.Basic
/-- The nth symmetric power is n-tuples up to permutation.  We define it
as a subtype of `Multiset` since these are well developed in the
library.  We also give a definition `Sym.sym'` in terms of vectors, and we
show these are equivalent in `Sym.symEquivSym'`.
 -/
Sym : Type u_1 → ℕ → Type (max 0 u_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termI₃_1 : Lean.ParserDescr
-- Mathlib.Order.RelSeries
/-- Adjacent elements are related  -/
RelSeries.step : ∀ {α : Type u_1} {r : SetRel α α} (self : RelSeries r) (i : Fin self.length),
  (self.toFun i.castSucc, self.toFun i.succ) ∈ r
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_eq : ∀ {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₃ : ι₃) (i₁₂ : ι₁₂) (j : ι₄)
  (h₁₂ : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) (h : c₁₂.π c₃ c₄ (i₁₂, i₃) = j),
  HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j ⋯ =
    CategoryTheory.CategoryStruct.comp ((G.map ⋯).app (K₃.X i₃))
      ((K₁.mapBifunctor K₂ F₁₂ c₁₂).ιMapBifunctor K₃ G c₄ i₁₂ i₃ j h)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.pi_top : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] (I : Set ι), (Submonoid.pi I fun i => ⊤) = ⊤
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Debug `lia` by identifying places where it does not yet supersede `omega`.  -/
omegaToLiaRegressions : Mathlib.TacticAnalysis.Config
-- Mathlib.Logic.Equiv.Defs
Equiv.Perm.ext : ∀ {α : Sort u} {σ τ : Equiv.Perm α}, (∀ (x : α), σ x = τ x) → σ = τ
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- A useful strengthening of being antitone is to require that each set contains
the closure of each of its children.  -/
CantorScheme.ClosureAntitone : {β : Type u_1} → {α : Type u_2} → (List β → Set α) → [TopologicalSpace α] → Prop
-- Init.Data.List.Monadic
List.foldrM_filterMap : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  {f : α → Option β} {g : β → γ → m γ} {l : List α} {init : γ},
  List.foldrM g init (List.filterMap f l) =
    List.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init l
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] {a : α} {c : ℕ},
  (Std.HashMap.Raw.emptyWithCapacity c).getKey! a = default
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.comp_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {M : CategoryTheory.Functor C D}
  (f : F.HomObj G A) (g : G.HomObj M A) (X : C) (a : A.obj X),
  (f.comp g).app X a = CategoryTheory.CategoryStruct.comp (f.app X a) (g.app X a)
-- Init.Data.Vector.Lemmas
Vector.exists_of_mem_flatMap : ∀ {β : Type u_1} {α : Type u_2} {n m : ℕ} {b : β} {xs : Vector α n} {f : α → Vector β m},
  b ∈ xs.flatMap f → ∃ a ∈ xs, b ∈ f a
-- Mathlib.Topology.NhdsSet
nhds_le_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {x : X}, x ∈ s → nhds x ≤ nhdsSet s
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.spanning_iff_compl_coindep : ∀ {α : Type u_2} {M : Matroid α} {S : Set α},
  autoParam (S ⊆ M.E) Matroid.spanning_iff_compl_coindep._auto_1 → (M.Spanning S ↔ M.Coindep (M.E \ S))
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero : ∀ {K : Type u_1} [inst : Field K] {x : (NumberField.RingOfIntegers K)ˣ} {w : NumberField.InfinitePlace K},
  ↑w.mult * Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x)) = 0 ↔
    w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x) = 1
-- Init.Data.List.Perm
List.Perm.length_eq : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₁.length = l₂.length
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- the second projection  -/
CategoryTheory.Limits.ChosenPullback.p₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} →
      {f₁ : X₁ ⟶ S} → {f₂ : X₂ ⟶ S} → (self : CategoryTheory.Limits.ChosenPullback f₁ f₂) → self.pullback ⟶ X₂
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.prop_cokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderCokernels] {X Y : C} (f : X ⟶ Y)
  [inst_3 : CategoryTheory.Limits.HasCokernel f], P X → P Y → P (CategoryTheory.Limits.cokernel f)
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `VAdd` across an `Equiv`  -/
Equiv.vadd : (M : Type u_1) → {α : Type u_2} → {β : Type u_3} → α ≃ β → [VAdd M β] → VAdd M α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.homologyι =
    CategoryTheory.CategoryStruct.comp S₁.homologyι (CategoryTheory.ShortComplex.opcyclesMap φ)
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.warning : Lean.Lsp.MessageType
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_mul_units_right : ∀ {R : Type u_1} [inst : CommSemiring R] {u v : R},
  IsUnit u → IsUnit v → ∀ (y z : R), IsCoprime (y * u) (z * v) ↔ IsCoprime y z
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxi.Iterator.toList_eq_match : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {it : Std.Iter α},
  it.toList =
    match it.internalState.next with
    | none => []
    | some a => a :: { internalState := { next := Std.PRange.succ? a } }.toList
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.reflTransSymmAux_mem_I : ∀ (x : ↑unitInterval × ↑unitInterval), Path.Homotopy.reflTransSymmAux x ∈ unitInterval
-- Mathlib.Order.Defs.Unbundled
IsStrictOrder.toIsTrans : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsStrictOrder α r], IsTrans α r
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.symm_comp_rid_symm_assoc : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  ↑(TensorProduct.comm R M' R) ∘ₗ ↑(TensorProduct.rid R M').symm ∘ₗ f = ↑(TensorProduct.lid R M').symm ∘ₗ f
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_of_countable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [Countable α]
  [MeasurableSingletonClass α] (f : α → β), Measurable f
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.addAction_faithful : ∀ {α : Type u_2} [inst : DecidableEq α] {G : Type u_3} [inst_1 : AddGroup G] [inst_2 : AddAction G α] {n : ℕ},
  1 ≤ n → ↑n < ENat.card α → ∀ {g : G}, AddAction.toPerm g = 1 ↔ AddAction.toPerm g = 1
-- Mathlib.Data.Set.Function
Set.mapsTo_id : ∀ {α : Type u_1} (s : Set α), Set.MapsTo id s s
-- Init.Data.List.Impl
/-- Auxiliary for `takeWhile`: `takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs`,
unless no element satisfying `p` is found in `xs` in which case it returns `l`.  -/
_private.Init.Data.List.Impl.0.List.takeWhileTR.go : {α : Type u_1} → (α → Bool) → List α → List α → Array α → List α
-- Mathlib.FieldTheory.Separable
/-- In a field `F`, `X ^ n - 1` is separable iff `↑n ≠ 0`.  -/
Polynomial.X_pow_sub_one_separable_iff : ∀ {F : Type u} [inst : Field F] {n : ℕ}, (Polynomial.X ^ n - 1).Separable ↔ ↑n ≠ 0
-- Mathlib.Data.Complex.Basic
Complex.ofReal_comp_pow : ∀ {α : Type u_1} (f : α → ℝ) (n : ℕ), Complex.ofReal ∘ (f ^ n) = Complex.ofReal ∘ f ^ n
-- Std.Time.Date.Unit.Week
/-- Convert `Week.Offset` into `Hour.Offset`.
 -/
Std.Time.Week.Offset.toHours : Std.Time.Week.Offset → Std.Time.Hour.Offset
-- Mathlib.Data.List.Basic
List.forall_iff_forall_mem : ∀ {α : Type u} {p : α → Prop} {l : List α}, List.Forall p l ↔ ∀ x ∈ l, p x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The identity lax transformation.  -/
CategoryTheory.Lax.LaxTrans.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → (F : CategoryTheory.LaxFunctor B C) → CategoryTheory.Lax.LaxTrans F F
-- Mathlib.Algebra.Opposites
PreOpposite.op'.inj : ∀ {α : Type u_3} {unop' unop'_1 : α}, { unop' := unop' } = { unop' := unop'_1 } → unop' = unop'_1
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.mk : Lean.TSyntax `Lean.Parser.Command.declModifiers →
  Option (Lean.TSyntax `Lean.Parser.Command.docComment) →
    Lean.Elab.Visibility →
      Bool → Lean.Elab.ComputeKind → Lean.Elab.RecKind → Bool → Array Lean.Elab.Attribute → Lean.Elab.Modifiers