mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.Corner.Defs
isCornerFree_empty : ∀ {G : Type u_1} [inst : AddCommMonoid G], IsCornerFree ∅
-- Mathlib.LinearAlgebra.Multilinear.DirectSum
/-- Prefer using `fromDirectSumEquiv_lof` where possible.  -/
MultilinearMap.fromDirectSumEquiv_apply : ∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] [inst_7 : (i : ι) → DecidableEq (κ i)]
  [inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) M')
  (x : DirectSum ι fun i => DirectSum (κ i) fun j => M i j),
  (MultilinearMap.fromDirectSumEquiv f) ⇑x =
    ∑ p ∈ Fintype.piFinset fun i => DFinsupp.support (x i), (f p) fun i => (x i) (p i)
-- Lean.Parser.Term
Lean.Parser.Term.motive.formatter : Lean.PrettyPrinter.Formatter
-- Std.Async.Basic
Std.Async.MaybeTask.ofTask : {α : Type} → Task α → Std.Async.MaybeTask α
-- Init.Data.SInt.Lemmas
ISize.toUSize_mul : ∀ (a b : ISize), (a * b).toUSize = a.toUSize * b.toUSize
-- Mathlib.GroupTheory.GroupAction.Basic
/-- If a subgroup acts nontrivially, then the type is nontrivial.  -/
AddAction.nontrivial_of_fixedPoints_ne_univ : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.fixedPoints G α ≠ Set.univ → Nontrivial α
-- Mathlib.Analysis.Complex.Conformal
/-- A real continuous linear map on the complex plane is conformal if and only if the map or its
conjugate is complex linear, and the map is nonvanishing.  -/
isConformalMap_iff_is_complex_or_conj_linear : ∀ {g : ℂ →L[ℝ] ℂ},
  IsConformalMap g ↔
    ((∃ map, ContinuousLinearMap.restrictScalars ℝ map = g) ∨
        ∃ map, ContinuousLinearMap.restrictScalars ℝ map = g ∘SL ↑Complex.conjCLE) ∧
      g ≠ 0
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingalePart_add_ae_eq : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E]
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f g : ℕ → Ω → E},
  MeasureTheory.Martingale f ℱ μ →
    (MeasureTheory.StronglyAdapted ℱ fun n => g (n + 1)) →
      g 0 = 0 →
        (∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) → ∀ (n : ℕ), MeasureTheory.martingalePart (f + g) ℱ μ n =ᵐ[μ] f n
-- Mathlib.Tactic.Linter.UnusedTactic
/-- The main entry point to the unused tactic linter.  -/
_private.Mathlib.Tactic.Linter.UnusedTactic.0.Mathlib.Linter.UnusedTactic.unusedTacticLinter : Lean.Linter
-- Mathlib.RingTheory.RingHom.Surjective
Localization.awayMap.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (f : R →+* P) (r : R),
  Localization.awayMap f r = IsLocalization.Away.map (Localization.Away r) (Localization.Away (f r)) f r
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.iUnion_eq : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}, π.IsPartition → π.iUnion = ↑I
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Option (γ a)}, t.WF → (Std.DTreeMap.Internal.Impl.filterMap f t h).impl.WF
-- Mathlib.Analysis.Normed.Operator.Basic
/-- If `‖x‖ = 0` and `f` is continuous then `‖f x‖ = 0`.  -/
norm_image_of_norm_eq_zero : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {𝓕 : Type u_8} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
  [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕), Continuous ⇑f → ∀ {x : E}, ‖x‖ = 0 → ‖f x‖ = 0
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.throwUnknownId : Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.continuousOn_exp : ∀ {s : Set ℝ}, ContinuousOn Real.exp s
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelSectLOfProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (b : β) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.IsZeroOrMarkovKernel (κ.sectL b)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findSome?_toList : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id]
  [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Option γ},
  List.findSome? f it.toList = it.findSome? f
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isAdjointPair_iff_comp_eq_compl₂ : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] [inst_5 : AddCommMonoid M₃]
  [inst_6 : Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃} {f : M →ₗ[R] M₁}
  {g : M₁ →ₗ[R] M}, B.IsAdjointPair B' ⇑f ⇑g ↔ B' ∘ₗ f = B.compl₂ g
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.comp.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [inst : SMul M X]
  {Y : Type u_6} [inst_1 : SMul N Y] {Z : Type u_7} [inst_2 : SMul P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y)
  [κ : CompTriple φ ψ χ], g.comp f = { toFun := fun x => g (f x), map_smul' := ⋯ }
-- Aesop.Forward.State
/-- Extract stats from a `ForwardState`.  -/
Aesop.ForwardState.stats : Aesop.ForwardState → Aesop.ForwardStateStats
-- Mathlib.MeasureTheory.Measure.Trim
/-- Restriction of a measure to a sub-σ-algebra.
It is common to see a measure `μ` on a measurable space structure `m0` as being also a measure on
any `m ≤ m0`. Since measures in mathlib have to be trimmed to the measurable space, `μ` itself
cannot be a measure on `m`, hence the definition of `μ.trim hm`.

This notion is related to `OuterMeasure.trim`, see the lemma
`toOuterMeasure_trim_eq_trim_toOuterMeasure`.  -/
MeasureTheory.Measure.trim : {α : Type u_1} → {m m0 : MeasurableSpace α} → MeasureTheory.Measure α → m ≤ m0 → MeasureTheory.Measure α
-- Mathlib.Data.Set.Prod
Set.disjoint_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} [∀ (i : ι), Nonempty (α i)],
  Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i)
