mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.References
/-- Yields a `ParentDecl` for the declaration `name`.  -/
Lean.Server.References.ParentDecl.ofDecls? : Lean.Lsp.Decls → String → Option Lean.Server.References.ParentDecl
-- Lean.Elab.PreDefinition.WF.GuessLex
_private.Lean.Elab.PreDefinition.WF.GuessLex.0.Lean.Elab.WF.GuessLex.naryVarNames.freshen : Array Lean.Name → Lean.Name → Lean.MetaM Lean.Name
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_add_cancel_right : ∀ {x : ℤ} {n : ℕ} {y : ℤ} (i : ℤ), (x + i).bmod n = (y + i).bmod n ↔ x.bmod n = y.bmod n
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.pi_proj : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs : (i : ι) → X i}
  (p : Path.Homotopic.Quotient as bs), (Path.Homotopic.pi fun i => Path.Homotopic.proj i p) = p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
NNReal.instContinuousMapZero.UniqueHom : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : Module ℝ A] [inst_3 : TopologicalSpace A]
  [IsSemitopologicalRing A] [inst_5 : IsScalarTower ℝ A A] [inst_6 : SMulCommClass ℝ A A] [T2Space A],
  ContinuousMapZero.UniqueHom NNReal A
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.homEquivToProd_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z : C} (f : Z ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y),
  CategoryTheory.CartesianMonoidalCategory.homEquivToProd f =
    (CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))
-- Batteries.Data.List.Basic
/-- Auxiliary for `countPBefore`: `countPBefore.go p l i acc = countPBefore p l i + acc`.  -/
List.countPBefore.go : {α : Type u_1} → (α → Bool) → List α → ℕ → ℕ → ℕ
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.lie_snd_eq_zero_of_mem_prodCartan : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂) {y : ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂)},
  y ∈ LieAlgebra.Basis.prodCartan✝ eι b₁ b₂ → ∀ (x : ↥H₂), ⁅(↑y).2, ↑x⁆ = 0
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_induction₂ : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A}
  {p : (x y : A) → x ∈ NonUnitalAlgebra.adjoin R s → y ∈ NonUnitalAlgebra.adjoin R s → Prop},
  (∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p 0 x ⋯ hx) →
      (∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x 0 hx ⋯) →
        (∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s)
            (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
          (∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s)
              (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
            (∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s)
                (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
              (∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s)
                  (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
                (∀ (r : R) (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s),
                    p x y hx hy → p (r • x) y ⋯ hy) →
                  (∀ (r : R) (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s),
                      p x y hx hy → p x (r • y) hx ⋯) →
                    ∀ {x y : A} (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s),
                      p x y hx hy
-- Mathlib.Data.Nat.Totient
Nat.totient_super_multiplicative : ∀ (a b : ℕ), a.totient * b.totient ≤ (a * b).totient
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All n-simplices among cospherical points in n-space have the same
circumradius.  -/
EuclideanGeometry.exists_circumradius_eq_of_cospherical : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V],
  Module.finrank ℝ V = n →
    EuclideanGeometry.Cospherical ps →
      ∃ r, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.of_mul_lt_mul_left : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : LinearOrder α],
  (∀ (a b c : α), b < c → a * b < a * c) → IsOrderedCancelMonoid α
-- Mathlib.Tactic.Ring.Common
/-- Evaluate the inverse of a coefficient.  -/
Mathlib.Tactic.Ring.Common.RingCompute.inv : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα →
          {x : Q(«$α»)} →
            Option Q(CharZero «$α») →
              (fα : Q(Semifield «$α»)) →
                BaseType x → Mathlib.Tactic.AtomM (Option (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x»⁻¹)))
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_insert_eq_add_one : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, e ∈ M.E \ M.closure X → M.eRk (insert e X) = M.eRk X + 1
-- Lean.Meta.Tactic.Simp.Types
/-- Number of times each simp theorem has been used/applied.  -/
Lean.Meta.Simp.Diagnostics.usedThmCounter : Lean.Meta.Simp.Diagnostics → Lean.PHashMap Lean.Meta.Origin ℕ
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.lift₂NatIso.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂]
  [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E))
  [inst_9 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁']
  [inst_10 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (e e_1 : F₁ ≅ F₂),
  e = e_1 →
    CategoryTheory.Localization.lift₂NatIso L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e =
      CategoryTheory.Localization.lift₂NatIso L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e_1
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_naturality₂ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₂ : CategoryTheory.LocalizedMonoidal L W ε} (f₂ : X₂ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ f₂) X₃)
      (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₂ X₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₂ X₃))
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instSMulCommClass : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  {𝕜 : Type u_5} {𝕜' : Type u_6} [inst_2 : SMul 𝕜 γ] [inst_3 : ContinuousConstSMul 𝕜 γ] [inst_4 : SMul 𝕜' γ]
  [inst_5 : ContinuousConstSMul 𝕜' γ] [SMulCommClass 𝕜 𝕜' γ], SMulCommClass 𝕜 𝕜' (α →ₘ[μ] γ)
