mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.SnakeLemma
/-- Suppose we have an exact commutative diagram
```
        K₂ -F-→ K₃
        |       |
        ι₂      ι₃
        ↓       ↓
M₁ -f₁→ M₂ -f₂→ M₃
|       |       |
i₁      i₂      i₃
↓       ↓       ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁

```
such that `f₂` is surjective, `g₁` is injective, and `ι₃` is injective,
then `K₂ -F→ K₃ -δ→ C₁` is exact.
 -/
SnakeLemma.exact_δ'_right : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  {N₃ : Type u_7} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Function.Exact ⇑g₁ ⇑g₂)
  (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) {K₂ : Type u_8} {K₃ : Type u_9} {C₁ : Type u_10}
  [inst_13 : AddCommGroup K₂] [inst_14 : Module R K₂] [inst_15 : AddCommGroup K₃] [inst_16 : Module R K₃]
  [inst_17 : AddCommGroup C₁] [inst_18 : Module R C₁] (ι₂ : K₂ →ₗ[R] M₂),
  Function.Exact ⇑ι₂ ⇑i₂ →
    ∀ (ι₃ : K₃ →ₗ[R] M₃) (hι₃ : Function.Exact ⇑ι₃ ⇑i₃) (π₁ : N₁ →ₗ[R] C₁) (hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
      (hf₂ : Function.Surjective ⇑f₂) (hg₁ : Function.Injective ⇑g₁) (F : K₂ →ₗ[R] K₃), ⋯ = ⋯ → ⋯ → ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.all_eq_true : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {p : α → β → Bool},
  (↑m).WF →
    ((↑m).all p = true ↔
      ∀ (a : α) (h : m.contains a = true), p (m.getKey a h) (Std.DHashMap.Internal.Raw₀.Const.get m a h) = true)
-- Mathlib.Data.Fin.Parity
Fin.not_even_iff_odd_of_even : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Even n → (¬Even k ↔ Odd k)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getToIntId : Lean.Meta.Grind.Arith.Cutsat.ToIntM ℕ
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instInterOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Inter (Std.ExtDHashMap α β)
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that right-closed ranges \(i.e., for bounds `a` and `b`,
`a...=b`, `a<...=b` and `*...=b`\) are always finite.
This is a prerequisite for many functions and instances, such as
`Rcc.toList` or `ForIn'`.
 -/
Std.Rxc.IsAlwaysFinite : (α : Type u) → [Std.PRange.UpwardEnumerable α] → [LE α] → Prop
-- Std.Data.HashSet.Lemmas
Std.HashSet.empty_equiv_iff_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  ∅.Equiv m ↔ m.isEmpty = true
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
RootPairing.GeckConstruction.isNilpotent_e : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CharZero R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [inst_7 : P.IsCrystallographic] [P.IsReduced] {b : P.Base} [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (i : ↥b.support), IsNilpotent (RootPairing.GeckConstruction.e i)
-- Mathlib.Data.Finset.Grade
CovBy.exists_finset_insert : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⋖ t → ∃ a ∉ s, insert a s = t
-- Mathlib.Data.Finsupp.WellFounded
/-- Transferred from `DFinsupp.Lex.acc`. See the top of that file for an explanation for the
appearance of the relation `rᶜ ⊓ (≠)`.  -/
Finsupp.Lex.acc : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] {r : α → α → Prop} {s : N → N → Prop},
  (∀ ⦃n : N⦄, ¬s n 0) →
    WellFounded s → ∀ (x : α →₀ N), (∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) a) → Acc (Finsupp.Lex r s) x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldl.eq_1 : ∀ {σ : Sort u_1} {α : Type u_2} (f : σ → α → σ) (x : σ), RBTree.RBNode.Stream.foldl f x RBTree.RBNode.Stream.nil = x
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
/-- A path in the groupoid defines an isomorphism between its endpoints.
 -/
CategoryTheory.Groupoid.vertexGroupIsomOfPath : {C : Type u} → [inst : CategoryTheory.Groupoid C] → {c d : C} → Quiver.Path c d → (c ⟶ c) ≃* (d ⟶ d)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Return the minimum element of the tree, or the provided default value.