-- Mathlib.LinearAlgebra.Reflection
Module.involutive_preReflection : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M}, f x = 2 → Function.Involutive ⇑(Module.preReflection x f)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.canonicallyOverPullback_over : ∀ {M S T : AlgebraicGeometry.Scheme} [inst : M.Over S] {f : T ⟶ S},
  CategoryTheory.Limits.pullback (M ↘ S) f ↘ T = CategoryTheory.Limits.pullback.snd (M ↘ S) f
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_left_mem_nonZeroDivisors_eq_zero_iff : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {r x : M₀}, r ∈ nonZeroDivisors M₀ → (r * x = 0 ↔ x = 0)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.finite_co_support : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (g : Γ), Function.HasFiniteSupport fun a => (s a).coeff g
-- Mathlib.Analysis.Normed.Group.Real
tendsto_norm_atTop_atTop : Filter.Tendsto norm Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multispan_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) (a : J.L),
  I.multispan.obj (CategoryTheory.Limits.WalkingMultispan.left a) = I.left a
-- Mathlib.Order.Filter.Pointwise
Filter.div_eq_bot_iff : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α}, f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Mathlib.Analysis.Meromorphic.Order
/-- Meromorphic functions that agree in a punctured neighborhood of `z₀` have the same order at
`z₀`.  -/
meromorphicOrderAt_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜},
  f₁ =ᶠ[nhdsWithin x {x}ᶜ] f₂ → meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Determine for each argument whether it should be ignored,
and return a list consisting of one `StackEntry` for each argument.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.getStackEntries : Lean.Expr → Array Lean.Expr → List Lean.FVarId → Lean.MetaM (List Lean.Meta.RefinedDiscrTree.StackEntry)
-- Mathlib.Data.Nat.Periodic
/-- An interval of length `a` filtered over a periodic predicate of period `a` has cardinality
equal to the number naturals below `a` for which `p a` is true.  -/
Nat.filter_Ico_card_eq_of_periodic : ∀ (n a : ℕ) (p : ℕ → Prop) [inst : DecidablePred p],
  Function.Periodic p a → (Finset.filter p (Finset.Ico n (n + a))).card = Nat.count p a
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.toCycles_i : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (X.iCycles f g n) =
    (X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_lt_lineMap_iff_of_lt' : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r r' : k},
  a < b → ((AffineMap.lineMap a b) r < (AffineMap.lineMap a b) r' ↔ r < r')
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_finite_iff : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ),
  Dynamics.netMaxcard T F U n < ⊤ ↔ ∃ s, Dynamics.IsDynNetIn T F U n ↑s ∧ ↑s.card = Dynamics.netMaxcard T F U n
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.forIn'Unsafe.loop : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} →
      [Monad m] → (as : Array α) → ((a : α) → a ∈ as → β → m (ForInStep β)) → USize → USize → β → m β
