mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph.0.SimpleGraph.Walk.toSubgraph.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2)
  (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_1 : V) → (h : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h p)),
  (match u, SimpleGraph.Walk.nil with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h p => h_2 v v_1 h p) =
    h_1 ()
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlight : Type
-- Mathlib.Data.Set.Finite.Lattice
/-- **Alias** of `iSup_iInf_of_monotone`. -/
Set.iSup_iInf_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι']
  [inst_3 : Order.Frame α] {f : ι → ι' → α}, (∀ (i : ι), Monotone (f i)) → ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
-- Mathlib.Algebra.Order.Monovary
Monovary.mul_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β}, Monovary f₁ g → Monovary f₂ g → Monovary (f₁ * f₂) g
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioc_ofDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (b a : αᵒᵈ),
  Finset.Ioc (OrderDual.ofDual b) (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ico a b)
-- Init.Tactics
/-- `injections` applies `injection` to all hypotheses recursively
(since `injection` can produce new hypotheses). Useful for destructing nested
constructor equalities like `(a::b::c) = (d::e::f)`.  -/
Lean.Parser.Tactic.injections : Lean.ParserDescr
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce_append_reduce_reduce : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.reduce (FreeAddGroup.reduce L₁ ++ FreeAddGroup.reduce L₂) = FreeAddGroup.reduce (L₁ ++ L₂)
-- Init.Data.BitVec.Lemmas
/-- `0#w = 1#w` iff the width is zero.  -/
BitVec.zero_eq_one_iff : ∀ (w : ℕ), 0#w = 1#w ↔ w = 0
-- Mathlib.Analysis.Analytic.Basic
AnalyticOn.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) (s : Set E),
  AnalyticOn 𝕜 f s = ∀ x ∈ s, AnalyticWithinAt 𝕜 f s x
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- A family of submodules in a commutative `R`-algebra `A` is a submodules basis if it satisfies
some axioms ensuring there is a topology on `A` which is compatible with the ring structure and
admits this family as a basis of neighborhoods of zero.  -/
SubmodulesRingBasis : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} → [inst : CommRing R] → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → (ι → Submodule R A) → Prop
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk_top : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α}, ⟨⊤, ⋯⟩ = ⊤
-- Mathlib.Order.Preorder.Chain
Antitone.isChain_range : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → IsChain (fun x1 x2 => x1 ≤ x2) (Set.range f)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.det_ne_zero_of_left_inverse : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α}
  [Nontrivial α], B * A = 1 → A.det ≠ 0
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.toPermHom.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Equiv.Perm.OnCycleFactors.toPermHom g = MulAction.toPermHom ↥(Subgroup.centralizer {g}) ↥g.cycleFactorsFinset
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The `i`th object (with `i : ℕ` such that `i ≤ n`) of `F : ComposableArrows C n`.  -/
CategoryTheory.ComposableArrows.obj' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      CategoryTheory.ComposableArrows C n → (i : ℕ) → autoParam (i ≤ n) CategoryTheory.ComposableArrows.obj'._auto_1 → C
-- Mathlib.Topology.Basic
isClosed_iUnion_of_finite : ∀ {X : Type u} {ι : Sort v} [inst : TopologicalSpace X] [Finite ι] {s : ι → Set X},
  (∀ (i : ι), IsClosed (s i)) → IsClosed (⋃ i, s i)
-- Std.Data.TreeMap.Raw.Basic
/-- Inserts multiple elements into the tree map by iterating over the given collection and calling
`insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.
 -/
Std.TreeMap.Raw.insertManyIfNewUnit : {α : Type u} →
  {cmp : α → α → Ordering} →
    {ρ : Type u_1} → [ForIn Id ρ α] → Std.TreeMap.Raw α Unit cmp → ρ → Std.TreeMap.Raw α Unit cmp
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_symm_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁), e.symm.symm x = e x
-- Mathlib.Topology.Bases
IsOpenMap.separableSpace_of_injective : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] [TopologicalSpace.SeparableSpace β]
  {f : α → β}, IsOpenMap f → Function.Injective f → TopologicalSpace.SeparableSpace α
-- Mathlib.Algebra.Category.ModuleCat.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.mk.injEq : ∀ {R : Type u} [inst : Ring R] (carrier : Type v) [isAddCommGroup : AddCommGroup carrier] [isModule : Module R carrier]
  (carrier_1 : Type v) (isAddCommGroup_1 : AddCommGroup carrier_1) (isModule_1 : Module R carrier_1),
  ({ carrier := carrier, isAddCommGroup := isAddCommGroup, isModule := isModule } =
      { carrier := carrier_1, isAddCommGroup := isAddCommGroup_1, isModule := isModule_1 }) =
    (carrier = carrier_1 ∧ isAddCommGroup ≍ isAddCommGroup_1 ∧ isModule ≍ isModule_1)
-- Init.Data.Array.Basic
/-- Applies a function that returns an `Option` to each element of an array, collecting the non-`none`
values.

Example:
```lean example
#eval #[1, 2, 5, 2, 7, 7].filterMap fun x =>
  if x > 2 then some (2 * x) else none