-- Mathlib.Algebra.Free
FreeAddSemigroup.traverse.eq_1 : ∀ {m : Type u → Type u} [inst : Applicative m] {α β : Type u} (F : α → m β) (x : FreeAddSemigroup α),
  FreeAddSemigroup.traverse F x =
    x.recOnPure (fun x => pure <$> F x) fun _x _y ihx ihy => (fun x1 x2 => x1 + x2) <$> ihx <*> ihy
-- Mathlib.Algebra.Order.IsBotOne
zero_min : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Zero α] [IsBotZeroClass α] (a : α), min 0 a = 0
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.comap_comap : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {W : Type u_5}
  [inst_2 : TopologicalSpace W] (f : C(W, X)) (g : C(X, Y)) (x : LocallyConstant Y Z),
  LocallyConstant.comap f (LocallyConstant.comap g x) = LocallyConstant.comap (g.comp f) x
-- Mathlib.Algebra.Homology.Single
/-- The object in degree `j` of `(single V c h).obj A` is just `A`.  -/
HomologicalComplex.singleObjXSelf : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            (c : ComplexShape ι) → (j : ι) → (A : V) → ((HomologicalComplex.single V c j).obj A).X j ≅ A
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_insert_map_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {a : α}
  {s : Set ↥(SubMulAction.ofStabilizer M a)}, Function.Bijective ⇑(SubMulAction.ofFixingSubgroup_insert_map a s)
-- Batteries.Tactic.Lint.Simp
/-- Returns true if this is a `@[simp]` declaration.  -/
Batteries.Tactic.Lint.isSimpTheorem : Lean.Name → Lean.MetaM Bool
-- Mathlib.GroupTheory.Coset.Basic
normal_of_eq_addCosets : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), (∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s) → s.Normal
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.instFunLike : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        {I : Ideal A} → {J : Ideal B} → (hI : DividedPowers I) → (hJ : DividedPowers J) → FunLike (hI.DPMorphism hJ) A B
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.isEmpty = false ↔
    ∃ k, ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), (f k (t.get k h)).isSome = true
-- Lean.Environment
/-- The constructor of `Environment` is private to protect against modification that bypasses the
kernel.
 -/
_private.Lean.Environment.0.Lean.Kernel.Environment.mk : Lean.ConstMap →
  Bool →
    Lean.Kernel.Diagnostics →
      Std.HashMap Lean.Name Lean.ModuleIdx →
        Array Lean.EnvExtensionState → Array Lean.EnvExtensionState → Lean.EnvironmentHeader → Lean.Kernel.Environment
