mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Heyting.Basic
/-- Pullback a `HeytingAlgebra` along an injection.  -/
Function.Injective.heytingAlgebra : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : Top α] →
              [inst_5 : Bot α] →
                [inst_6 : Compl α] →
                  [inst_7 : HImp α] →
                    [inst_8 : HeytingAlgebra β] →
                      (f : α → β) →
                        Function.Injective f →
                          (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                            (∀ {x y : α}, f x < f y ↔ x < y) →
                              (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                  f ⊤ = ⊤ →
                                    f ⊥ = ⊥ →
                                      (∀ (a : α), f aᶜ = (f a)ᶜ) →
                                        (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) → HeytingAlgebra α
-- Mathlib.CategoryTheory.Limits.Final
/-- A natural transformation `α : F ⟶ G` between functors `F G : C ⥤ Cat` which is final on each
fiber `(α.app X)` induces an equivalence of fiberwise colimits of `map α ⋙ H` and `H` for each
functor `H : Grothendieck G ⥤ Type`.  -/
CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F G : CategoryTheory.Functor C CategoryTheory.Cat} →
      (α : F ⟶ G) →
        [∀ (X : C), (α.app X).toFunctor.Final] →
          (H : CategoryTheory.Functor (CategoryTheory.Grothendieck G) (Type u₂)) →
            CategoryTheory.Limits.fiberwiseColimit ((CategoryTheory.Grothendieck.map α).comp H) ≅
              CategoryTheory.Limits.fiberwiseColimit H
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} {k : α},
  Std.DTreeMap.Raw.Const.insertManyIfNewUnit t [k] = t.insertIfNew k ()
-- Mathlib.CategoryTheory.Join.Basic
/-- Elements of `Join C D` are either elements of `C` or elements of `D`.  -/
CategoryTheory.Join : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] → (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → Type (max u₁ u₂)
-- Mathlib.Order.Hom.CompleteLattice
Set.image_sSup : ∀ {α : Type u_2} {β : Type u_3} {f : α → β} (s : Set (Set α)), f '' sSup s = sSup (Set.image f '' s)
-- Lean.Meta.Tactic.Grind.Arith.Insts
Lean.Meta.Grind.Arith.getIsCharInst? : Lean.Level → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option (Lean.Expr × ℕ))
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.cos_oangle_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
-- Lean.Meta.Match.Match
/-- Return true if the next element on the `p.vars` list is a variable.  -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isNextVar : Lean.Meta.Match.Problem → Bool
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- [Stacks Tag 00Q2](https://stacks.math.columbia.edu/tag/00Q2) -/
Algebra.not_isStronglyTranscendental_of_quasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S] {x : S},
  (Polynomial.aeval x).Finite →
    ∀ (P : Ideal S) [inst_4 : P.IsPrime] [Algebra.QuasiFiniteAt R P], ¬IsStronglyTranscendental R x
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Entries for the `apply` discrimination tree.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.app : Mathlib.Tactic.ClickSuggestions.Entries✝ →
  Array
    (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyLemma)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_ext₂_right_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {f : J → C} {X Y Z : C}
  {g h :
    X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y) Z},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.coe_id : ∀ {V : Type u_1} {G : SimpleGraph V}, ⇑(SimpleGraph.Copy.id G) = id
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k fallback : α}, k ∈ t → t.getKeyD k fallback = k
-- Mathlib.Data.List.Sort
List.decidableSortedLE : {α : Type u_1} → [inst : Preorder α] → [DecidableLE α] → DecidablePred List.SortedLE
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.injective : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B), Function.Injective ⇑f.toHom
-- Mathlib.GroupTheory.Transfer
/-- The transfer homomorphism `G →* center G`.  -/
MonoidHom.transferCenterPow : (G : Type u_1) → [inst : Group G] → [(Subgroup.center G).FiniteIndex] → G →* ↥(Subgroup.center G)
-- Mathlib.Algebra.Exact.Basic
Function.Exact.comp_eq_zero : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : Zero P], Function.Exact f g → g ∘ f = 0
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.ofTop.congr_simp : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) (h : p = ⊤), LinearEquiv.ofTop p h = LinearEquiv.ofTop p h
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.alts : Lean.Elab.Tactic.ElimApp.State✝ → Array Lean.Elab.Tactic.ElimApp.Alt
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.fintypeBot.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.fintypeBot = { elems := {0}, complete := ⋯ }
-- Mathlib.CategoryTheory.Category.Bipointed
swap_comp_bipointedToPointedFst : Bipointed.swap.comp bipointedToPointedFst = bipointedToPointedSnd
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.jmp.inj : ∀ {ref : Lean.Syntax} {jpName : Lean.Name} {args : Array Lean.Syntax} {ref_1 : Lean.Syntax} {jpName_1 : Lean.Name}
  {args_1 : Array Lean.Syntax},
  Lean.Elab.Term.Do.Code.jmp ref jpName args = Lean.Elab.Term.Do.Code.jmp ref_1 jpName_1 args_1 →
    ref = ref_1 ∧ jpName = jpName_1 ∧ args = args_1
