mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_symm_toLinearEquiv : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ⇑(↑e).symm = ⇑e.symm
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map  -/
CategoryTheory.AddMonObj.«termδ[_,_]» : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ico_succ : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ico a.succ b.succ, f i = ∏ i ∈ Finset.Ico a b, f i.succ
-- Mathlib.Analysis.Normed.Group.Constructions
norm_toAdd : ∀ {E : Type u_2} [inst : Norm E] (x : Multiplicative E), ‖Multiplicative.toAdd x‖ = ‖x‖
-- Plausible.Random
/-- A monad transformer to generate random objects using the generic generator type `g`  -/
Plausible.RandGT : Type → (Type u_1 → Type u_2) → Type u_1 → Type (max u_1 u_2)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_pow : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] (n : ℕ) (r : R),
  QuadraticAlgebra.C (r ^ n) = QuadraticAlgebra.C r ^ n
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ↔ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.gc_map_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N),
  GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_image_image : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁), ⇑e.symm '' ⇑e '' s = s
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn.match_1.splitter : {α : Type u_1} →
  (motive : (l : List α) → l ≠ [] → Sort u_2) →
    (l : List α) → (h : l ≠ []) → ((x : α) → (xs : List α) → (h : x :: xs ≠ []) → motive (x :: xs) h) → motive l h
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.support_leadingTerm' : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {p : MvPolynomial σ R},
  p ≠ 0 → (m.leadingTerm p).support = {m.degree p}
-- Init.Data.Nat.Lemmas
Nat.le_sub_iff_add_le : ∀ {k m n : ℕ}, k ≤ m → (n ≤ m - k ↔ n + k ≤ m)
-- Mathlib.RingTheory.LocalProperties.ProjectiveDimension
ModuleCat.localizedModule_hasProjectiveDimensionLE : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (n : ℕ) (S : Submonoid R) (M : ModuleCat R)
  [CategoryTheory.HasProjectiveDimensionLE M n], CategoryTheory.HasProjectiveDimensionLE (M.localizedModule S) n
-- Mathlib.SetTheory.Cardinal.Order
_private.Mathlib.SetTheory.Cardinal.Order.0.Cardinal.add_le_add' : ∀ {a b c d : Cardinal.{u_1}}, a ≤ b → c ≤ d → a + c ≤ b + d
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.Context.mk : Lean.Lsp.DocumentUri → Lean.Lsp.Position → ℕ → Lean.Server.Completion.Context✝
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instPartialOrder : PartialOrder ZFSet.{u}
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The subgroup generated by an element of a group equals the set of integer number powers of
the element.  -/
Subgroup.mem_closure_singleton : ∀ {G : Type u_1} [inst : Group G] {x y : G}, y ∈ Subgroup.closure {x} ↔ ∃ n, x ^ n = y
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.dist_of_mem_subset_mk_sphere : ∀ {P : Type u_2} [inst : MetricSpace P] {p c : P} {ps : Set P} {r : ℝ},
  p ∈ ps → ps ⊆ Metric.sphere { center := c, radius := r }.center { center := c, radius := r }.radius → dist p c = r
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.mem_ofSimplex_obj : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  x ∈ (SSet.Subcomplex.ofSimplex x).obj (Opposite.op { len := n })
-- Mathlib.Logic.Small.Defs
small_zero : ∀ (α : Type), Small.{w, 0} α
-- Mathlib.Data.List.TakeDrop
List.dropLast_take_eq_take_dropLast : ∀ {α : Type u} (l : List α) (n : ℕ), (List.take n l).dropLast = List.take (n - 1) l.dropLast
-- Init.Data.Int.DivMod.Bootstrap
Int.add_ediv_of_dvd_left : ∀ {a b c : ℤ}, c ∣ a → (a + b) / c = a / c + b / c
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_modifyKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCastD k (Std.Internal.List.modifyKey k f l) fallback =
      (Option.map f (Std.Internal.List.getValueCast? k l)).getD fallback
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_comp_neg_X : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, (p.comp (-Polynomial.X)).degree = p.degree
-- Std.Time.Format.Modifier
Std.Time.instInhabitedOffsetO.default : Std.Time.OffsetO
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The composition `hom ≫ inv` is isomorphic to the identity.  -/
CategoryTheory.Bicategory.Equivalence.unit : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (self : CategoryTheory.Bicategory.Equivalence a b) →
        CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp self.hom self.inv
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The linear equivalence between bilinear maps and `n × m` matrices  -/
LinearMap.toMatrix₂' : (R : Type u_1) →
  {S₁ : Type u_3} →
    {S₂ : Type u_5} →
      {N₂ : Type u_10} →
        {n : Type u_11} →
          {m : Type u_12} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid N₂] →
                [inst_2 : Module R N₂] →
                  [inst_3 : Semiring S₁] →
                    [inst_4 : Semiring S₂] →
                      [inst_5 : Module S₁ N₂] →
                        [inst_6 : Module S₂ N₂] →
                          [inst_7 : SMulCommClass S₁ R N₂] →
                            [inst_8 : SMulCommClass S₂ R N₂] →
                              [inst_9 : SMulCommClass S₂ S₁ N₂] →
                                [Fintype n] →
                                  [Fintype m] →
                                    [DecidableEq n] →
                                      [DecidableEq m] → ((n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) ≃ₗ[R] Matrix n m N₂
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isCofilteredOrEmpty_op_of_isFilteredOrEmpty : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C],
  CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is weakly between the other two, the oriented angle at the