```
```output
#[10, 14, 14]
```
 -/
Array.filterMap : {α : Type u} → {β : Type u_1} → (α → Option β) → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → Array β
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Companion lemma to `MeromorphicOn.exists_ecanonicalDecomp`: In the setting of the extended canonical
decomposition, write the function `h` entirely in terms of `f`, under the assumption that `f` has
order zero.
 -/
Complex.ECanonicalDecomp.eq_smul_meromorphicTrailingCoeffAt_of_meromorphicOrderAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {w : ℂ} {f h : ℂ → E},
  Complex.ECanonicalDecomp f h R →
    w ∈ Metric.closedBall 0 R →
      meromorphicOrderAt f w = 0 →
        0 < R →
          h w =
            ((∏ᶠ (i : ℂ), Complex.canonicalFactor R i w ^ (MeromorphicOn.divisor f (Metric.ball 0 R)) i) *
                ∏ᶠ (i : ℂ), (w - i) ^ (-MeromorphicOn.divisor f (Metric.sphere 0 R)) i) •
              meromorphicTrailingCoeffAt f w
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}, ProbabilityTheory.Kernel.fst 0 = 0
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHaveEqnsDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNNNorm_toMatrix : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NontriviallyNormedField α] [NormedAlgebra ℝ α] [inst_4 : DecidableEq n] (f : (n → α) →L[α] m → α),
  ‖LinearMap.toMatrix' ↑f‖₊ = ‖f‖₊
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The `Matrix` version of `inv_add_inv'`  -/
Matrix.inv_add_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
  (IsUnit A ↔ IsUnit B) → A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹
-- Batteries.Util.Cache
/-- Creates a cache with an initialization function.  -/
Batteries.Tactic.Cache.mk : {α : Type} → Lean.MetaM α → IO (Batteries.Tactic.Cache α)
-- Init.Data.Option.Array
Option.forIn'_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (o : Option α) (b : β)
  (f : (a : α) → a ∈ o.toArray → β → m (ForInStep β)), forIn' o.toArray b f = forIn' o b fun a m b => f a ⋯ b
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion.0.iteratedDerivWithin_tsum_exp_aux_eq : ∀ {k : ℕ},
  1 ≤ k →
    ∀ (z : UpperHalfPlane),
      iteratedDerivWithin k
          (fun z =>
            ↑Real.pi * Complex.I -
              2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n)
          UpperHalfPlane.upperHalfPlaneSet ↑z =
        -(2 * ↑Real.pi * Complex.I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The vector from `centroid` to a vertex corresponding `faceOppositeCentroid` is `n⁻¹` of the
vector from the vertex to the centroid.  -/
Affine.Simplex.faceOppositeCentroid_vsub_centroid_eq_smul_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i -ᵥ s.centroid = (↑n)⁻¹ • (s.centroid -ᵥ s.points i)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_eq_setToSimpleFunc : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F) (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.setToL1S T f =
    MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameOptions.mk.injEq : ∀ (prepareProvider prepareProvider_1 : Bool),
  ({ prepareProvider := prepareProvider } = { prepareProvider := prepareProvider_1 }) =
    (prepareProvider = prepareProvider_1)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_add : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (s t : NonemptyInterval α), (s + t).toProd.2 = s.toProd.2 + t.toProd.2
-- Mathlib.Logic.Encodable.Basic
Encodable.mk : {α : Type u_1} → (encode : α → ℕ) → (decode : ℕ → Option α) → (∀ (a : α), decode (encode a) = some a) → Encodable α
-- Mathlib.Topology.Constructions.SumProd
/-- Precomposing `f` with `Prod.snd` is continuous  -/
Continuous.snd' : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : Y → Z}, Continuous f → Continuous fun x => f x.2
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ipcStdioConfig : IO.Process.StdioConfig
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.instFunctorPostconditionT : {m : Type w → Type w'} → [Functor m] → Functor (Std.Iterators.PostconditionT m)
-- Init.Data.String.Iterate
String.Slice.PosIterator.instIteratorSubtypePosNeEndPosOfPure : {m : Type → Type u_1} → {s : String.Slice} → [Pure m] → Std.Iterator s.PosIterator m { p // p ≠ s.endPos }
-- Mathlib.Order.Lattice
instDistribLatticeNat : DistribLattice ℕ
-- Init.Data.SInt.Lemmas
Int64.toISize_mul : ∀ (a b : Int64), (a * b).toISize = a.toISize * b.toISize
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_iff_smul_rearrangement`.

---

Two functions monovary iff the rearrangement inequality holds.  -/
Monovary.smul_add_smul_le_smul_add_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β},
  Monovary f g → ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.coe_vadd : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ[σ] F)
  (g : E →ₛₗ.[σ] F), ↑(f +ᵥ g) = ⇑(f ∘ₛₗ g.domain.subtype) + ↑g
-- Mathlib.Order.Filter.Subsingleton
/-- A nontrivial subsingleton filter is equal to `pure a` for some `a`.  -/
Filter.Subsingleton.exists_eq_pure : ∀ {α : Type u_1} {l : Filter α} [l.NeBot], l.Subsingleton → ∃ a, l = pure a
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHom`. -/
AddCommGroup.isTorsion_quotient_range_nsmulAddMonoidHom : ∀ (G : Type u_1) [inst : AddCommGroup G] {n : ℕ}, n ≠ 0 → IsAddTorsion (G ⧸ (nsmulAddMonoidHom n).range)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass =
    OrderEmbedding.ofStrictMono (fun s => { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ s}, upper' := ⋯ }) ⋯
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
to the power of the `v`-adic valuation.  -/
NumberField.FinitePlace.norm_embedding' : ∀ {K : Type u_1} [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : K),
  ‖(NumberField.FinitePlace.embedding v) x‖ =
    ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.coe_det : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M ≃ₗ[R] M),
  ↑(LinearEquiv.det f) = LinearMap.det ↑f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α}
  (h : t.WF) {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.size = if k ∈ t then t.size else t.size + 1
-- Mathlib.Logic.Function.Iterate
Function.Commute.iterate_left : ∀ {α : Type u} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ), Function.Commute f^[n] g
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Given a set `S` and a walk `w` from `u` to `v` such that `u ∈ S` but `v ∉ S`,
there exists a dart in the walk whose start is in `S` but whose end is not.  -/
SimpleGraph.Walk.exists_boundary_dart : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (S : Set V),
  u ∈ S → v ∉ S → ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
-- Mathlib.Order.Basic
/-- **Alias** of `le_antisymm`. -/
LE.le.antisymm : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.inclusion.congr_simp : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S T : NonUnitalSubalgebra R A} (h : S ≤ T), NonUnitalSubalgebra.inclusion h = NonUnitalSubalgebra.inclusion h
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β},
      (t.modify k f).isEmpty = false →
        ∀ {fallback : α},
          (t.modify k f).minKeyD fallback = if cmp (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.lift_matrix : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] {K : Type} [inst_3 : Finite K] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} {P : C} (x : (j : J) → P ⟶ f j) (m : (j : J) → (k : K) → f j ⟶ g k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift x)
      (CategoryTheory.Limits.biproduct.matrix m) =
    CategoryTheory.Limits.biproduct.lift fun k => ∑ j, CategoryTheory.CategoryStruct.comp (x j) (m j k)
-- Init.Data.Int.DivMod.Lemmas
Int.add_bmod_eq_add_bmod_right : ∀ {x : ℤ} {n : ℕ} {y : ℤ} (i : ℤ), x.bmod n = y.bmod n → (x + i).bmod n = (y + i).bmod n
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instMin : {E : Type u_3} → [inst : CommGroup E] → Min (GroupSeminorm E)
-- Init.Data.List.Perm
List.perm_comm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ ↔ l₂.Perm l₁
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.Internal.memcmpStr.go : (lhs rhs : String) →
  (lstart rstart len : String.Pos.Raw) →
    len.offsetBy lstart ≤ lhs.rawEndPos → len.offsetBy rstart ≤ rhs.rawEndPos → String.Pos.Raw → Bool
-- Mathlib.LinearAlgebra.Determinant
/-- If `R^m` and `R^n` are linearly equivalent, then `m` and `n` are also equivalent.  -/
equivOfPiLEquivPi : {m : Type u_6} →
  {n : Type u_7} →
    {R : Type u_8} → [Finite m] → [Finite n] → [inst : CommRing R] → [Nontrivial R] → ((m → R) ≃ₗ[R] n → R) → m ≃ n
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.dropWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.dropWhile pat = s.sliceFrom (s.skipPrefixWhile pat)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_smul : ∀ {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : SMul S R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃),
  (s • a).imI = s • a.imI
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt : Type
-- Mathlib.Data.Finset.Sups
Finset.diffs_union_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t₁ t₂ : Finset α},
  s.diffs (t₁ ∪ t₂) = s.diffs t₁ ∪ s.diffs t₂
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a b : MvPolynomial σ R),
  (a * b).totalDegree ≤ a.totalDegree + b.totalDegree
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instHashableEMatchTheoremKind.hash : Lean.Meta.Grind.EMatchTheoremKind → UInt64
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.UniversallyClosed.universally_isClosedMap : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.UniversallyClosed f],
  (AlgebraicGeometry.topologically @IsClosedMap).universally f
