mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_reindex : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq o]
  [inst_1 : DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : m ≃ l) (f : n ≃ o),
  ((Matrix.reindex e f) A).updateCol j c = (Matrix.reindex e f) (A.updateCol (f.symm j) fun i => c (e i))
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.toListModel.eq_1 : ∀ {α : Type u} {β : α → Type v} (buckets : Array (Std.DHashMap.Internal.AssocList α β)),
  Std.DHashMap.Internal.toListModel buckets = List.flatMap Std.DHashMap.Internal.AssocList.toList buckets.toList
-- Mathlib.Algebra.Polynomial.Div
/-- See `Polynomial.self_mul_modByMonic` for the other multiplication order. This version, unlike
that one, requires commutativity.  -/
Polynomial.mul_self_modByMonic : ∀ {R : Type u} [inst : CommRing R] {p q : Polynomial R}, q.Monic → p * q %ₘ q = 0
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.weightHom_injective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  Function.Injective ⇑(RootPairing.Hom.weightHom P)
-- Mathlib.Topology.EMetricSpace.Defs
uniformity_basis_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ε}
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeMonoid.symbols_of : ∀ {α : Type u_1} [inst : DecidableEq α] {m : α}, (FreeMonoid.of m).symbols = {m}
-- Mathlib.Order.Partition.Basic
Partition.parts_nonempty : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] (P : Partition s), s ≠ ⊥ → (↑P).Nonempty
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionCyclesIso.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (j k : ι) (hk : c.next j = k) {j' k' : ι'}
  (hj' : e.f j = j') (hk' : e.f k = k') (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j],
  K.restrictionCyclesIso e j k hk hj' hk' hk'' =
    {
      hom :=
        K.liftCycles (CategoryTheory.CategoryStruct.comp ((K.restriction e).iCycles j) (K.restrictionXIso e hj').hom) k'
          hk'' ⋯,
      inv :=
        (K.restriction e).liftCycles (CategoryTheory.CategoryStruct.comp (K.iCycles j') (K.restrictionXIso e hj').inv) k
          hk ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Geometry.Convex.Cone.Basic
Submodule.pointed_toConvexCone : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (C : Submodule R M), C.toConvexCone.Pointed
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_filter_of_ne : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} {p : ι → Prop}
  [inst_1 : DecidablePred p], (∀ x ∈ s, f x ≠ 1 → p x) → ∏ x ∈ s with p x, f x = ∏ x ∈ s, f x
-- Mathlib.Data.Int.Cast.Lemmas
eq_intCast : ∀ {F : Type u_1} {α : Type u_3} [inst : NonAssocRing α] [inst_1 : FunLike F ℤ α] [RingHomClass F ℤ α] (f : F) (n : ℤ),
  f n = ↑n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tan_add' : ∀ {x y : ℝ},
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) →
    Real.tan (x + y) = (Real.tan x + Real.tan y) / (1 - Real.tan x * Real.tan y)
-- Mathlib.Topology.Homotopy.Lifting
/-- The lift of a path to a covering space given a lift of the left endpoint.  -/
IsCoveringMap.liftPath : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} → IsCoveringMap p → (γ : C(↑unitInterval, X)) → (e : E) → γ 0 = p e → C(↑unitInterval, E)
-- Mathlib.RingTheory.Jacobson.Semiprimary
IsSemisimpleRing.jacobson_eq_bot : ∀ (R : Type u_1) [inst : Ring R] [IsSemisimpleRing R], Ring.jacobson R = ⊥
-- Init.Data.UInt.Lemmas
USize.toNat_ofNatClamp_of_lt : ∀ {n : ℕ}, n < USize.size → (USize.ofNatClamp n).toNat = n
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_Ioi_norm_cpow_of_lt : ∀ {a : ℂ},
  a.re < -1 → ∀ {c : ℝ}, 0 < c → MeasureTheory.IntegrableOn (fun t => ‖↑t ^ a‖) (Set.Ioi c) MeasureTheory.volume
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.isPerfectMatching_iff_forall_degree : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [inst : (v : V) → Fintype ↑(M.neighborSet v)],
  M.IsPerfectMatching ↔ ∀ (v : V), M.degree v = 1
-- Init.Data.Vector.Erase
Vector.eraseIdx_eq_take_drop_succ : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n),
  xs.eraseIdx i h = Vector.cast ⋯ (xs.take i ++ xs.drop (i + 1))
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.«term_◁_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instDecidableEqObjOppositeSimplexCategoryToSSet : {X : SSet} → (n : SimplexCategoryᵒᵖ) → (A : X.Subcomplex) → [DecidableEq (X.obj n)] → DecidableEq (A.toSSet.obj n)
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight₁_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K], Height.logHeight₁ 1 = 0
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.prod_symm_apply : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)] (x : B) (w₁ : F₁) (w₂ : F₂),
  ↑(e₁.prod e₂).symm (x, w₁, w₂) = ⟨x, (e₁.symm x w₁, e₂.symm x w₂)⟩
