mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.Card
Fintype.card_pos : ∀ {α : Type u_1} [inst : Fintype α] [h : Nonempty α], 0 < Fintype.card α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_inverse_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T),
  ((CategoryTheory.StructuredArrow.mapIso i).inverse.obj X).left = X.left
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_erase_lt_of_one_lt : ∀ {ι : Type u_1} {κ : Type u_5} [inst : DecidableEq ι] [inst_1 : CommMonoid κ] [inst_2 : LT κ] [MulLeftStrictMono κ]
  {s : Finset ι} {d : ι}, d ∈ s → ∀ {f : ι → κ}, 1 < f d → ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m
-- Batteries.Data.Vector.Lemmas
Vector.get_push_castSucc : ∀ {α : Type u_1} {n : ℕ} (v : Vector α n) (a : α) (i : Fin n), (v.push a).get i.castSucc = v.get i
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_empty : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε], MeasureTheory.IntegrableOn f ∅ μ
-- Mathlib.Topology.Neighborhoods
nhds_neBot : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, (nhds x).NeBot
-- Aesop.Tree.Data
Aesop.MVarCluster.isIrrelevant : Aesop.MVarCluster → Bool
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.instHasPullbackRL : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [Wₗ.HasPullbacksAgainst Wᵣ] {c c' c'' : C} (S₁ : CategoryTheory.Span Wₗ Wᵣ c c')
  (S₂ : CategoryTheory.Span Wₗ Wᵣ c' c''), CategoryTheory.Limits.HasPullback S₁.r S₂.l
-- Mathlib.CategoryTheory.Category.Bipointed
/-- Swaps the pointed elements of a bipointed type. `Prod.swap` as a functor.  -/
Bipointed.swap : CategoryTheory.Functor Bipointed Bipointed
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.State.mk.inj : ∀ {patterns : Array Lean.Expr} {done : Bool} {patterns_1 : Array Lean.Expr} {done_1 : Bool},
  { patterns := patterns, done := done } = { patterns := patterns_1, done := done_1 } →
    patterns = patterns_1 ∧ done = done_1
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.refl_apply : ∀ (α : Sort u_1) (a : α), (Function.Embedding.refl α) a = a
-- Mathlib.Order.Interval.Multiset
/-- **Alias** of the reverse direction of `Multiset.Icc_eq_zero_iff`. -/
Multiset.Icc_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a ≤ b → Multiset.Icc a b = 0
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.equivOfNatIso_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).functor =
    CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α.inv
-- Mathlib.GroupTheory.Rank
AddGroup.rank.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] [h : AddGroup.FG G], AddGroup.rank G = Nat.find ⋯
-- Mathlib.Geometry.Manifold.Riemannian.Basic
nnnorm_tangentSpace_vectorSpace : ∀ {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F}
  {v : TangentSpace (modelWithCornersSelf ℝ F) x}, ‖v‖₊ = ‖v‖₊
-- Lean.Meta.Sym.Arith.Types
/-- `Field` instance for `type` if available.  -/
Lean.Meta.Sym.Arith.CommRing.fieldInst? : Lean.Meta.Sym.Arith.CommRing → Option Lean.Expr
-- Mathlib.Analysis.Normed.Group.Pointwise
inv_closedBall : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), (Metric.closedBall x δ)⁻¹ = Metric.closedBall x⁻¹ δ
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An initial object in the opposite category is terminal in the original category.  -/
CategoryTheory.Limits.terminalUnopOfInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : Cᵒᵖ} → CategoryTheory.Limits.IsInitial X → CategoryTheory.Limits.IsTerminal (Opposite.unop X)
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.

This function returns a meaningful value given `LawfulUpwardEnumerable` and
`LawfulUpwardEnumerableLT` instances.
 -/
Std.Roo.isEmpty : {α : Type u} → [inst : LT α] → [DecidableLT α] → [Std.PRange.UpwardEnumerable α] → Std.Roo α → Bool
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsLittleOTVSIsLittleOTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsLittleOTVS 𝕜 l) (Asymptotics.IsLittleOTVS 𝕜 l)
                                  (Asymptotics.IsLittleOTVS 𝕜 l)
-- Std.Data.DTreeMap.Internal.Operations
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.modify : {α : Type u} →
  {β : Type v} →
    [Ord α] → α → (β → β) → (Std.DTreeMap.Internal.Impl α fun x => β) → Std.DTreeMap.Internal.Impl α fun x => β