first point is zero.  -/
Wbtw.oangle₂₁₃_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₂ p₁ p₃ = 0
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.AnchorRef.anchorPrefix : Lean.Meta.Grind.AnchorRef → UInt64
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicIntInterval : Inhabited Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_iff : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  [LocallyCompactSpace X],
  MeasureTheory.LocallyIntegrable f μ ↔ ∀ (k : Set X), IsCompact k → MeasureTheory.IntegrableOn f k μ
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.comp₂ : ∀ (f : ℕ → ℕ → ℕ),
  (Nat.Primrec' fun v => f v.head v.tail.head) →
    ∀ {n : ℕ} {g h : List.Vector ℕ n → ℕ}, Nat.Primrec' g → Nat.Primrec' h → Nat.Primrec' fun v => f (g v) (h v)
-- Init.Data.Range.Polymorphic.UInt
USize.rxiHasSize_eq_toBitVec : ∀ {lo : BitVec System.Platform.numBits}, Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
-- Init.Data.Iterators.Lemmas.Combinators.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Append.0.Std.Iter.step_append.match_1.eq_1 : ∀ {α₁ β : Type u_1} [inst : Std.Iterator α₁ Id β] {it₁ : Std.Iter β} (motive : it₁.Step → Sort u_2) (it₁' : Std.Iter β)
  (out : β) (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out))
  (h_1 :
    (it₁' : Std.Iter β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 : (it₁' : Std.Iter β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₁' out, h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₁' out h
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceSub : Lean.Meta.Simp.DSimproc
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.ext_iff_isCircuit : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ (C : Set α), M₁.IsCircuit C ↔ M₂.IsCircuit C
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is commutative.  -/
Subsemigroup.isMulCommutative_closure : ∀ (M : Type u_1) [inst : Semigroup M] {s : Set M},
  (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → IsMulCommutative ↥(Subsemigroup.closure s)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (a : X ⟶ Y) {Z : ↑(F.obj b₂)}
  (h : (CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map fg).toFunctor.map a)
        (CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app Y) h)) =
    CategoryTheory.CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a)) h
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedParam : Inhabited Lean.IR.Param
-- Mathlib.Algebra.Order.Module.Defs
pos_and_pos_or_neg_and_neg_of_smul_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : LinearOrder α] [inst_4 : LinearOrder β] [PosSMulMono α β] [SMulPosMono α β],
  0 < a • b → 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instInhabited : (R : Type u) → [inst : Semiring R] → Inhabited (SemimoduleCat R)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.r_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting),
  CategoryTheory.CategoryStruct.comp s.r S.f =
    CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp S.g s.s
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- The iterated derivative commutes with shifting the function by a constant on the right.  -/
iteratedDeriv_comp_add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜),
  (iteratedDeriv n fun z => f (z + s)) = fun t => iteratedDeriv n f (t + s)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow_comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F]
  (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))),
  (CategoryTheory.ConcreteCategory.hom f)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow) x) =
    (CategoryTheory.ConcreteCategory.hom 0) x
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Generate all combination of measures. Assumes we have numbered the measures of each function,
and their counts is in `numMeasures`.

This puts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
try first, when the mutually recursive functions have similar argument structures
 -/
