mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.ZMod
AddMonoidHom.coe_toZModLinearMap : ∀ (n : ℕ) {M : Type u_1} {M₁ : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₁] [inst_2 : Module (ZMod n) M]
  [inst_3 : Module (ZMod n) M₁] (f : M →+ M₁), ⇑(AddMonoidHom.toZModLinearMap n f) = ⇑f
-- Init.Data.String.OrderInstances
String.Slice.Pos.instLawfulOrderLT : ∀ {s : String.Slice}, Std.LawfulOrderLT s.Pos
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Submodule.reflection_orthogonal_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (v : E), Kᗮ.reflection v = -K.reflection v
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sigmaOfIsColimit_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (x x_1 : (E.sigmaOfIsColimit hc).I₀) (x_2 : PUnit.{w + 1}),
  (E.sigmaOfIsColimit hc hd).Y x_2 = d.pt
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.toMonoidHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : MulOneClass α] → [inst_3 : MulOneClass β] → (α →*o β) → α →* β
-- Mathlib.RingTheory.Regular.Flat
RingTheory.Sequence.IsWeaklyRegular.of_flat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular R rs → RingTheory.Sequence.IsWeaklyRegular S (List.map (⇑(algebraMap R S)) rs)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.image.mk : ∀ (f : ZFSet.{u} → ZFSet.{u}) [inst : ZFSet.Definable₁ f] (x : ZFSet.{u}) {y : ZFSet.{u}}, y ∈ x → f y ∈ ZFSet.image f x
-- Mathlib.Analysis.Calculus.ContDiff.Basic
ftaylorSeries_zero : ∀ {𝕜 : 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], ftaylorSeries 𝕜 0 = 0
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.exists_kerSquareLift_comp_eq_id : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B),
  ∃ σ₀,
    (Ideal.Quotient.mkₐ (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D))
              (Ideal.span
                (Set.range
                  (Algebra.Presentation.relationOfHasCoeffs
                    ↥(Algebra.Smooth.DescentAux.subalgebra✝ R D))))).kerSquareLift.comp
        σ₀ =
      AlgHom.id (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D))
        (Algebra.Presentation.ModelOfHasCoeffs ↥(Algebra.Smooth.DescentAux.subalgebra✝ R D))
-- Lean.Elab.Util
Lean.Elab.MacroStackElem.mk.sizeOf_spec : ∀ (before after : Lean.Syntax), sizeOf { before := before, after := after } = 1 + sizeOf before + sizeOf after
-- Mathlib.Tactic.ExtendDoc
/-- `extend_docs <declName> before <prefix_string> after <suffix_string>` extends the
docs of `<declName>` by adding `<prefix_string>` before and `<suffix_string>` after.  -/
Mathlib.Tactic.ExtendDocs.commandExtend_docs__Before__After_ : Lean.ParserDescr
-- Mathlib.Data.Int.Bitwise
Int.land_bit : ∀ (a : Bool) (m : ℤ) (b : Bool) (n : ℤ), (Int.bit a m).land (Int.bit b n) = Int.bit (a && b) (m.land n)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.SeparatingLeft.toMatrix₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n]
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂) {B : M₁ →ₗ[R] M₂ →ₗ[R] R},
  B.SeparatingLeft → ((LinearMap.toMatrix₂ b₁ b₂) B).SeparatingLeft
-- Batteries.Data.List.Count
List.rightInverse_sigmaCountToIdx_idxToSigmaCount : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs : List α},
  Function.RightInverse xs.sigmaCountToIdx xs.idxToSigmaCount
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_inv_nat_lt : ∀ {a : ENNReal}, a ≠ 0 → ∃ n, (↑n)⁻¹ < a
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.normNoninc_of_isometry : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  {f : NormedAddGroupHom V W}, Isometry ⇑f → f.NormNoninc
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.self_σ : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (a : S),
  (Algebra.Extension.self R S).σ a = id a
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_left : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (f i - f j) (f k) κ μ
-- Init.Core
Eq.propIntro : ∀ {a b : Prop}, (a → b) → (b → a) → a = b
-- Mathlib.CategoryTheory.Galois.EssSurj
/-- The constructed cocone `coconeQuotientDiag` on the diagram `quotientDiag` is colimiting.  -/
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.coconeQuotientDiagIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {V U : OpenSubgroup (CategoryTheory.Aut F)} →
            (h : (↑U).Normal) →
              {A : C} →
                (u :
                    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
                      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
                        (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U))) →
                  (hUinV : U ≤ V) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.PreGaloisCategory.coconeQuotientDiag✝ h u hUinV)