-- Mathlib.Algebra.Lie.Abelian
LieModule.trivial_iff_le_maximal_trivial : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N : LieSubmodule R L M), LieModule.IsTrivial L ↥N ↔ N ≤ LieModule.maxTrivSubmodule R L M
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.smul_eq_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M], CategoryTheory.ModObj.smul = CategoryTheory.MonObj.mul
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasure.measure_univ_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.IsFiniteMeasure μ],
  μ Set.univ < ⊤
-- Lean.Declaration
Lean.instInhabitedAxiomVal.default : Lean.AxiomVal
-- Mathlib.Tactic.Ring.Common
/-- Checks whether `e` would be processed by `eval` as a ring expression,
or otherwise if it is an atom or something simplifiable via `norm_num`.

We use this in `ring_nf` to avoid rewriting atoms unnecessarily.

Returns:
* `none` if `eval` would process `e` as an algebraic ring expression
* `some none` if `eval` would treat `e` as an atom.
* `some (some r)` if `eval` would not process `e` as an algebraic ring expression,
  but `NormNum.derive` can nevertheless simplify `e`, with result `r`.
 -/
Mathlib.Tactic.Ring.Common.isAtomOrDerivable : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.Cache sα →
            (e : Q(«$α»)) →
              Mathlib.Tactic.AtomM
                (Option (Option (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) e)))
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- The morphism `(F.shift a).obj X ⟶ (F.shift a').obj Y` induced by a morphism
`f : X ⟶ Y⟦n⟧` when `n + a = a'`.  -/
CategoryTheory.Functor.shiftMap : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} A] →
        (F : CategoryTheory.Functor C A) →
          {M : Type u_4} →
            [inst_2 : AddMonoid M] →
              [inst_3 : CategoryTheory.HasShift C M] →
                [inst_4 : F.ShiftSequence M] →
                  {X Y : C} →
                    {n : M} →
                      (X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) →
                        (a a' : M) → n + a = a' → ((F.shift a).obj X ⟶ (F.shift a').obj Y)
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_toPEquiv_apply : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] (f : m ≃ n)
  (i : m), f.toPEquiv.toMatrix i = Pi.single (f i) 1
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Real.hasDerivAt_Gamma_one_half : HasDerivAt Real.Gamma (-√Real.pi * (Real.eulerMascheroniConstant + 2 * Real.log 2)) (1 / 2)
-- Init.Control.Id
Id.instMonadLiftTOfPure : {m : Type u → Type v} → [Pure m] → MonadLiftT Id m
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.image_smul_distrib : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Mul α]
  [inst_3 : Mul β] [inst_4 : FunLike F α β] [MulHomClass F α β] (f : F) (a : α) (s : Finset α),
  Finset.image (⇑f) (a • s) = f a • Finset.image (⇑f) s
-- Init.Core
/-- The second component of a dependent pair. Its type depends on the first component.
 -/
PSigma.snd : {α : Sort u} → {β : α → Sort v} → (self : PSigma β) → β self.fst
-- Mathlib.Data.Set.Function
Function.invFunOn_mem : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [inst : Nonempty α],
  (∃ a ∈ s, f a = b) → Function.invFunOn f s b ∈ s
-- Mathlib.Topology.ContinuousOn
/-- If `f` is continuous on `s` and `u` is a neighbourhood of `t`, then `f ⁻¹' u` is a neighbourhood
of `s ∩ f ⁻¹' t` within `s`.  -/
ContinuousOn.preimage_mem_nhdsSetWithin_of_mem_nhdsSet : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s → ∀ {t u : Set β}, u ∈ nhdsSet t → f ⁻¹' u ∈ nhdsSetWithin (s ∩ f ⁻¹' t) s
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.sum_isAddUnit_iff : ∀ {M : Type u_8} [inst : AddCommMonoid M] {L : List M}, IsAddUnit L.sum ↔ ∀ m ∈ L, IsAddUnit m
-- Mathlib.Data.Fin.VecNotation
/-- `![a, b, ...] 1` is equal to `b`.

The simplifier needs a special lemma for length `≥ 2`, in addition to
`cons_val_succ`, because `1 : Fin 1 = 0 : Fin 1`.
 -/
Matrix.cons_val_one : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ → α), Matrix.vecCons x u 1 = u 0