-- Mathlib.Data.Matrix.Basic
/-- A version of `Matrix.scalar_commute_iff` for rectangular matrices.  -/
Matrix.scalar_comm_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : Semiring α] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : DecidableEq m] [inst_4 : Fintype m] {r : α} {M : Matrix m n α},
  (Matrix.scalar m) r * M = M * (Matrix.scalar n) r ↔ r • M = MulOpposite.op r • M
-- Mathlib.Analysis.Fourier.PoissonSummation
/-- **Poisson's summation formula** for Schwartz functions.  -/
SchwartzMap.tsum_eq_tsum_fourier : ∀ (f : SchwartzMap ℝ ℂ) (x : ℝ), ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), (FourierTransform.fourier f) ↑n * (fourier n) ↑x
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_rel_of_associated : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : α},
  Associated a b → Multiset.Rel Associated (UniqueFactorizationMonoid.factors a) (UniqueFactorizationMonoid.factors b)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValRat.multiplicity_sub_multiplicity : ∀ {p : ℕ} {q : ℚ}, p ≠ 1 → q ≠ 0 → padicValRat p q = ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mono' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} {g : α → ℝ},
  MeasureTheory.Integrable g μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) → MeasureTheory.Integrable f μ
-- Init.Data.AC
Lean.Data.AC.insert.eq_2 : ∀ (x a : ℕ) (as : List ℕ),
  Lean.Data.AC.insert x (a :: as) = if x < a then x :: a :: as else a :: Lean.Data.AC.insert x as
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.State.mk.inj : ∀ {toAssert : Array (Lean.Expr × Lean.Expr × ℕ)} {usedHyps : Std.HashSet Lean.FVarId}
  {toAssert_1 : Array (Lean.Expr × Lean.Expr × ℕ)} {usedHyps_1 : Std.HashSet Lean.FVarId},
  { toAssert := toAssert, usedHyps := usedHyps } = { toAssert := toAssert_1, usedHyps := usedHyps_1 } →
    toAssert = toAssert_1 ∧ usedHyps = usedHyps_1
-- Mathlib.Analysis.Normed.Module.DoubleDual
NormedSpace.inclusionInDoubleDual_norm_le : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], ‖NormedSpace.inclusionInDoubleDual 𝕜 E‖ ≤ 1
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedCommGroup.mem_closure_iff : ∀ {E : Type u_4} [inst : SeminormedCommGroup E] {a : E} {s : Set E},
  a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε
-- Mathlib.CategoryTheory.Action.Limits
/-- If `V` has colimits of shape `J`, so does `Action V G`.  -/
Action.hasColimitsOfShape : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J] [CategoryTheory.Limits.HasColimitsOfShape J V],
  CategoryTheory.Limits.HasColimitsOfShape J (Action V G)
-- Mathlib.Data.List.Cycle
List.next_cons_cons_eq' : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y z : α) (h : x ∈ y :: z :: l),
  x = y → (y :: z :: l).next x h = z
-- Init.Data.Array.Lemmas
/-- Variant of `append_inj_right` instead requiring equality of the sizes of the second arrays.  -/
Array.append_inj_right' : ∀ {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → ys₁.size = ys₂.size → ys₁ = ys₂
-- Mathlib.Algebra.Star.MonoidHom
/-- Reinterpret a star monoid homomorphism as a monoid homomorphism
by forgetting the interaction with the star operation.  -/
StarMonoidHom.toMonoidHom : {A : Type u_6} →
  {B : Type u_7} → [inst : Monoid A] → [inst_1 : Star A] → [inst_2 : Monoid B] → [inst_3 : Star B] → (A →⋆* B) → A →* B
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction_le_prefixFunction_sub_one_add_one : ∀ {pat : ByteArray} {stackPos : ℕ} {hst : stackPos < pat.size} (h₀ : 0 < stackPos),
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst ≤
    String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (stackPos - 1) ⋯ + 1
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Given a local frame `{s i}` on `U ∋ x`, returns the basis `{s i}` of `V x`  -/
IsLocalFrameOn.toBasisAt : {𝕜 : 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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : FiberBundle F V] →
                                        {ι : Type u_7} →
                                          {s : ι → (x : M) → V x} →
                                            {u : Set M} →
                                              {x : M} →
                                                {n : WithTop ℕ∞} →
                                                  IsLocalFrameOn I F n s u → x ∈ u → Module.Basis ι 𝕜 (V x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.method.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.method = 1
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.finiteDimensional_right : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  [FiniteDimensional K L], FiniteDimensional (↥F) L
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_expand_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {w x y z : P},
  Wbtw R w x y → Wbtw R x y z → x ≠ y → Wbtw R w x z
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forIn_eq_forIn : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ},
  Std.TreeMap.forIn f init t = forIn t init fun a d => f a.1 a.2 d
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- The limit cone for `F : J ⥤ C` lifts to a cocone in `Under (limit F)` with cone point
`𝟙 (limit F)`. This is automatically also a limit cone.  -/
CategoryTheory.Limits.limit.toUnder : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Limits.Cone
              ((CategoryTheory.Limits.limit.toStructuredArrow F).comp
                (CategoryTheory.StructuredArrow.toUnder (CategoryTheory.Limits.limit F) F))