-- Mathlib.RingTheory.KrullDimension.Zero
Ideal.jacobson_eq_radical : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [Ring.KrullDimLE 0 R], I.jacobson = I.radical
-- Mathlib.Algebra.CubicDiscriminant
Cubic.mk : {R : Type u_1} → R → R → R → R → Cubic R
-- Std.Data.Internal.List.Associative
/-- Given a proof that the list is nonempty, returns the largest key in an associative list.  -/
Std.Internal.List.maxKey : {α : Type u} → {β : α → Type v} → [Ord α] → (xs : List ((a : α) × β a)) → xs.isEmpty = false → α
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_zero : ∀ {A : Type u_3} {E : Type u_4} [inst : AddCommGroup E], (WithCStarModule.equiv A E) 0 = 0
-- Init.NotationExtra
Lean.calcSteps : Lean.ParserDescr
-- Init.Data.SInt.Lemmas
Int64.mul_sub : ∀ {a b c : Int64}, a * (b - c) = a * b - a * c
-- Mathlib.RingTheory.Localization.BaseChange
/-- The natural isomorphism `S ⊗[R] A[1/g] ≃ (S ⊗[R] A)[1/g]`.  -/
IsLocalization.Away.tensorProductEquivTMulRight : (R : Type u_7) →
  (S : Type u_8) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {A : Type u_9} →
            [inst_3 : CommSemiring A] →
              [inst_4 : Algebra R A] →
                (g : A) →
                  (B : Type u_10) →
                    [inst_5 : CommSemiring B] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra A B] →
                          [IsScalarTower R A B] →
                            [IsLocalization.Away g B] → TensorProduct R S B ≃ₐ[S] Localization.Away (1 ⊗ₜ[R] g)
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.linearIndependent_row_iff : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n R}
  [IsCancelAdd R], LinearIndependent R A.row ↔ A.Nonsingular
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.dec.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {n : ℕ} {check persistent : Bool} {objs? : Option ℕ}
  {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_17} {fvarId_1 : Lean.FVarId}
  {n_1 : ℕ} {check_1 persistent_1 : Bool} {objs?_1 : Option ℕ} {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_17},
  Lean.Compiler.LCNF.Code.dec fvarId n check persistent objs? k h =
      Lean.Compiler.LCNF.Code.dec fvarId_1 n_1 check_1 persistent_1 objs?_1 k_1 h_1 →
    fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1 ∧ objs? = objs?_1 ∧ k = k_1
-- Mathlib.FieldTheory.KummerExtension
isCyclic_of_isSplittingField_X_pow_sub_C : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  (primitiveRoots n K).Nonempty →
    ∀ {a : K},
      Irreducible (Polynomial.X ^ n - Polynomial.C a) →
        ∀ (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
          [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] [NeZero n], IsCyclic Gal(L/K)
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F.rightOp : J ⥤ Cᵒᵖ` into a colimit for `F : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.isColimitCoconeOfConeRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          {c : CategoryTheory.Limits.Cone F.rightOp} →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeRightOp c)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.instMin : {C : Type u} → [inst : CategoryTheory.Groupoid C] → Min (CategoryTheory.Subgroupoid C)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.inter_left : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Set α}, G.IsClique s → ∀ (t : Set α), G.IsClique (s ∩ t)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubOffset_3 : HSub Std.Time.Timestamp Std.Time.Minute.Offset Std.Time.Timestamp
-- Mathlib.SetTheory.Ordinal.Basic
wellFoundedLT_toType : ∀ (o : Ordinal.{u_1}), WellFoundedLT o.ToType
-- Init.Core
/-- `LawfulRightIdentity op o` indicates `o` is a verified right identity of
`op`.
 -/