-- Init.Data.Int.Gcd
Int.lcm_one_left : ∀ (a : ℤ), Int.lcm 1 a = a.natAbs
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β] (f : α → β),
  Finset.inf 1 f = f 1
-- Mathlib.Data.List.Cycle
List.nextOr_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (x y d : α), [y].nextOr x d = d
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.pairwise_disjoint_labelGraph : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabeling K},
  Pairwise fun k l => Disjoint (C.labelGraph k) (C.labelGraph l)
-- Init.Data.Nat.Lemmas
Nat.mul_add_mod_of_lt : ∀ {a b c : ℕ}, c < b → (a * b + c) % b = c
-- Mathlib.Topology.Separation.Regular
regularSpace_induced : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [RegularSpace X] (f : Y → X), RegularSpace Y
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.coe_inf : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S T : IntermediateField F E), ↑(S ⊓ T) = ↑S ∩ ↑T
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Client.mk.inj : ∀ {shared shared_1 : Std.Http.Internal.Mock.SharedState✝},
  { shared := shared } = { shared := shared_1 } → shared = shared_1
-- Init.Data.BitVec.Lemmas
/-- Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree,
because it makes the value of the bitvector less than or equal to `2^(w-1)`.
 -/
BitVec.toInt_ushiftRight_of_lt : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, 0 < n → (x >>> n).toInt = ↑(x.toNat >>> n)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for `Iso.hom η`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.homM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.operation_lift : ∀ {m : Type w → Type w'} [inst : Functor m] {α : Type w} {x : m α},
  (Std.Iterators.PostconditionT.lift x).operation = (fun x_1 => ⟨x_1, ⋯⟩) <$> x
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
/-- The **Ahlswede-Zhang Identity**.  -/
AhlswedeZhang.infSum_eq_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {𝒜 : Finset (Finset α)} [Nonempty α],
  𝒜.Nonempty → ∅ ∉ 𝒜 → AhlswedeZhang.infSum 𝒜 = 1
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.refl_apply : ∀ (X : Type u) [inst : TopologicalSpace X] (a : X), (ContinuousMap.HomotopyEquiv.refl X).toFun a = a
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.IsSplittingField.instIsTorsionFreeSplittingField : ∀ {K : Type v} [inst : Field K] (f : Polynomial K), Module.IsTorsionFree K f.SplittingField
-- Mathlib.Topology.Homotopy.Basic
/-- Let `F` be a homotopy between `f₀ : C(X, Y)` and `f₁ : C(X, Y)`. Let `G` be a homotopy between
`g₀ : C(Z, Z')` and `g₁ : C(Z, Z')`. Then `F.prodMap G` is the homotopy between `f₀.prodMap g₀` and
`f₁.prodMap g₁` that sends `(t, x, z)` to `(F (t, x), G (t, z))`.  -/
ContinuousMap.Homotopy.prodMap : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      {Z' : Type x} →
        [inst : TopologicalSpace X] →
          [inst_1 : TopologicalSpace Y] →
            [inst_2 : TopologicalSpace Z] →
              [inst_3 : TopologicalSpace Z'] →
                {f₀ f₁ : C(X, Y)} →
                  {g₀ g₁ : C(Z, Z')} → f₀.Homotopy f₁ → g₀.Homotopy g₁ → (f₀.prodMap g₀).Homotopy (f₁.prodMap g₁)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase.induct : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α)
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Prop),
  (∀ (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced), motive Std.DTreeMap.Internal.Impl.leaf hr) →
    (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
        (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
        compare k k' = Ordering.lt →
          ∀ (l'_1 : Std.DTreeMap.Internal.Impl α β) (hl'₁ : l'_1.Balanced) (hl'₂ : l'.size - 1 ≤ l'_1.size)
            (hl'₃ : l'_1.size ≤ l'.size),
            Std.DTreeMap.Internal.Impl.erase k l' ⋯ =
                { impl := l'_1, balanced_impl := hl'₁, lb_le_size_impl := hl'₂, size_impl_le_ub := hl'₃ } →
              motive l' ⋯ → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
      (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
          (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
          compare k k' = Ordering.gt →
            ∀ (l'_1 : Std.DTreeMap.Internal.Impl α β) (hl'₁ : l'_1.Balanced) (hl'₂ : r'.size - 1 ≤ l'_1.size)
              (hl'₃ : l'_1.size ≤ r'.size),
              Std.DTreeMap.Internal.Impl.erase k r' ⋯ =
                  { impl := l'_1, balanced_impl := hl'₁, lb_le_size_impl := hl'₂, size_impl_le_ub := hl'₃ } →
                motive r' ⋯ → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
        (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
            compare k k' = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
          ∀ (t : Std.DTreeMap.Internal.Impl α β) (h : t.Balanced), motive t h
-- Mathlib.Data.List.Nodup
List.Nodup.sdiff_eq_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List α},
  l₁.Nodup → l₁.diff l₂ = List.filter (fun x => decide (x ∉ l₂)) l₁
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A pair of continuous linear maps such that `f₁ ∘ f₂ = id` generates a continuous
linear equivalence `e` between `M` and `M₂ × f₁.ker` such that `(e x).2 = x` for `x ∈ f₁.ker`,
`(e x).1 = f₁ x`, and `(e (f₂ y)).2 = 0`. The map is given by `e x = (f₁ x, x - f₂ (f₁ x))`.  -/
ContinuousLinearEquiv.equivOfRightInverse : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_3} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] →
            {M₂ : Type u_4} →
              [inst_4 : TopologicalSpace M₂] →
                [inst_5 : AddCommGroup M₂] →
                  [inst_6 : Module R M₂] →
                    [IsTopologicalAddGroup M] →
                      (f₁ : M →L[R] M₂) → (f₂ : M₂ →L[R] M) → Function.RightInverse ⇑f₂ ⇑f₁ → M ≃L[R] M₂ × ↥(↑f₁).ker
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_injective : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7}, Function.Injective DFunLike.coe
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_zero_eq_bot : SimpleGraph.cycleGraph 0 = ⊥
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.mulIndicator_const_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : One β] {s : Set α} {c : β},
  Filter.EventuallyConst (s.mulIndicator fun x => c) l ↔ c = 1 ∨ Filter.EventuallyConst s l
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.lift_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z)
  (h : autoParam (CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) _auto_83✝) {Z_1 : C}
  (h_1 : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.lift a b h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd f g) h_1) =
    CategoryTheory.CategoryStruct.comp b h_1
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivisionMonoid` if it admits an injective map
that preserves `1`, `*`, `⁻¹`, and `/` to a `DivisionMonoid`. See note [reducible non-instances]  -/
Function.Injective.divisionMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : DivisionMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → DivisionMonoid M₁
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_map_map : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β},
  Disjoint (Multiset.map f s) (Multiset.map g t) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b
-- Std.Http.Data.Method
/-- Perform a message loop-back test.
Source: https://httpwg.org/specs/rfc9110.html#section-9.3.8
 -/
Std.Http.Method.trace : Std.Http.Method
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.addBottom.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} (L : Turing.ListBlank ((k : K) → Option (Γ k))),
  Turing.TM2to1.addBottom L =
    Turing.ListBlank.cons (true, L.head) (Turing.ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkAddNat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- When `M` is a module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
module structure over `R`.

The preferred way of setting this up is `[Module R M] [Module S M] [IsScalarTower R S M]`.
 -/
RestrictScalars.module : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : CommSemiring R] → [Algebra R S] → [Module S M] → Module R (RestrictScalars R S M)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.arrayLit.injEq : ∀ (a a_1 : List Lean.Meta.Match.Example),
  (Lean.Meta.Match.Example.arrayLit a = Lean.Meta.Match.Example.arrayLit a_1) = (a = a_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {l : List α}
  {k : α}, l.contains k = false → (Std.DHashMap.Raw.Const.unitOfList l).getKey! k = default
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get!.eq_1 : ∀ {α : Type u} {δ : Type w} [inst : Ord α] [inst_1 : Inhabited δ] (k : α),
  Std.DTreeMap.Internal.Impl.Const.get! Std.DTreeMap.Internal.Impl.leaf k =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.get!" 227 13
      "Key is not present in map"
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.clz_congr : ∀ (w : ℕ) (x x' : BitVec w), x = x' → x'.clz = x.clz
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearEquiv_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ↑e.symm = (↑e).symm
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.sum_le_mk_mul_iSup : ∀ {ι : Type u} (f : ι → Cardinal.{u}), Cardinal.sum f ≤ Cardinal.mk ι * ⨆ i, f i
-- Mathlib.Algebra.Order.Module.Defs
Pi.instPosSMulReflectLE : ∀ {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [inst : Zero α] [inst_1 : Preorder α]
  [inst_2 : (i : ι) → Preorder (β i)] [inst_3 : (i : ι) → SMul α (β i)] [∀ (i : ι), PosSMulReflectLE α (β i)],
  PosSMulReflectLE α ((i : ι) → β i)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instInhabited : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → Inhabited (ContinuousMultilinearMap R M₁ M₂)
-- Mathlib.CategoryTheory.Category.Preorder
/-- The equivalence of categories `X ≌ Y` induced by `e : X ≃o Y`.  -/
OrderIso.equivalence : {X : Type u} → {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → X ≃o Y → (X ≌ Y)
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.CommSemiRingCat.Hom.mk : {R S : CommSemiRingCat} → (↑R →+* ↑S) → R.Hom S
-- Mathlib.Data.Set.Function
Set.MapsTo.image_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t → f '' s ⊆ t
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_right_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) {X Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G}
  (g : X ⟶ Y), ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).map g).right.right = g.right
-- Mathlib.Analysis.Normed.Affine.Convex
Wbtw.dist_add_dist : ∀ {E : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] {x y z : P},
  Wbtw ℝ x y z → dist x y + dist y z = dist x z
-- Aesop.Tree.Data
Aesop.MVarCluster.setState : Aesop.NodeState → Aesop.MVarCluster → Aesop.MVarCluster
-- Mathlib.Order.Lattice
sup_congr_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, b ≤ a ⊔ c → c ≤ a ⊔ b → a ⊔ b = a ⊔ c
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.leftDeriv_fderiv_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) (x : G),
  φ.leftDeriv ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) x) = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
/-- The `ℝ`-spectrum of an element of the form `star b * b` in a C⋆-algebra is nonnegative.

This is the key result used to establish `CStarAlgebra.instNonnegSpectrumClass`.  -/
spectrum_star_mul_self_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] {b : A}, ∀ x ∈ spectrum ℝ (star b * b), 0 ≤ x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Min α] [inst_1 : LE α]
  [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] [Std.LawfulEqCmp cmp],
  t.WF → t.toList.min? = t.min?
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- **Alias** of `AlgebraicGeometry.Smooth.smooth_appLE`. -/
AlgebraicGeometry.Scheme.Hom.smooth_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.Smooth f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Smooth
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_pos_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (x : R), 0 < v.restrict x ↔ 0 < v x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} {hc : k ∈ t.alter k f},
  (t.alter k f).get k hc = (f (t.get? k)).get ⋯
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice},
  String.Slice.Pattern.BackwardPattern.skipSuffix? p s =
    String.Slice.Pattern.BackwardPattern.skipSuffix? (fun x => decide (p x)) s