Lean.Elab.WF.GuessLex.generateCombinations? : Array ℕ → optParam ℕ 32 → Option (Array (Array ℕ))
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_eq_one : ∀ {a : Cardinal.{u_1}}, a.ord = 1 ↔ a = 1
-- Mathlib.RingTheory.Valuation.RankOne
/-- A valuation has rank at most one if its image (defined as `MonoidWithZeroHom.valueGroup₀ v`)
is contained in `ℝ≥0`. Note that this class includes the data
of an inclusion morphism `MonoidWithZeroHom.valueGroup₀ v → ℝ≥0`.  -/
Valuation.RankLeOne : {R : Type u_1} →
  {Γ₀ : Type u_2} → [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → Valuation R Γ₀ → Type u_2
-- Mathlib.Data.PEquiv
PEquiv.symm_bot : ∀ {α : Type u} {β : Type v}, ⊥.symm = ⊥
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  (Std.ExtHashMap.filter f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => f x_2 m[x_2]
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_iff_exists_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₂ : P},
  p₂ ∈ s → (s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.forget_createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J MonCat) → CategoryTheory.CreatesLimit F (CategoryTheory.forget MonCat)
-- Mathlib.Topology.UniformSpace.Equicontinuity
UniformEquicontinuousOn.mono : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α}
  {S T : Set β}, UniformEquicontinuousOn F T → S ⊆ T → UniformEquicontinuousOn F S
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb_toNat : ∀ {n : ℕ} (hi lo : ℕ) (x : BitVec n), (BitVec.extractLsb hi lo x).toNat = x.toNat >>> lo % 2 ^ (hi - lo + 1)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation : ∀ {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] (v : IsDedekindDomain.HeightOneSpectrum R),
  (IsDedekindDomain.HeightOneSpectrum.valuation K v).IsNontrivial
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.radius_regularizedGaussHGFunSeries_ge_one : ∀ (a b c : ℂ), 1 ≤ (a.regularizedGaussHGFunSeries b c).radius
-- Mathlib.Analysis.Calculus.Deriv.ZPow
DifferentiableAt.zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {m : ℤ} {f : E → 𝕜} {a : E},
  DifferentiableAt 𝕜 f a → f a ≠ 0 ∨ 0 ≤ m → DifferentiableAt 𝕜 (fun x => f x ^ m) a
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.of_smul_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β},
  (s • t).Nonempty → t.Nonempty
-- Mathlib.RingTheory.Etale.Field
/-- If `R` is an étale `k`-algebra over a separably closed field `k`, it is
isomorphic to the (finite) product of copies of `k` indexed by the prime spectrum of `R`.  -/
Algebra.FormallyEtale.equivPiOfIsSepClosed : (K : Type u_1) →
  (A : Type u) →
    [inst : Field K] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra K A] →
          [Algebra.EssFiniteType K A] → [Algebra.FormallyEtale K A] → [IsSepClosed K] → A ≃ₐ[K] PrimeSpectrum A → K
-- Mathlib.Algebra.Group.Action.Option
Option.vadd_def : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] (a : M) (x : Option α), a +ᵥ x = Option.map (fun x => a +ᵥ x) x
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.HomIsOver.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {S : C}
  [inst_1 : CategoryTheory.OverClass X S] [inst_2 : CategoryTheory.OverClass Y S],
  autoParam (CategoryTheory.CategoryStruct.comp f (Y ↘ S) = X ↘ S) CategoryTheory.HomIsOver.comp_over._autoParam →
    CategoryTheory.HomIsOver f S
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_inter_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  Set.Ioc b₁ a₁ ∩ Set.Ioc b₂ a₂ = Set.Ioc (max b₁ b₂) (min a₁ a₂)
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.binop.inj : ∀ {ref : Lean.Syntax} {f : Lean.Expr} {lhs rhs : FBinopElab.Tree✝} {ref_1 : Lean.Syntax} {f_1 : Lean.Expr}
  {lhs_1 rhs_1 : FBinopElab.Tree✝},
  FBinopElab.Tree.binop✝ ref f lhs rhs = FBinopElab.Tree.binop✝ ref_1 f_1 lhs_1 rhs_1 →
    ref = ref_1 ∧ f = f_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.MeasureTheory.Integral.Lebesgue.Norm