Std.LawfulRightIdentity : {α : Sort u} → {β : Sort u_1} → (α → β → α) → outParam β → Prop
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.nnHolderNorm_eq_zero : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : EMetricSpace Y] {r : NNReal} {f : X → Y},
  MemHolder r f → (nnHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂)
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearEquiv_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) (v : V), φ.toLinearEquiv v = ↑φ v
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite : ∀ {L : FirstOrder.Language} {α : Type w} (T : L.Theory) (s : Set α) (M : Type w') [inst : L.Structure M] [M ⊨ T]
  [Infinite M], ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
-- Mathlib.Data.Sum.Interval
Sum.Ico_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₁ : α) (b₂ : β), Finset.Ico (Sum.inl a₁) (Sum.inr b₂) = ∅
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- Let `I` be a fractional ideal of `K`. Assume that `f : InfinitePlace K → ℝ≥0` is such that
`minkowskiBound K I < volume (convexBodyLT K f)` where `convexBodyLT K f` is the set of
points `x` such that `‖x w‖ < f w` for all infinite places `w` (see `convexBodyLT_volume` for
the computation of this volume), then there exists a nonzero algebraic number `a` in `I` such
that `w a < f w` for all infinite places `w`.  -/
NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {f : NumberField.InfinitePlace K → NNReal}
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  NumberField.mixedEmbedding.minkowskiBound K I < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) →
    ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w a < ↑(f w)
-- Mathlib.Data.Int.Bitwise
Int.bitwise_xor : Int.bitwise xor = Int.xor
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableDiv₂.toMeasurableDiv : ∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Div G] [MeasurableDiv₂ G], MeasurableDiv G
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.M.mk.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  (x : (j : J) × ↑(F.obj j)),
  AddMonCat.FilteredColimits.M.mk F x = (F.comp (CategoryTheory.forget AddMonCat)).ιColimitType x.fst x.snd
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.span_relation_le_ker_π : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M),
  Submodule.span A (Set.range relations.relation) ≤ solution.π.ker
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.sub_nat : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (n : ℕ), LiouvilleWith p (x - ↑n)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.unbox.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_23),
  sizeOf (Lean.Compiler.LCNF.LetValue.unbox fvarId h) = 1 + sizeOf fvarId + sizeOf h
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (c : G.Walk v v) (h : u ∈ c.support),
  (c.rotate u h).toSubgraph = c.toSubgraph
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Lift a functor between over categories to a functor between `MonoOver` categories,
given suitable evidence that morphisms are taken to monomorphisms.
 -/
CategoryTheory.MonoOver.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {Y : D} →
            (F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)) →
              (∀ (f : CategoryTheory.MonoOver Y),
                  CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom) →
                CategoryTheory.Functor (CategoryTheory.MonoOver Y) (CategoryTheory.MonoOver X)
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_inv : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  {F G : CategoryTheory.Functor (A ⊕ A') B}
  (η₁ : (CategoryTheory.Sum.inl_ A A').comp F ≅ (CategoryTheory.Sum.inl_ A A').comp G)
  (η₂ : (CategoryTheory.Sum.inr_ A A').comp F ≅ (CategoryTheory.Sum.inr_ A A').comp G),
  (CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr η₁ η₂).inv =
    CategoryTheory.Sum.natTransOfWhiskerLeftInlInr η₁.inv η₂.inv
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.instRespectsIsoIsColocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P.isColocal.RespectsIso
-- Mathlib.SetTheory.ZFC.Class
instInterClass : Inter Class.{u_1}
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- the scalar product by a non-zero complex number as a continuous real-linear equivalence.  -/
scalarSMulCLE : (H : Type u_1) → [inst : NormedAddCommGroup H] → [inst_1 : InnerProductSpace ℂ H] → ℂˣ → H ≃L[ℝ] H
-- Mathlib.Analysis.Analytic.ConvergenceRadius
ContinuousLinearMap.compFormalMultilinearSeries.congr_simp : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : AddCommMonoid G] [inst_12 : Module 𝕜 G] [inst_13 : TopologicalSpace G]
  [inst_14 : ContinuousAdd G] [inst_15 : ContinuousConstSMul 𝕜 G] (f f_1 : F →L[𝕜] G),
  f = f_1 →
    ∀ (p p_1 : FormalMultilinearSeries 𝕜 E F),
      p = p_1 → ∀ (n : ℕ), f.compFormalMultilinearSeries p n = f_1.compFormalMultilinearSeries p_1 n
-- Std.Sync.StreamMap
/-- Remove a stream by name
 -/
Std.StreamMap.unregister : {α β : Type} → [BEq α] → Std.StreamMap α β → α → Std.StreamMap α β
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProd.const.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  (value value_1 : BaseType e),
  (Mathlib.Tactic.Ring.Common.ExProd.const value = Mathlib.Tactic.Ring.Common.ExProd.const value_1) = (value = value_1)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_add_left_nhdsNE : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {c a : G},
  Filter.map (fun x => c + x) (nhdsWithin a {a}ᶜ) = nhdsWithin (c + a) {c + a}ᶜ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get_eq_getElem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : a ∈ t}, t.get a h = t[a]
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.empty_ext : ∀ {X : AlgebraicGeometry.Scheme} (f g : ∅ ⟶ X), f = g
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Call.mk.sizeOf_spec : ∀ (expr relevantArgs : Lean.Expr),
  sizeOf { expr := expr, relevantArgs := relevantArgs } = 1 + sizeOf expr + sizeOf relevantArgs
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'' : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x =
    Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) •
      ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis fun i =>
        if i = NumberField.Units.dirichletUnitTheorem.w₀ then 0 else x i
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMap.match_1.eq_1 : ∀ {β' : Type u_1} (motive : Option β' → Sort u_2) (h_1 : none = none → motive none)
  (h_2 : (out' : β') → none = some out' → motive (some out')),
  (match h' : none with
    | none => h_1 h'
    | some out' => h_2 out' h') =
    h_1 ⋯
-- Init.Omega.IntList
Lean.Omega.IntList.instHMulInt : HMul ℤ Lean.Omega.IntList Lean.Omega.IntList
-- ProofWidgets.Data.Html
/-- See [MDN docs](https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_Flow_Layout/Block_and_Inline_Layout_in_Normal_Flow).  -/
ProofWidgets.LayoutKind : Type
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_inv_left : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute (↑u) a → Commute (↑u⁻¹) a
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.norm_indicatorConstLp' : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  p ≠ 0 → μ s ≠ 0 → ‖MeasureTheory.indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)
-- Mathlib.RingTheory.Finiteness.FinitePresentationLocal
/-- Finite-presentation can be checked on a standard covering of the target.  -/
Algebra.FinitePresentation.of_span_eq_top_target : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set S),
  Ideal.span s = ⊤ → (∀ i ∈ s, Algebra.FinitePresentation R (Localization.Away i)) → Algebra.FinitePresentation R S