```
findMin' 37 {1, 2, 3} = 1
findMin' 37 ∅ = 37
```  -/
Ordnode.findMin' : {α : Type u_1} → Ordnode α → α → α
-- Lean.LocalContext
Lean.LocalContext.setBinderInfo : Lean.LocalContext → Lean.FVarId → Lean.BinderInfo → Lean.LocalContext
-- Mathlib.Data.Analysis.Topology
/-- Map a Ctop to an equivalent representation type.  -/
Ctop.ofEquiv : {α : Type u_1} → {σ : Type u_3} → {τ : Type u_4} → σ ≃ τ → Ctop α σ → Ctop α τ
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.instDecidableLECastMode : DecidableLE Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.Analysis.SpecificLimits.Normed
tsum_choose_mul_geometric_of_norm_lt_one : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜},
  ‖r‖ < 1 → ∑' (n : ℕ), ↑((n + k).choose k) * r ^ n = 1 / (1 - r) ^ (k + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.inr_opProdIsoCoprod_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op (A ⨯ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd.op h
-- Mathlib.GroupTheory.Finiteness
/-- An additive group is finitely generated if and only
if it is finitely generated as an additive monoid.  -/
AddGroup.fg_iff_addMonoid_fg : ∀ {G : Type u_3} [inst : AddGroup G], AddGroup.FG G ↔ AddMonoid.FG G
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The identity oplax transformation.  -/
CategoryTheory.Lax.OplaxTrans.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → (F : CategoryTheory.LaxFunctor B C) → CategoryTheory.Lax.OplaxTrans F F
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticRelatedInformation.default : Lean.Lsp.DiagnosticRelatedInformation
-- Mathlib.Data.Set.Countable
Set.Countable.mono : ∀ {α : Type u} {s₁ s₂ : Set α}, s₁ ⊆ s₂ → s₂.Countable → s₁.Countable
-- Mathlib.Order.Closure
LowerAdjoint.closureOperator_isClosed : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α),
  l.closureOperator.IsClosed x = ((fun x => u (l.toFun x)) x = x)
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The map on valuation subrings to their principal unit groups is an order embedding.  -/
ValuationSubring.principalUnitGroupOrderEmbedding : {K : Type u} → [inst : Field K] → ValuationSubring K ↪o (Subgroup Kˣ)ᵒᵈ
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.derivative_det_one_add_X_smul_aux : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} (M : Matrix (Fin n) (Fin n) R),
  Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace
-- Init.Data.Int.DivMod.Lemmas
Int.add_ediv : ∀ {a b c : ℤ}, c ≠ 0 → (a + b) / c = a / c + b / c + if ↑c.natAbs ≤ a % c + b % c then c.sign else 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion
    (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g).snd
-- Mathlib.Tactic.Push
/-- `pull c` rewrites the goal by pulling the constant `c` closer to the head of the expression.
For instance, `pull _ ∈ _` rewrites `x ∈ y ∨ ¬ x ∈ z` into `x ∈ y ∪ zᶜ`.
More precisely, the `pull` tactic repeatedly rewrites an expression by applying lemmas
of the form `... (c ...) = c ...` (where `c` can appear 1 or more times on the left hand side).
`pull` is the inverse tactic to `push`. To extend the `pull` tactic, you can tag a lemma
with the `@[push]` attribute. `pull` works as both a tactic and a conv tactic.

A lemma is considered a `pull` lemma if its reverse direction is a `push` lemma
that actually moves the given constant away from the head. For example
- `not_or : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q` is a `pull` lemma, but `not_not : ¬ ¬ p ↔ p` is not.
- `log_mul : log (x * y) = log x + log y` is a `pull` lemma, but `log_abs : log |x| = log x` is not.
- `Pi.mul_def : f * g = fun (i : ι) => f i * g i` and `Pi.one_def : 1 = fun (x : ι) => 1` are both
  `pull` lemmas for `fun`, because every `push fun _ ↦ _` lemma is also considered a `pull` lemma.