-- Init.Data.ByteArray.Basic
/-- An efficient implementation of a monadic left fold on for `ByteArray` that uses `USize`
rather than `Nat` for indices.

We claim this unsafe implementation is correct because an array cannot have more than
`USize.size` elements in our runtime. This is similar to the `Array` version.
 -/
ByteArray.foldlMUnsafe : {β : Type v} →
  {m : Type v → Type w} → [Monad m] → (β → UInt8 → m β) → β → (as : ByteArray) → optParam ℕ 0 → optParam ℕ as.size → m β
-- Mathlib.Order.Monotone.Monovary
Monovary.comp_antitone_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Monovary f g → Antitone f' → Antivary (f' ∘ f) g
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right]
  (a :
    CategoryTheory.Limits.Fork
      (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))
      (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))),
  (I.multiforkEquivPiFork.inverse.obj a).pt = a.pt
-- Mathlib.Data.Set.Sups
Set.infs_self_subset : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, s ⊼ s ⊆ s ↔ InfClosed s
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp S.pOpcycles h.opcyclesIso.hom = h.p
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.map_equivFun : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [inst_5 : Finite ι] (b : Module.Basis ι R M)
  (f : M ≃ₗ[R] M'), (b.map f).equivFun = f.symm ≪≫ₗ b.equivFun
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoidClass.coe_finsetSum : ∀ {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : SetLike B M]
  [inst_2 : AddSubmonoidClass B M] (f : ι → ↥S) (s : Finset ι), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Batteries.Data.AssocList
Batteries.AssocList.beq.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β] (key : α) (value : β) (tail : Batteries.AssocList α β),
  (Batteries.AssocList.cons key value tail).beq Batteries.AssocList.nil = false
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.minKey?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.minKey? = t₂.minKey?
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_ne_zero_of_pos_of_ne_one_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 0 < x → x ≠ 1 → Real.logb b x ≠ 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k fallback : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => (f x (m.get x ⋯)).isSome).getD fallback
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.instIsScalarTower : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K], IsScalarTower R K (IsDedekindDomain.FiniteAdeleRing R K)
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Pons asinorum**, vector angle form.  -/
InnerProductGeometry.angle_sub_eq_angle_sub_rev_of_norm_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  ‖x‖ = ‖y‖ → InnerProductGeometry.angle x (x - y) = InnerProductGeometry.angle y (y - x)
-- Batteries.Data.List.Scan
List.partialSums_nil : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α], [].partialSums = [0]
-- Mathlib.GroupTheory.Perm.DomMulAct
/-- The `MulEquiv` from the `MulOpposite` of `MulAction.stabilizer (Perm α)ᵈᵐᵃ f`
to the product of the `Equiv.Perm {a // f a = i}`  -/
DomMulAct.stabilizerMulEquiv : {α : Type u_1} →
  {ι : Type u_2} →
    (f : α → ι) → (↥(MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f))ᵐᵒᵖ ≃* ((i : ι) → Equiv.Perm { a // f a = i })
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.neg_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} (h : W'.Nonsingular x y),
  -WeierstrassCurve.Affine.Point.some x y h = WeierstrassCurve.Affine.Point.some x (W'.negY x y) ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α}, t.getKey! a = t.getKeyD a default
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Two bases are equal if their basis vectors are the same.  -/
Module.Basis.eq_of_apply_eq : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {b₁ b₂ : Module.Basis ι R M}, (∀ (i : ι), b₁ i = b₂ i) → b₁ = b₂
-- Mathlib.Topology.Category.Stonean.EffectiveEpi
Stonean.instPreregular : CategoryTheory.Preregular Stonean
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The canonical basis on the `CotangentSpace`.  -/
Algebra.Generators.cotangentSpaceBasis : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type w} → (P : Algebra.Generators R S ι) → Module.Basis ι S P.toExtension.CotangentSpace
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.AncestralRel.dim_le : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} [P.IsProper] {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim ≤ (↑y).dim
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α],
  t.WF →
    ∀ {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (t.insertMany l).getKey! k = t.getKey! k
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS₂.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ),
  complEDS₂ b c d k =
    (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
        preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
      if Even k then 1 else b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α} {h' : k ∈ Std.TreeMap.filterMap f t},
  (Std.TreeMap.filterMap f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Topology.Algebra.Order.Group
Continuous.mabs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G}, Continuous f → Continuous fun x => |f x|ₘ
-- Mathlib.RingTheory.LocalProperties.IntegrallyClosed
IsIntegrallyClosed.iInf : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {ι : Type u_3} (S : ι → Subalgebra R K), (∀ (i : ι), IsIntegrallyClosed ↥(S i)) → IsIntegrallyClosed ↥(⨅ i, S i)
-- Init.Data.Fin.Lemmas
Fin.mul_one : ∀ {n : ℕ} [i : NeZero n] (k : Fin n), k * 1 = k
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isSome_getElem?_eq_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m[a]?.isSome = m.contains a
-- Init.Data.String.Slice
/-- Interprets a slice as the decimal representation of a natural number, returning it. Returns
`none` if the slice does not contain a decimal natural number.

A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
it are digits. Underscores \(`_`\) are allowed as digit separators and are ignored during parsing.

Use `isNat` to check whether `toNat?` would return `some`.
`toNat!` is an alternative that panics instead of
returning `none` when the slice is not a natural number.

Examples:

* `"".toSlice.toNat? = none`

* `"0".toSlice.toNat? = some 0`

* `"5".toSlice.toNat? = some 5`

* `"587".toSlice.toNat? = some 587`

* `"1_000".toSlice.toNat? = some 1000`

* `"100_000_000".toSlice.toNat? = some 100000000`

* `"-587".toSlice.toNat? = none`

* `" 5".toSlice.toNat? = none`

* `"2+3".toSlice.toNat? = none`

* `"0xff".toSlice.toNat? = none`
 -/
String.Slice.toNat? : String.Slice → Option ℕ
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.finrank_eq_of_rank_eq : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  Module.rank R M = ↑n → Module.finrank R M = n
-- Mathlib.Data.Int.Cast.Defs
AddCommGroupWithOne.toOne : {R : Type u} → [self : AddCommGroupWithOne R] → One R
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.nonReservedSymbolNoAntiquot.parenthesizer : String → Lean.PrettyPrinter.ParenthesizerM Unit
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'}
  {h' h₂' : 𝕜'},
  HasDerivWithinAt h₂ h₂' s' (h x) →
    HasDerivWithinAt h h' s x → Set.MapsTo h s s' → HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
-- Init.Meta.Defs
/-- Converts a name to a string.

- If `escape` is `true`, then escapes name components using `«` and `»` to ensure that
those names that can appear in source files round trip.
Names with number components, anonymous names, and names containing `»` might not round trip.
Furthermore, "pseudo-syntax" produced by the delaborator, such as `_`, `#0` or `?u`, is not escaped.
 -/
_private.Init.Meta.Defs.0.Lean.Name.Internal.Meta.toString : Lean.Name → optParam Bool true → String
-- Mathlib.Topology.Order.OrderClosed
Continuous.max : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f g : β → α}
  [inst_3 : TopologicalSpace β], Continuous f → Continuous g → Continuous fun b => max (f b) (g b)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'_hom_app : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (X : ModuleCat R₃),
  (ModuleCat.restrictScalarsComp' f g gf hgf).hom.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).hom
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- The property of reflecting coproducts expressed in terms of cofans.  -/
CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Discrete.functor f) G] →
                {P : C} →
                  (g : (j : J) → f j ⟶ P) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j)) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk P g)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- If the bottom-left element of a block matrix is invertible, then the whole matrix is invertible
iff the corresponding Schur complement is.  -/
Matrix.isUnit_fromBlocks_iff_of_invertible₂₂ : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
  {D : Matrix n n α} [inst_5 : Invertible D], IsUnit (Matrix.fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C)
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- The covariance matrix of the finite dimensional distribution of the Brownian motion
indexed by `I`.  -/
ProbabilityTheory.BrownianReal.covMatrix : (I : Finset NNReal) → Matrix ↥I ↥I ℝ