-- Mathlib.Data.Nat.Choose.Multinomial
Finsupp.multinomial.eq_1 : ∀ {α : Type u_1} (f : α →₀ ℕ), f.multinomial = (f.sum fun x => id).factorial / f.prod fun x n => n.factorial
-- Mathlib.MeasureTheory.Integral.IntervalAverage
/-- The mean value theorem for integrals:
There exists a point in an interval such that the mean of a continuous function over the interval
equals the value of the function at the point.  -/
exists_eq_interval_average : ∀ {f : ℝ → ℝ} {a b : ℝ}, a ≠ b → ContinuousOn f (Set.uIcc a b) → ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in a..b, f x
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of an `AddMonoid` inherits an addition.  -/
AddSubmonoid.add : {M : Type u_4} → [inst : AddZeroClass M] → (S : AddSubmonoid M) → Add ↥S
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexXZeroIso.eq_1 : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  Λ.chainComplexXZeroIso X = CategoryTheory.Iso.refl ((Λ.chainComplex X).X 0)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.instMul : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              (x : Submonoid A) →
                [inst_3 : AddCommMonoid ι] →
                  [inst_4 : DecidableEq ι] → [GradedRing 𝒜] → Mul (HomogeneousLocalization.NumDenSameDeg 𝒜 x)
-- Mathlib.Topology.Semicontinuity.Defs
semicontinuousOn_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {s : Set α},
  SemicontinuousOn r s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, ¬r x' y) → ¬r x y
-- Mathlib.NumberTheory.Padics.PadicNumbers
Int.padicValuation_eq_one_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {x : ℤ}, (Int.padicValuation p) x = 1 ↔ ¬↑p ∣ x
-- ProofWidgets.Component.MakeEditLink
/-- A link that, when clicked, makes the specified edit
and potentially moves the cursor
or makes a selection.  -/
ProofWidgets.MakeEditLink : ProofWidgets.Component ProofWidgets.MakeEditLinkProps
-- Mathlib.NumberTheory.LSeries.SumCoeff
/-- If `f` takes nonnegative real values and the partial sums `∑ k ∈ Icc 1 n, f k` are `O(n ^ r)`
for some real `0 ≤ r`, then for `s : ℂ` with `r < s.re`, we have
`LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (-(s + 1))`.  -/
LSeries_eq_mul_integral_of_nonneg : ∀ (f : ℕ → ℝ) {r : ℝ},
  0 ≤ r →
    ∀ {s : ℂ},
      r < s.re →
        ((fun n => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun n => ↑n ^ r) →
          (∀ (n : ℕ), 0 ≤ f n) →
            LSeries (fun n => ↑(f n)) s =
              s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Finset.Icc 1 ⌊t⌋₊, ↑(f k)) * ↑t ^ (-(s + 1))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.forM_eq_forM : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → β → m PUnit.{w + 1}},
  Std.ExtTreeMap.forM f t = forM t fun a => f a.1 a.2
-- Init.Data.Nat.Gcd
Nat.gcd_dvd_gcd_mul_left_left : ∀ (m n k : ℕ), m.gcd n ∣ (k * m).gcd n
-- Mathlib.Tactic.Peel
Mathlib.Tactic.Peel.frequently_imp : ∀ {α : Type u_1} {p q : α → Prop} {f : Filter α}, (∀ (x : α), p x → q x) → (∃ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x
-- Mathlib.Tactic.Linter.TextBased
/-- Output the formatted error message, containing its context.
`style` specifies if the error should be formatted for humans to read, github problem matchers
to consume, or for the style exceptions file.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.outputMessage : Mathlib.Linter.TextBased.ErrorContext✝ → Mathlib.Linter.TextBased.ErrorFormat → String
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instInhabitedIProp : Inhabited Mathlib.Tactic.ITauto.IProp
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.property : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x),
  Manifold.LiftSourceTargetPropertyAt I J n f x (Manifold.SubmersionAtProp h.complement I J M N)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_p_pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ), ‖↑p ^ n‖ = ↑p ^ (-↑n)