-- Std.Data.DHashMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.DHashMap.alter : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [LawfulBEq α] → Std.DHashMap α β → (a : α) → (Option (β a) → Option (β a)) → Std.DHashMap α β
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
/-- Type synonym for turning a `LieRing` into a `NonUnitalNonAssocRing`.

A `LieRing` can be regarded as a `NonUnitalNonAssocRing` by turning its
`Bracket` (denoted `⁅, ⁆`) into a `Mul` (denoted `*`).  -/
CommutatorRing : Type v → Type v
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {A B : AlgCat R} {f g : A ⟶ B}, f = g ↔ AlgCat.Hom.hom f = AlgCat.Hom.hom g
-- Mathlib.Analysis.Normed.Affine.Convex
/-- We can intercalate a simplex between a point and one of its neighborhoods.  -/
exists_mem_interior_convexHull_affineBasis : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
  s ∈ nhds x → ∃ b, x ∈ interior ((convexHull ℝ) (Set.range ⇑b)) ∧ (convexHull ℝ) (Set.range ⇑b) ⊆ s
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The equalizer in `CommRingCat` is the equalizer as sets.  -/
CommRingCat.equalizerForkIsLimit : {A B : CommRingCat} → (f g : A ⟶ B) → CategoryTheory.Limits.IsLimit (CommRingCat.equalizerFork f g)
-- Mathlib.Data.Sym.Card
Sym2.two_mul_card_image_offDiag : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α),
  2 * (Finset.image (Function.uncurry Sym2.mk) s.offDiag).card = s.offDiag.card
-- Init.Data.BitVec.Lemmas
BitVec.getElem_xor : ∀ {w : ℕ} {x y : BitVec w} {i : ℕ} (h : i < w), (x ^^^ y)[i] = (x[i] ^^ y[i])
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.fst_mem_orbit_of_mem_orbit : ∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] {β : Type u_1} [inst_2 : AddAction M β]
  {x y : α × β}, x ∈ AddAction.orbit M y → x.1 ∈ AddAction.orbit M y.1
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n ↔ M ∈ Matrix.rowStochastic R n ∧ M ∈ Matrix.colStochastic R n
-- Mathlib.Algebra.CharP.Basic
CharP.natCast_eq_natCast_mod : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] (a : ℕ), ↑a = ↑(a % p)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.equiv_apply_coe : ∀ {R : Type u_1} [inst : Semiring R] (P : Cubic R), ↑(Cubic.equiv P) = P.toPoly
-- Init.Data.Array.Lemmas
Array.foldl_assoc : ∀ {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {xs : Array α} {a₁ a₂ : α},
  Array.foldl op (op a₁ a₂) xs = op a₁ (Array.foldl op a₂ xs)