TODO: define a `@[pull]` attribute for tagging `pull` lemmas that are not `push` lemmas.

* `pull _ ~ _` pulls the operator or relation `~`.
* `pull c at l1 l2 ...` rewrites at the given locations.
* `pull c at *` rewrites at all hypotheses and the goal.
* `pull (disch := tac) c` uses the tactic `tac` to discharge any hypotheses for `@[push]` lemmas.

Examples:
* `pull _ ∈ _` rewrites `x ∈ y ∨ ¬ x ∈ z` into `x ∈ y ∪ zᶜ`.
* `pull (disch := positivity) Real.log` rewrites `log a + 2 * log b` into `log (a * b ^ 2)`.
* `pull fun _ ↦ _` rewrites `f ^ 2 + 5` into `fun x => f x ^ 2 + 5` where `f` is a function.
 -/
Mathlib.Tactic.Push.pull : Lean.ParserDescr
-- Mathlib.Order.Hom.Bounded
/-- Morphisms preserve the top element. The preferred spelling is `_root_.map_top`.  -/
BoundedOrderHomClass.map_top : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : LE α} {inst_1 : LE β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedOrderHomClass F α β] (f : F), f ⊤ = ⊤
-- Mathlib.Data.Finset.Basic
Finset.disjoint_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.span_orbit_mem_invtSubmodule : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {G : Type u_3}
  [inst_3 : Monoid G] [inst_4 : DistribMulAction G M] [inst_5 : SMulCommClass G R M] (x : M) (g : G),
  Submodule.span R (MulAction.orbit G x) ∈ Module.End.invtSubmodule (DistribSMul.toLinearMap R M g)
-- Mathlib.Topology.Order.LocalExtr
/-- `IsLocalMinOn f s a` means that `f a ≤ f x` for all `x ∈ s` in some neighborhood of `a`.  -/
IsLocalMinOn : {α : Type u} → {β : Type v} → [TopologicalSpace α] → [Preorder β] → (α → β) → Set α → α → Prop
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Algebra F),
  CategoryTheory.Endofunctor.Algebra.Hom.f 0 = 0
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- A one-element space is terminal in `CompHaus`  -/
CompHausLike.isTerminalPUnit : {P : TopCat → Prop} →
  [inst : CompHausLike.HasProp P PUnit.{u + 1}] → CategoryTheory.Limits.IsTerminal (CompHausLike.of P PUnit.{u + 1})
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.quasiIsoAt_shift_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n i j : ℤ),
  n + i = j →
    (QuasiIsoAt ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ) i ↔ QuasiIsoAt φ j)
-- Mathlib.Data.Finsupp.Sigma
/-- Embed a finitely supported function `f : ι k →₀ M` into the `k`-th summand
of the sigma type `(Σ k, ι k) →₀ M`.

This is `Finsupp.embDomain` specialized to `Function.Embedding.sigmaMk k`.  -/
Finsupp.embSigma : {κ : Type u_1} → {ι : κ → Type u_2} → {M : Type u_3} → [inst : Zero M] → {k : κ} → (ι k →₀ M) → (k : κ) × ι k →₀ M
-- Mathlib.Order.Basic
/-- **Alias** of `gt_trans`. -/
LT.lt.trans' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b < a → c < b → c < a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, for all `x₁ : M` and `y₁ ∈ S`,
if `x₂ : M, y₂ ∈ S` are such that `f x₁ * (f y₁)⁻¹ * f y₂ = f x₂`, then there exists `c ∈ S`
such that `x₁ * y₂ * c = x₂ * y₁ * c`.  -/
Submonoid.LocalizationMap.exists_of_sec_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), ∃ c, ↑c * (↑(f.sec (f.mk' x y)).2 * x) = ↑c * (↑y * (f.sec (f.mk' x y)).1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, t.getKey? (t.minKey he) = some (t.minKey he)
-- Lean.Parser.Term
Lean.Parser.Term.dotIdent : Lean.Parser.Parser
-- Mathlib.Data.Num.Bitwise
PosNum.shiftl_eq_shiftLeft : ∀ (p : PosNum) (n : ℕ), p.shiftl n = p <<< n
-- Mathlib.LinearAlgebra.Transvection.Generation
/-- If an element `e : V ≃ₗ[K] V` is such that `e.fixedReduce`
is not a homothety, then `e` is the product of at
most `finrank K (V ⧸ e.fixedSubmodule) - 1` transvections
and one dilatransvection.

This is the second non-exceptional case in Dieudonné's theorem.  -/
LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_fixedReduce_ne_smul_id : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {e : V ≃ₗ[K] V},
  (∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x) →
    e ∈
      LinearEquiv.transvections K V ^ (Module.finrank K (V ⧸ (↑e).fixedSubmodule) - 1) *
        LinearEquiv.dilatransvections K V
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toBialgHom_toAlgHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ↑↑e = ↑e.toAlgEquiv
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasProd.even_mul_odd : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousMul M] {f : ℕ → M},
  HasProd (fun k => f (2 * k)) m → HasProd (fun k => f (2 * k + 1)) m' → HasProd f (m * m')