-- Lean.Language.Basic
/-- The asynchronously available children of the snapshot tree node.  -/
Lean.Language.SnapshotTree.children : Lean.Language.SnapshotTree → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.root_sub_nsmul_mem_range_iff_le_chainBotCoeff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∀ {n : ℕ}, P.root j - n • P.root i ∈ Set.range ⇑P.root ↔ n ≤ RootPairing.chainBotCoeff i j
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- Given `U : FormalCoproduct C` and a type `α`, this is the formal coproduct
indexed by all `i : α → U.I` of the products of the objects `U.obj (i a)`
for all `a : α`.  -/
CategoryTheory.Limits.FormalCoproduct.power : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Limits.FormalCoproduct C →
      (α : Type t) → [CategoryTheory.Limits.HasProductsOfShape α C] → CategoryTheory.Limits.FormalCoproduct C
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanHom_one_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsAddFreimanHom 1 A B f ↔ Set.MapsTo f A B
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension G] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape D H]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape C H] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X) (L.colimitIsoColimitGrothendieck G).hom =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G)
      { base := L.obj X, fiber := CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)) }
-- Init.GrindInstances.Ring.UInt
UInt64.instOfNat.eq_1 : ∀ {n : ℕ}, UInt64.instOfNat = { ofNat := UInt64.ofNat n }
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.inv_mem_Ioc_iff : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a c d : α},
  a⁻¹ ∈ Set.Ioc c d ↔ a ∈ Set.Ico d⁻¹ c⁻¹
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ioo : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a b : α i),
  Pi.mulSingle i '' Set.Ioo a b = Set.Ioo (Pi.mulSingle i a) (Pi.mulSingle i b)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_inter_add_sdiff : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s →
    MeasurableSet t →
      μ.IntegrableOn f s →
        ∫ᵛ (x : X) in s ∩ t, f x ∂[B; μ] + ∫ᵛ (x : X) in s \ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₁₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (self : CategoryTheory.ShortComplex.SnakeInput C) {Z : CategoryTheory.ShortComplex C} (h : self.L₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.v₁₂ (CategoryTheory.CategoryStruct.comp self.v₂₃ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.charFun_map_sum_pi_eq_prod : ∀ {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E]
  [SecondCountableTopology E] [inst_4 : Fintype ι] [inst_5 : InnerProductSpace ℝ E] (μ : ι → MeasureTheory.Measure E)
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)],
  MeasureTheory.charFun (MeasureTheory.Measure.map (fun p => ∑ i, p i) (MeasureTheory.Measure.pi μ)) =
    ∏ i, MeasureTheory.charFun (μ i)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldrM.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (x : δ), Std.DHashMap.Internal.AssocList.foldrM f x Std.DHashMap.Internal.AssocList.nil = pure x
-- Mathlib.Order.Monotone.Defs
Subsingleton.monotone' : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton β] (f : α → β), Monotone f
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_eq_mul_pow_sub_pow_div_expChar : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) (n : ℕ) {p : ℕ} [hR : ExpChar R p],
  (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
-- Init.Data.BitVec.Basic
/-- If two natural numbers `n` and `m` are equal, then a bitvector of width `n` is also a bitvector of
width `m`.

Using `x.cast eq` should be preferred over `eq ▸ x` because there are special-purpose `simp` lemmas
that can more consistently simplify `BitVec.cast` away.
 -/
BitVec.cast : {n m : ℕ} → n = m → BitVec n → BitVec m
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.sum : ∀ {α : Type u_1} {n : ℤ} {f g : α → ℤ} {s : Finset α},
  (∀ x ∈ s, f x ≡ g x [ZMOD n]) → ∑ x ∈ s, f x ≡ ∑ x ∈ s, g x [ZMOD n]
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.d₂ : ∀ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂}
  {e₀₂ : SSet.Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 2)) h.simplex = e₀₁.edge
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_closure : ∀ {R : Type u} [inst : NonAssocRing R] {x : R} {s : Set R}, x ∈ Subring.closure s ↔ ∀ (S : Subring R), s ⊆ ↑S → x ∈ S
-- Mathlib.Algebra.Prime.Lemmas
Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p a b : M} {n : ℕ},
  Prime p → p ^ n.succ ∣ a ^ n.succ * b ^ n → ¬p ^ 2 ∣ b → p ∣ a