MeasureTheory.lintegral_enorm_of_nonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ f → ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
-- Mathlib.Logic.Equiv.Defs
Equiv.coe_refl : ∀ {α : Sort u}, ⇑(Equiv.refl α) = id
-- Mathlib.Algebra.Module.Equiv.Defs
SemilinearEquivClass.toAddEquivClass : ∀ {F : Type u_14} {R : outParam (Type u_15)} {S : outParam (Type u_16)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ}
  {M : outParam (Type u_17)} {M₂ : outParam (Type u_18)} {inst_4 : AddCommMonoid M} {inst_5 : AddCommMonoid M₂}
  {inst_6 : Module R M} {inst_7 : Module S M₂} {inst_8 : EquivLike F M M₂} [self : SemilinearEquivClass F σ M M₂],
  AddEquivClass F M M₂
-- Aesop.Script.SpecificTactics
Aesop.assertHypothesisS : Lean.MVarId → Lean.Meta.Hypothesis → Lean.Meta.TransparencyMode → Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.stepRet.match_1.eq_1 : ∀ (motive : Turing.ToPartrec.Cont → List ℕ → Sort u_1) (v : List ℕ)
  (h_1 : (v : List ℕ) → motive Turing.ToPartrec.Cont.halt v)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₁ fs as k) v)
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₂ ns k) v)
  (h_4 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.comp f k) v)
  (h_5 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.fix f k) v),
  (match Turing.ToPartrec.Cont.halt, v with
    | Turing.ToPartrec.Cont.halt, v => h_1 v
    | Turing.ToPartrec.Cont.cons₁ fs as k, v => h_2 fs as k v
    | Turing.ToPartrec.Cont.cons₂ ns k, v => h_3 ns k v
    | Turing.ToPartrec.Cont.comp f k, v => h_4 f k v
    | Turing.ToPartrec.Cont.fix f k, v => h_5 f k v) =
    h_1 v
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.add_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B D : LinearMap.BilinForm R M) (x y : M), ((B + D) x) y = (B x) y + (D x) y
-- Mathlib.Algebra.Group.Submonoid.Support
/-- The support of a submonoid is the largest subgroup it contains.  -/
Subgroup.gc_toSubmonoid_mulSupport : ∀ {G : Type u_1} [inst : Group G], GaloisConnection Subgroup.toSubmonoid Submonoid.mulSupport
-- Mathlib.Data.Finset.Grade
Finset.grade_eq : ∀ {α : Type u_1} (s : Finset α), grade ℕ s = s.card
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- Given three properties of objects `P₁`, `P₂`, and `Q` in a monoidal
category `C`, we say `TensorLE P₁ P₂ Q` holds if the tensor product
of an object in `P₁` and an object `P₂` is necessary in `Q`,
see also `ObjectProperty.IsMonoidal`.  -/
CategoryTheory.ObjectProperty.TensorLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Topology.UniformSpace.Compact
lebesgue_number_lemma_nhdsWithin' : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {U : (x : α) → x ∈ K → Set α},
  IsCompact K →
    (∀ (x : α) (hx : x ∈ K), U x hx ∈ nhdsWithin x K) →
      ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ y, UniformSpace.ball x V ∩ K ⊆ U ↑y ⋯
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Let `F : C₀ ⥤ C` be a dense subsite, and assume we have a family
`data : ∀ X, F.OneHypercoverDenseData J₀ J X`.
This lemma shows that `G : Cᵒᵖ ⥤ A` is a sheaf iff `F.op F.op ⋙ G : C₀ᵒᵖ ⥤ A`
is a sheaf and for any `X : C`, the multifork for `G` and the `1`-hypercover
given by `data X` is a limit.  -/
CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  (G : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf J G ↔
    CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G) ∧
      ∀ (X : C), Nonempty (CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G))
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Augmented.stdSimplex_map_right : ∀ {X Y : SimplexCategory} (θ : X ⟶ Y),
  (SSet.Augmented.stdSimplex.map θ).right =
    CategoryTheory.Limits.terminal.from
      { left := SSet.stdSimplex.obj X, right := ⊤_ Type u,
          hom :=
            {
              app := fun x =>
                CategoryTheory.Limits.terminal.from
                  (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj
                        (SSet.stdSimplex.obj X)).obj
                    x),
              naturality := ⋯ } }.right
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Entrypoint.mk : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_read_MonadReaderOf_lift_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m n : Type u → Type v} [inst : MonadLift m n]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : (α : Type u) → Std.Internal.Do.WP (n α) α Pred EPred] {ρ : Type u} {post : ρ → Pred} {epost : EPred}
  [inst_4 : MonadReaderOf ρ m],
  Std.Internal.Do.wp MonadReaderOf.read post epost = Std.Internal.Do.wp (MonadLift.monadLift read) post epost