-- Mathlib.Order.Cover
ofDual_covBy_ofDual_iff : ∀ {α : Type u_1} [inst : LT α] {a b : αᵒᵈ}, OrderDual.ofDual a ⋖ OrderDual.ofDual b ↔ b ⋖ a
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver : ∀ (R : Type u_2) [inst : CommSemiring R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Ideal R)
  (P : Ideal A) [P.IsPrime] [P.LiesOver p], (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R A) p)) P).IsPrime
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by all the matrices in `listTransvecCol M` kills all the coefficients in the
last column but the last one.  -/
Matrix.Pivot.listTransvecCol_mul_last_col : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
    ∀ (i : Fin r), ((Matrix.Pivot.listTransvecCol M).prod * M) (Sum.inl i) (Sum.inr ()) = 0
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
instPartialOrderHomogeneousSubmodule : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {σA : Type u_3} →
      {σM : Type u_4} →
        {A : Type u_5} →
          {M : Type u_6} →
            [inst : Semiring A] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module A M] →
                  (𝒜 : ιA → σA) →
                    (ℳ : ιM → σM) →
                      [inst_3 : DecidableEq ιA] →
                        [inst_4 : AddMonoid ιA] →
                          [inst_5 : SetLike σA A] →
                            [inst_6 : AddSubmonoidClass σA A] →
                              [inst_7 : GradedRing 𝒜] →
                                [inst_8 : DecidableEq ιM] →
                                  [inst_9 : SetLike σM M] →
                                    [inst_10 : AddSubmonoidClass σM M] →
                                      [inst_11 : DirectSum.Decomposition ℳ] →
                                        [inst_12 : VAdd ιA ιM] →
                                          [inst_13 : SetLike.GradedSMul 𝒜 ℳ] → PartialOrder (HomogeneousSubmodule 𝒜 ℳ)
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then
it is analytic at every point of this ball.  -/
HasFPowerSeriesOnBall.analyticAt_of_mem : ∀ {𝕜 : 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] [CompleteSpace F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x y : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → y ∈ Metric.eball x r → AnalyticAt 𝕜 f y
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `c * X`
has Gaussian law with mean `c * μ` and variance `c ^ 2 * v`.  -/
ProbabilityTheory.gaussianReal_const_mul : ∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ∀ (c : ℝ),
      ProbabilityTheory.HasLaw (fun ω => c * X ω) (ProbabilityTheory.gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)) P
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.contains.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α),
  Std.DHashMap.Internal.AssocList.contains a Std.DHashMap.Internal.AssocList.nil = false
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.extend_function_finite : ∀ {α : Type u} {β : Type v} [Finite α] {s : Set α} (f : ↑s ↪ β), Nonempty (α ≃ β) → ∃ g, ∀ (x : ↑s), g ↑x = f x
-- Mathlib.Data.Vector.Basic
/-- Apply an applicative function to each component of a vector.  -/
List.Vector.traverse : {n : ℕ} → {F : Type u → Type u} → [Applicative F] → {α β : Type u} → (α → F β) → List.Vector α n → F (List.Vector β n)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Given a morphism `h : Y ⟶ X`, send a sieve S on X to a sieve on Y
as the inverse image of S with `_ ≫ h`. That is, `Sieve.pullback S h := (≫ h) '⁻¹ S`.  -/
CategoryTheory.Sieve.pullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (Y ⟶ X) → CategoryTheory.Sieve X → CategoryTheory.Sieve Y
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.div_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  MonovaryOn f₁ g s → AntivaryOn f₂ g s → MonovaryOn (f₁ / f₂) g s
-- Lean.Language.Basic
/-- Returns a task that waits on all snapshots in the tree.  -/
Lean.Language.SnapshotTree.waitAll : Lean.Language.SnapshotTree → BaseIO (Task Unit)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- To show two paths equal it suffices to show that they have the same edges.  -/
SSet.Truncated.Path.ext' : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} {m : ℕ} {f g : X.Path (m + 1)},
  (∀ (i : Fin (m + 1)), f.arrow i = g.arrow i) → f = g
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseBPeriod : String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool}
  {k : α}, (Std.TreeMap.filter (fun k x => f k) t).getKey? k = Option.filter f (t.getKey? k)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.lastDart_toProd : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil), (p.lastDart hp).toProd = (p.penultimate, w)