-- Init.Data.UInt.Lemmas
UInt32.one_def : 1 = { toBitVec := 1 }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.size_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.size = t₂.size
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.dimacs.go : Std.Sat.CNF ℕ → Std.Sat.CNF.DimacsM✝ String
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₂₃_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G) (f : G × G → ↑A) (g : G × G × G),
  (ModuleCat.Hom.hom (groupCohomology.d₂₃ A)) f g =
    (A.ρ g.1) (f g.2) - f (g.1 * g.2.1, g.2.2) + f (g.1, g.2.1 * g.2.2) - f (g.1, g.2.1)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instUniformSpace : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → UniformSpace (SchwartzMap E F)
-- Init.PropLemmas
Decidable.and_or_imp : ∀ {a b c : Prop} [Decidable a], a ∧ b ∨ (a → c) ↔ a → b ∨ c
-- Lean.DocString.Types
Lean.Doc.DescItem.mk.inj : ∀ {α : Type u} {β : Type v} {term : Array α} {desc : Array β} {term_1 : Array α} {desc_1 : Array β},
  { term := term, desc := desc } = { term := term_1, desc := desc_1 } → term = term_1 ∧ desc = desc_1
-- Init.Data.UInt.Lemmas
UInt16.sub_add_cancel : ∀ (a b : UInt16), a - b + b = a
-- Mathlib.Topology.Order.Monotone
MonotoneOn.tendsto_nhdsGT : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α},
  MonotoneOn f (Set.Ioi x) →
    BddBelow (f '' Set.Ioi x) → Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioi x)))
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.swapCompInr_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : D), (CategoryTheory.Sum.swapCompInr C D).inv.app X = CategoryTheory.CategoryStruct.id (Sum.inl X)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.beq_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] [inst_3 : (k : α) → BEq (β k)] {m₃ m₄ : Std.DHashMap.Raw α β},
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_ofENat : ∀ (n : ℕ∞), Cardinal.toENat ↑n = n
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.complexEmbedding_inj : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ) (u v : (NumberField.RingOfIntegers K)ˣ),
  (NumberField.Units.complexEmbedding φ) u = (NumberField.Units.complexEmbedding φ) v ↔ u = v
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_image_indep_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Matroid α} {hf : Set.InjOn f M.E} {I : Set α},
  I ⊆ M.E → ((M.map f hf).Indep (f '' I) ↔ M.Indep I)