-- Mathlib.Algebra.Algebra.Defs
Algebra.commutes' : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : Algebra R A] (r : R) (x : A),
  (algebraMap R A) r * x = x * (algebraMap R A) r
-- Mathlib.Order.Filter.Map
Filter.disjoint_comap_iff_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β},
  Disjoint F (Filter.comap f G) ↔ Disjoint (Filter.map f F) G
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientKerEquivOfRightInverse.eq_1 : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ),
  QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ =
    { toFun := ⇑(QuotientGroup.kerLift φ), invFun := QuotientGroup.mk ∘ ψ, left_inv := ⋯, right_inv := hφ,
      map_mul' := ⋯ }
-- Init.Data.UInt.Lemmas
BitVec.ofFin_uSizeToFin : ∀ (n : USize), { toFin := n.toFin } = n.toBitVec
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_castSucc_of_lt : ∀ {n : ℕ} (p i : Fin n), i < p → p.castSucc.succAbove i = i.castSucc
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.inv : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : Group β]
  [ContinuousInv β],
  MeasureTheory.IsStronglyProgressive f u → MeasureTheory.IsStronglyProgressive f fun i ω => (u i ω)⁻¹
-- Mathlib.RingTheory.IsTensorProduct
/-- The tensor product of a pair of linear maps between modules.  -/
IsTensorProduct.map : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M₁ : Type u_2} →
      {M₂ : Type u_3} →
        {M : Type u_4} →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R M] →
                      {f : M₁ →ₗ[R] M₂ →ₗ[R] M} →
                        {N₁ : Type u_6} →
                          {N₂ : Type u_7} →
                            {N : Type u_8} →
                              [inst_7 : AddCommMonoid N₁] →
                                [inst_8 : AddCommMonoid N₂] →
                                  [inst_9 : AddCommMonoid N] →
                                    [inst_10 : Module R N₁] →
                                      [inst_11 : Module R N₂] →
                                        [inst_12 : Module R N] →
                                          {g : N₁ →ₗ[R] N₂ →ₗ[R] N} →
                                            IsTensorProduct f →
                                              IsTensorProduct g → (M₁ →ₗ[R] N₁) → (M₂ →ₗ[R] N₂) → M →ₗ[R] N
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.zsmul_val : ∀ {R : Type u_1} {a b : R} [inst : CommRing R] (n : ℤ) (x y : R),
  ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.ae_map_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ →
    ∀ {p : β → Prop},
      MeasurableSet {x | p x} → ((∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ, p (f x))
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isWeaklyRegular_singleton_iff : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R),
  RingTheory.Sequence.IsWeaklyRegular M [r] ↔ IsSMulRegular M r
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.IsFiniteType.exists_localGeneratorsData : ∀ {C : Type u'} {inst : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} (M : SheafOfModules R) [self : M.IsFiniteType],
  ∃ σ, σ.IsFiniteType
-- Init.Omega.Int
Lean.Omega.Int.not_lt_of_ge : ∀ {x y : ℤ}, y ≥ x → ¬y < x
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.eq_1 : ∀ {G : Type u_1} [inst : AddMonoid G] (x : G), IsOfFinAddOrder x = (0 ∈ Function.periodicPts fun x_1 => x + x_1)
-- Init.Data.Array.Find
Array.idxOf_eq_size : ∀ {α : Type u_1} {a : α} [inst : BEq α] [LawfulBEq α] {xs : Array α}, a ∉ xs → Array.idxOf a xs = xs.size
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.mk.sizeOf_spec : ∀ (recursorName typeName : Lean.Name) (univLevelPos : List Lean.Meta.RecursorUnivLevelPos) (depElim recursive : Bool)
  (numArgs majorPos : ℕ) (paramsPos : List (Option ℕ)) (indicesPos : List ℕ) (produceMotive : List Bool),
  sizeOf
      { recursorName := recursorName, typeName := typeName, univLevelPos := univLevelPos, depElim := depElim,
        recursive := recursive, numArgs := numArgs, majorPos := majorPos, paramsPos := paramsPos,
        indicesPos := indicesPos, produceMotive := produceMotive } =
    1 + sizeOf recursorName + sizeOf typeName + sizeOf univLevelPos + sizeOf depElim + sizeOf recursive +
              sizeOf numArgs +
            sizeOf majorPos +
          sizeOf paramsPos +
        sizeOf indicesPos +
      sizeOf produceMotive
-- Mathlib.Algebra.GroupWithZero.Defs
/-- `a ^ 0 = 1`  -/
GroupWithZero.zpow_zero' : ∀ {G₀ : Type u} [self : GroupWithZero G₀] (a : G₀), a ^ 0 = 1
-- Mathlib.Tactic.Widget.Conv
/-- `Path.ofSubExprPosArray.go pos expr i` is the same as `Path.ofSubExprPosArray expr (pos.drop i)`
 -/
_private.Mathlib.Tactic.Widget.Conv.0.Mathlib.Tactic.Conv.Path.ofSubExprPosArray.go : (pos : Array ℕ) → Lean.Expr → Fin (pos.size + 1) → Lean.MetaM Mathlib.Tactic.Conv.Path
-- Lean.Compiler.IR.Format
_private.Lean.Compiler.IR.Format.0.Lean.IR.formatFnBodyHead' : Lean.IR.FnBody → String
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.toReal_lintegral_coe_eq_integral : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X]
  (f : BoundedContinuousFunction X NNReal) (μ : MeasureTheory.Measure X),
  (∫⁻ (x : X), ↑(f x) ∂μ).toReal = ∫ (x : X), ↑(f x) ∂μ