-- Mathlib.Order.RelIso.Set
Subrel.coe_inclusionEmbedding : ∀ {α : Type u_1} (r : α → α → Prop) {s t : Set α} (h : s ⊆ t), ⇑(Subrel.inclusionEmbedding r h) = Set.inclusion h
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
/-- If `A` is an `R`-algebra, then a continuous `A`-linear map can be interpreted as a continuous
`R`-linear map. We assume `LinearMap.CompatibleSMul M₁ M₂ R A` to match assumptions of
`LinearMap.map_smul_of_tower`.  -/
ContinuousLinearMap.restrictScalars : {A : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      (R : Type u_4) →
        [inst : Semiring A] →
          [inst_1 : Semiring R] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : Module A M₁] →
                [inst_4 : Module R M₁] →
                  [inst_5 : TopologicalSpace M₁] →
                    [inst_6 : AddCommMonoid M₂] →
                      [inst_7 : Module A M₂] →
                        [inst_8 : Module R M₂] →
                          [inst_9 : TopologicalSpace M₂] →
                            [LinearMap.CompatibleSMul M₁ M₂ R A] → (M₁ →L[A] M₂) → M₁ →L[R] M₂
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionObj : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : Dᵒᵖ) (d : Cᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj c d =
    Opposite.op
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (Opposite.unop c) (Opposite.unop d))
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {B : Set (TopologicalSpace.Opens ↑X)},
  TopologicalSpace.Opens.IsBasis B →
    ∀ {F G : TopCat.Presheaf C X} {α : F ⟶ G},
      (∀ U ∈ B, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U)))) →
        ∀ (x : ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map α))
-- Mathlib.Topology.SmallInductiveDimension
_private.Mathlib.Topology.SmallInductiveDimension.0.hasSmallInductiveDimensionLE_of_smallInductiveDimension_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ}, smallInductiveDimension X ≤ ↑n → HasSmallInductiveDimensionLE X n
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj.homEquiv_apply : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {C : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_3} C]
  (F : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) C),
  CategoryTheory.ReflQuiv.adj.homEquiv F = CategoryTheory.Cat.toFreeRefl V ⋙rq F.toReflPrefunctor
-- Mathlib.Algebra.Group.Action.Pretransitive
AddAction.IsPretransitive.of_vadd_eq : ∀ {M : Type u_5} {N : Type u_6} {α : Type u_7} [inst : VAdd M α] [inst_1 : VAdd N α] [AddAction.IsPretransitive M α]
  (f : M → N), (∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x) → AddAction.IsPretransitive N α
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.continuous_iteratedLineDerivOp : ∀ {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] [inst_1 : TopologicalSpace E] [ContinuousLineDeriv V E E]
  {n : ℕ} (m : Fin n → V), Continuous (LineDeriv.iteratedLineDerivOp m)