-- Mathlib.Data.List.Lattice
List.bagInter_eq_nil_iff_disjoint : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α], l₁.bagInter l₂ = [] ↔ l₁.Disjoint l₂
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from `Expr` to a variable representing it.  -/
Lean.Meta.Grind.Arith.CommRing.Semiring.varMap : Lean.Meta.Grind.Arith.CommRing.Semiring → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsUniversal.below.all : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsUniversal → Prop} {n : ℕ}
  {φ : L.BoundedFormula α (n + 1)} (h : φ.IsUniversal),
  FirstOrder.Language.BoundedFormula.IsUniversal.below h →
    motive φ h → FirstOrder.Language.BoundedFormula.IsUniversal.below ⋯
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mk.sizeOf_spec : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : optParam (Set M) Set.univ} [inst_6 : SizeOf ι]
  [inst_7 : SizeOf E] [inst_8 : SizeOf H] [inst_9 : SizeOf M] [inst_10 : (a : M) → SizeOf (s a)] (c : ι → M)
  (toFun : (i : ι) → SmoothBumpFunction I (c i)) (c_mem' : ∀ (i : ι), c i ∈ s)
  (locallyFinite' : LocallyFinite fun i => Function.support ↑(toFun i))
  (eventuallyEq_one' : ∀ x ∈ s, ∃ i, ↑(toFun i) =ᶠ[nhds x] 1),
  sizeOf
      { c := c, toFun := toFun, c_mem' := c_mem', locallyFinite' := locallyFinite',
        eventuallyEq_one' := eventuallyEq_one' } =
    1
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The valuation ring of a valuative commutative square.  -/
AlgebraicGeometry.ValuativeCommSq.R : {X Y : AlgebraicGeometry.Scheme} → {f : X ⟶ Y} → AlgebraicGeometry.ValuativeCommSq f → Type u
-- Mathlib.RingTheory.Localization.Algebra
IsLocalization.mapₐ_surjective_of_surjective : ∀ {R : Type u_5} [inst : CommSemiring R] (M : Submonoid R) {A : Type u_6} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] {B : Type u_7} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Rₚ : Type u_8)
  [inst_5 : CommSemiring Rₚ] [inst_6 : Algebra R Rₚ] [inst_7 : IsLocalization M Rₚ] (Aₚ : Type u_9)
  [inst_8 : CommSemiring Aₚ] [inst_9 : Algebra R Aₚ] [inst_10 : Algebra A Aₚ] [inst_11 : IsScalarTower R A Aₚ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type u_10) [inst_13 : CommSemiring Bₚ]
  [inst_14 : Algebra R Bₚ] [inst_15 : Algebra B Bₚ] [inst_16 : IsScalarTower R B Bₚ]
  [inst_17 : IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ] [inst_18 : Algebra Rₚ Aₚ] [inst_19 : Algebra Rₚ Bₚ]
  [inst_20 : IsScalarTower R Rₚ Aₚ] [inst_21 : IsScalarTower R Rₚ Bₚ] (f : A →ₐ[R] B),
  Function.Surjective ⇑f → Function.Surjective ⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f)
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.instAbelian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Abelian (CategoryTheory.ShortComplex C)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_symm_toIsometryEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), ⇑e.toIsometryEquiv.symm = ⇑e.symm
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.isIntegrallyClosed_dvd_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {s : S},
  IsIntegral R s → ∀ (p : Polynomial R), (Polynomial.aeval s) p = 0 ↔ minpoly R s ∣ p
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_trans : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃), ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a `PullbackObjObj` of `f₁ : Arrow C₁` and `f₃ : Arrow C₃`, a `PullbackObjObj` of `f₁'` and
`f₃ : Arrow C₃`, and an isomorphism `f₁ ≅ f₁'`, this defines an isomorphism of the induced
pullback maps.  -/
CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_left : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {f₁ f₁' : CategoryTheory.Arrow C₁} →
                {f₃ : CategoryTheory.Arrow C₃} →
                  (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) →
                    (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) →
                      (f₁ ≅ f₁') → (CategoryTheory.Arrow.mk sq₁₃.π ≅ CategoryTheory.Arrow.mk sq₁₃'.π)
-- ProofWidgets.Component.RefreshComponent
/-- Update the current HTML tree to be `html`.

The `html` thunk is only forced when the client requests it;
if another update is made before that, it will never be forced.

This function is thread-safe: each update is made atomically.  -/
ProofWidgets.RefreshToken.updateLazy : ProofWidgets.RefreshToken → Thunk ProofWidgets.Html → BaseIO Unit
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedLength_zero : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  [LieAlgebra.IsSolvable ↥I], LieAlgebra.derivedLengthOfIdeal R L I = 0 ↔ I = ⊥
-- Init.Data.Nat.Lemmas
Nat.one_lt_two_pow' : ∀ (n : ℕ), 1 < 2 ^ (n + 1)
-- Mathlib.Order.Bounds.Image
IsGreatest.image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → IsGreatest s a → IsGreatest t b → IsGreatest (Set.image2 f s t) (f a b)
-- Mathlib.Order.Hom.Basic
OrderHom.uliftMap_coe_down : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (i : ULift.{u_8, u_2} α),
  (f.uliftMap i).down = f i.down
-- Mathlib.Algebra.Divisibility.Prod
pi_dvd_iff : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Semigroup (G i)] {x y : (i : ι) → G i},
  x ∣ y ↔ ∀ (i : ι), x i ∣ y i
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpointType.partialFixpoint : Lean.Elab.PartialFixpointType
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.union m₂).get? k = m₁.get? k
-- Mathlib.Data.Multiset.AddSub
Multiset.count_sub : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
  Multiset.count a (s - t) = Multiset.count a s - Multiset.count a t
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.SeenCalls.mk.inj : ∀ {calls : Array Lean.Expr} {seen : Std.HashSet (Lean.Name × Array Lean.Expr)} {calls_1 : Array Lean.Expr}
  {seen_1 : Std.HashSet (Lean.Name × Array Lean.Expr)},
  { calls := calls, seen := seen } = { calls := calls_1, seen := seen_1 } → calls = calls_1 ∧ seen = seen_1
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_self : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [inst : DecidableEq m],
  M.updateRow i b i = b
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- Probability density function of the Gaussian distribution with mean `μ` and variance `v`.  -/
ProbabilityTheory.gaussianPDFReal : ℝ → NNReal → ℝ → ℝ
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.hasBasis_right_ideal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology Rᵐᵒᵖ R],
  (nhds 0).HasBasis (fun I => ↑I ∈ nhds 0) fun I => ↑I
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofUserWidgetInfo.injEq : ∀ (i i_1 : Lean.Elab.UserWidgetInfo),
  (Lean.Elab.Info.ofUserWidgetInfo i = Lean.Elab.Info.ofUserWidgetInfo i_1) = (i = i_1)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f),
  (F.mapComp' f₀₁ f₁₃ f ⋯).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
          (F.mapComp' f₀₂ f₂₃ f ⋯).inv))
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.category_id_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (x : X.I),
  (CategoryTheory.CategoryStruct.id X).φ x = CategoryTheory.CategoryStruct.id (X.obj x)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instCoeZMod : {q : ℕ} → Coe (ZMod q) (LucasLehmer.X q)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_biUnion`. -/
EMetric.infEdist_biUnion : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ι : Type u_2} (f : ι → Set α) (I : Set ι) (x : α),
  Metric.infEDist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, Metric.infEDist x (f i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₈_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.b₈ = 4 * W.a₂ * W.a₆
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.isClosedSubgraph_iff : ∀ {α : Type u_1} {β : Type u_2} (H G : Graph α β),
  H.IsClosedSubgraph G ↔ H.IsInducedSubgraph G ∧ ∀ ⦃e : β⦄ ⦃x : α⦄, G.Inc e x → x ∈ H.vertexSet → e ∈ H.edgeSet
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_option : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : CommMonoid M] (f : Option α → M),
  ∏ i, f i = f none * ∏ i, f (some i)
-- Lean.Meta.AbstractMVars
/-- Abstracts metavariables in `e`. Assumes `instantiateMVars` has been applied to `e`.
 -/
Lean.Meta.AbstractMVars.abstractExprMVars : Lean.Expr → Lean.Meta.AbstractMVars.M Lean.Expr
-- Mathlib.Algebra.Order.Kleene
IdemCommSemiring.toCommSemiring : {α : Type u_5} → [self : IdemCommSemiring α] → CommSemiring α
-- Mathlib.Data.Finmap
Finmap.extract_eq_lookup_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : Finmap β),
  Finmap.extract a s = (Finmap.lookup a s, Finmap.erase a s)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse_injective : ∀ {T : Type u_1}, Function.Injective ContextFreeGrammar.reverse
-- Mathlib.Algebra.Ring.Parity
odd_add_one : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Odd (a + 1) ↔ Even a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, k ∈ t.insert k v
-- Lean.Message
Lean.MessageDataContext.mctx : Lean.MessageDataContext → Lean.MetavarContext
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ofList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {k : α} {v : β} {tl : List (α × β)},
  Std.DTreeMap.Raw.Const.ofList ((k, v) :: tl) cmp = Std.DTreeMap.Raw.Const.insertMany (∅.insert k v) tl
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.left.sizeOf_spec : ∀ {J : CategoryTheory.Limits.MultispanShape} (a : J.L),
  sizeOf (CategoryTheory.Limits.WalkingMultispan.left a) = 1 + sizeOf a
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- A triangle in `HomotopyCategory C (ComplexShape.up ℤ)` is distinguished if it is isomorphic to
the triangle `CochainComplex.mappingCone.triangleh φ` for some morphism of cochain
complexes `φ`.  -/
HomotopyCategory.Pretriangulated.distinguishedTriangles : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        Set (CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcyclesIso_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (K.pOpcyclesIso i j hi h).inv =
    CategoryTheory.CategoryStruct.id (K.X j)
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandResultSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {cmdState : Lean.Elab.Command.State} {toSnapshot_1 : Lean.Language.Snapshot}
  {cmdState_1 : Lean.Elab.Command.State},
  { toSnapshot := toSnapshot, cmdState := cmdState } = { toSnapshot := toSnapshot_1, cmdState := cmdState_1 } →
    toSnapshot = toSnapshot_1 ∧ cmdState = cmdState_1
-- Mathlib.Analysis.Convex.Combination
convexHull_list_sum : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (l : List (Set E)),
  (convexHull R) l.sum = (List.map (⇑(convexHull R)) l).sum
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rio_eq_mkSlice_rio_min : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ},
  (Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rio.Sliceable.mkSlice xs *...min hi xs.size
-- Mathlib.GroupTheory.Subsemigroup.Center
Subsemigroup.center.eq_1 : ∀ (M : Type u_1) [inst : Mul M], Subsemigroup.center M = { carrier := Set.center M, mul_mem' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.HasReflexiveCoequalizers.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ ⦃A B : C⦄ (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g], CategoryTheory.Limits.HasCoequalizer f g) →
    CategoryTheory.Limits.HasReflexiveCoequalizers C
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_ext : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {f g : M ⟶ N}, ModuleCat.Hom.hom f = ModuleCat.Hom.hom g → f = g
-- Mathlib.Data.Stream.Init
_private.Mathlib.Data.Stream.Init.0.Stream'.take.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → Stream' α → Sort u_2) (x : Stream' α) (h_1 : (x : Stream' α) → motive 0 x)
  (h_2 : (n : ℕ) → (s : Stream' α) → motive n.succ s),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, s => h_2 n s) =
    h_1 x