-- Mathlib.Algebra.Group.Action.Basic
arrowAddAction_vadd : ∀ {G : Type u_7} {A : Type u_8} {B : Type u_9} [inst : SubtractionMonoid G] [inst_1 : AddAction G A] (g : G) (F : A → B)
  (a : A), VAdd.vadd g F a = F (-g +ᵥ a)
-- Mathlib.Computability.RegularExpressions
RegularExpression.rmatch_iff_matches' : ∀ {α : Type u_1} [inst : DecidableEq α] (P : RegularExpression α) (x : List α), P.rmatch x = true ↔ x ∈ P.matches'
-- Init.Data.SInt.Lemmas
Int32.le_total : ∀ (a b : Int32), a ≤ b ∨ b ≤ a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_alter_of_not_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (Std.DTreeMap.Const.alter t k f).contains k' = t.contains k'
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- An endomorphism of a module is self-adjoint with respect to a bilinear map if it serves as an
adjoint for itself.  -/
LinearMap.IsSelfAdjoint : {R : Type u_1} →
  {M : Type u_5} →
    {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₁] → {I : R →+* R} → (M →ₗ[R] M →ₛₗ[I] M₁) → (M → M) → Prop
-- Mathlib.Algebra.Lie.Graded
/-- A derivation on the direct sum of graded pieces of a graded Lie algebra, induced by an additive
map on the grading monoid.  -/
LieDerivation.ofGradingSum : {ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid ι] →
          [inst_2 : CommRing R] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] →
                (ℒ : ι → Submodule R L) →
                  [inst_5 : GradedLieAlgebra ℒ] →
                    (ι →+ R) → LieDerivation R (DirectSum ι fun i => ↥(ℒ i)) (DirectSum ι fun i => ↥(ℒ i))
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.fold_hom : ∀ {α β : Type u_1} {γ₁ : Type x₁} {γ₂ : Type x₂} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [inst_4 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} (f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁},
  (∀ (x : γ₁) (y : β), g₂ (f x) y = f (g₁ x y)) → Std.Iter.fold g₂ (f init) it = f (Std.Iter.fold g₁ init it)
-- Std.Http.Data.Chunk
Std.Http.Chunk.mk : ByteArray → Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue) → Std.Http.Chunk
-- Mathlib.Tactic.Linarith.Datatypes
/-- `parseCompAndExpr e` checks if `e` is of the form `t < 0`, `t ≤ 0`, or `t = 0`.
If it is, it returns the comparison along with `t`.
 -/
Mathlib.Tactic.Linarith.parseCompAndExpr : Lean.Expr → Lean.MetaM (Mathlib.Ineq × Lean.Expr)
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_mul : ∀ {a b : ℤ} {hab₁ : Int16.minValue.toInt ≤ a * b} {hab₂ : a * b ≤ Int16.maxValue.toInt},
  Int16.ofIntLE (a * b) hab₁ hab₂ = Int16.ofInt a * Int16.ofInt b
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- Synonym for `Hom.mk` which makes unification easier.  -/
CategoryTheory.Bicategory.InducedBicategory.mkHom : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} → {X Y : CategoryTheory.Bicategory.InducedBicategory C F} → (F X ⟶ F Y) → (X ⟶ Y)