mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multispanMapIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MultispanShape}
  (d : CategoryTheory.Limits.MultispanIndex J C) (F : CategoryTheory.Functor C D)
  (X : CategoryTheory.Limits.WalkingMultispan J),
  (d.multispanMapIso F).hom.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Iso.refl (F.obj (d.left a))
      | CategoryTheory.Limits.WalkingMultispan.right a => CategoryTheory.Iso.refl (F.obj (d.right a))).hom
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C)
  (t : CategoryTheory.Limits.FormalCoproduct C) (m : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt ⟶ t) (i : 𝒜)
  (x : (f i).I),
  ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t) m i).φ x =
    m.φ (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f x)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_zero_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  (γ : Type u_4) {mγ : MeasurableSpace γ}, κ.compProd 0 = 0
-- Mathlib.Order.Hom.Lex
Prod.Lex.prodUnique_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Unique β] (x : Lex (α × β)),
  (Prod.Lex.prodUnique α β) x = (ofLex x).1
-- Mathlib.Topology.Algebra.Group.OpenMapping
/-- Consider a sigma-compact group acting continuously and transitively on a Baire space. Then
the orbit map is open around the identity. It follows in `isOpenMap_smul_of_sigmaCompact` that it
is open around any point.  -/
smul_singleton_mem_nhds_of_sigmaCompact : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : Group G]
  [IsTopologicalGroup G] [inst_4 : MulAction G X] [SigmaCompactSpace G] [BaireSpace X] [T2Space X] [ContinuousSMul G X]
  [MulAction.IsPretransitive G X] {U : Set G}, U ∈ nhds 1 → ∀ (x : X), U • {x} ∈ nhds x
-- Mathlib.RingTheory.Ideal.GoingUp
/-- Let `P` be an ideal in `R[x]`.  The map
`R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))`
is injective.
 -/
Ideal.injective_quotient_le_comap_map : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)),
  Function.Injective
    ⇑(Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)
        (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ⋯)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'_comp : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} {o : Type u_6} [inst_1 : Fintype n] [inst_2 : Fintype o]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq o] (M : Matrix n n R₁) (P Q : Matrix n o R₁),
  (Matrix.toBilin' M).comp (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toBilin' (P.transpose * M * Q)
-- Init.Data.List.Lemmas
List.removeAll.eq_1 : ∀ {α : Type u} [inst : BEq α] (xs ys : List α), xs.removeAll ys = List.filter (fun x => !List.elem x ys) xs
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.mk_int_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] (N : AddSubgroup R) [inst_1 : N.Normal] (n : ℤ) (a : R), ↑(↑n * a) = n • ↑a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, Nonempty S.LeftHomologyData → S.HasLeftHomology
-- Std.Internal.Parsec.ByteArray
/-- Parse a hex digit `0-9`, `a-f`, or `A-F` as a `Char`.
 -/
Std.Internal.Parsec.ByteArray.hexDigit : Std.Internal.Parsec.ByteArray.Parser Char
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.G.mk.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (x : (j : J) × ↑(F.obj j)),
  AddGrpCat.FilteredColimits.G.mk F x = (F.comp (CategoryTheory.forget AddGrpCat)).ιColimitType x.fst x.snd
-- Std.Do.WP.Monad
Std.Do.StateT.instWPMonad : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} →
    {σ : Type u} → [inst : Monad m] → [Std.Do.WPMonad m ps] → Std.Do.WPMonad (StateT σ m) (Std.Do.PostShape.arg σ ps)
-- Mathlib.Data.Finset.Sups
Finset.inter_mem_infs : ∀ {α : Type u_2} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s t : Finset α}, s ∈ 𝒜 → t ∈ ℬ → s ∩ t ∈ 𝒜 ⊼ ℬ
-- Mathlib.Order.Category.CompleteLat
/-- Construct a bundled `CompleteLat` from the underlying type and typeclass.  -/
CompleteLat.of : (carrier : Type u_1) → [str : CompleteLattice carrier] → CompleteLat
-- Mathlib.Algebra.BigOperators.Finprod
/-- If a function `f` equals `0` on a set `s`, then the sum of `f i` over `i ∈ s`
equals `0`.  -/
finsum_mem_of_eqOn_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α},
  Set.EqOn f 0 s → ∑ᶠ (i : α) (_ : i ∈ s), f i = 0
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.pointOfClosedPoint.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X)
  (hx : IsClosed {x}),
  AlgebraicGeometry.pointOfClosedPoint f x hx =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.residueFieldIsoBase f x hx).hom)
      (X.fromSpecResidueField x)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_eq_all_of_fixedPoint : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  f x ≤ x → ((∀ (o : Ordinal.{u}), OrdinalApprox.gfpApprox f x o = x) ↔ f x = x)
-- Init.Data.String.OrderInstances
String.Pos.Raw.instToIntCiOfNatInt : Lean.Grind.ToInt String.Pos.Raw (Lean.Grind.IntInterval.ci 0)
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `CommMonoid` across an `Equiv`  -/
Equiv.commMonoid : {α : Type u_2} → {β : Type u_3} → α ≃ β → [CommMonoid β] → CommMonoid α
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_map_val : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → M),
  (Multiset.map f s.val).prod = ∏ a ∈ s, f a
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
DirectedOn.isLUB_csSup : ∀ {α : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)
-- Std.Internal.Do.PredTrans
/-- Adds an exception layer to a predicate transformer.

Given a transformer over `Except ε α`, produces one over `α` with an additional
exception postcondition for `ε`. The normal and error postconditions are combined
via `pushExcept`.  -/
Std.Internal.Do.PredTrans.pushExcept : {α : Type u} →
  {ε : Type v} →
    {Pred : Type w} →
      {EPred : Type z} →
        Std.Internal.Do.PredTrans Pred EPred (Except ε α) →
          Std.Internal.Do.PredTrans Pred (EPost.Cons✝ (ε → Pred) EPred) α
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_one : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ s ≠ 0 → μ s ≠ ⊤ → ⨍⁻ (_x : α) in s, 1 ∂μ = 1
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_dvd_of_mem_conductorSet : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {d : ℕ} [NeZero n],
  d ∈ χ.conductorSet → χ.conductor ∣ d
-- Mathlib.Data.Set.Basic
Set.mem_dite_univ_left : ∀ {α : Type u} (p : Prop) [inst : Decidable p] (t : ¬p → Set α) (x : α),
  (x ∈ if h : p then Set.univ else t h) ↔ ∀ (h : ¬p), x ∈ t h
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.norm_embedding_eq : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : K), ‖w.embedding x‖ = w x
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.instIteratorLoop : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {n : Type u_1 → Type u_2} →
        {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
          [inst : Monad m] →
            [Monad n] → [inst_2 : Std.Iterator α m β] → Std.IteratorLoop (Std.Iterators.Types.DropWhile α m β P) m n
-- Mathlib.Analysis.Normed.Group.Defs
/-- The distance function is induced by the norm.  -/
NormedGroup.dist_eq : ∀ {E : Type u_8} [self : NormedGroup E] (x y : E), dist x y = ‖x⁻¹ * y‖
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.homIso_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Cofork f g}
  (ht : CategoryTheory.Limits.IsColimit t) (Z : C)
  (h : { h // CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h }),
  (CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Cofork.IsColimit.desc' ht ↑h ⋯)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The `addCovolume` of an action of `G` on `α` is the volume of some
fundamental domain, or `0` if none exists.  -/
MeasureTheory.addCovolume : (G : Type u_6) →
  (α : Type u_7) →
    [Zero G] →
      [VAdd G α] →
        [inst : MeasurableSpace α] → autoParam (MeasureTheory.Measure α) MeasureTheory.addCovolume._auto_1 → ENNReal
-- Mathlib.Algebra.Field.Basic
div_sub_one : ∀ {K : Type u_1} [inst : DivisionRing K] {a b : K}, b ≠ 0 → a / b - 1 = (a - b) / b
-- Mathlib.Data.Set.Sups
Set.infs_union_right : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t₁ t₂ : Set α}, s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.id_toNatTrans : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴),
  (CategoryTheory.BasedNatTrans.id F).toNatTrans = CategoryTheory.NatTrans.id F.toFunctor
-- Mathlib.Analysis.Distribution.DerivNotation
LineDerivAdd.mk : ∀ {V : Type u} {E : Type v} {F : outParam (Type w)} [inst : AddCommGroup V] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : LineDeriv V E F],
  (∀ (v : V) (x y : E), LineDeriv.lineDerivOp v (x + y) = LineDeriv.lineDerivOp v x + LineDeriv.lineDerivOp v y) →
    (∀ (v w : V) (x : E), LineDeriv.lineDerivOp (v + w) x = LineDeriv.lineDerivOp v x + LineDeriv.lineDerivOp w x) →
      LineDerivAdd V E F
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.exists_isNilRegular_of_finrank_le_card : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M) [inst_5 : Module.Free R M]
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [IsDomain R],
  ↑(Module.finrank R M) ≤ Cardinal.mk R → ∃ x, φ.IsNilRegular x
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Auxiliary definition for `equivMonComonUnitIsoApp`.  -/
CategoryTheory.Bimon.equivMonComonUnitIsoAppX : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (M : CategoryTheory.Bimon C) →
          M.X ≅ (((CategoryTheory.Bimon.toMonComon C).comp (CategoryTheory.Bimon.ofMonComon C)).obj M).X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput.vec : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig) → aig.BinaryRefVec self.w
-- Mathlib.Topology.Order
indiscreteTopology_iff : ∀ (α : Type u_2) [inst : TopologicalSpace α], IndiscreteTopology α ↔ inst = ⊤
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentFilter.mk.injEq : ∀ (language? scheme? pattern? language?_1 scheme?_1 pattern?_1 : Option String),
  ({ language? := language?, scheme? := scheme?, pattern? := pattern? } =
      { language? := language?_1, scheme? := scheme?_1, pattern? := pattern?_1 }) =
    (language? = language?_1 ∧ scheme? = scheme?_1 ∧ pattern? = pattern?_1)
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The array of matrix entries as an Expr  -/
Mathlib.Tactic.Determinant.Ctx.arrayExpr : {u : Lean.Level} → {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Ctx rα → Q(Array «$α»)
-- Mathlib.Data.Multiset.Sort
Multiset.length_sort : ∀ {α : Type u_1} {s : Multiset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], (s.sort r).length = s.card
-- Std.Data.DHashMap.Internal.AssocList.Basic
Std.DHashMap.Internal.AssocList.cons.inj : ∀ {α : Type u} {β : α → Type v} {key : α} {value : β key} {tail : Std.DHashMap.Internal.AssocList α β} {key_1 : α}
  {value_1 : β key_1} {tail_1 : Std.DHashMap.Internal.AssocList α β},
  Std.DHashMap.Internal.AssocList.cons key value tail = Std.DHashMap.Internal.AssocList.cons key_1 value_1 tail_1 →
    key = key_1 ∧ value ≍ value_1 ∧ tail = tail_1
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.algebraMap_extendRightEquiv' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  (S : Type u_5) [inst_7 : CommRing S] [inst_8 : Algebra S ↥F] [inst_9 : Algebra S M] [inst_10 : IsScalarTower S (↥F) M]
  (a : ↥F), (algebraMap (↥(F.extendRight M)) M) ((F.extendRightEquiv' M S) a) = (algebraMap (↥F) M) a
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iic_mul_Iio_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b : α),
  Set.Iic a * Set.Iio b ⊆ Set.Iio (a * b)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Request.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (id : Lean.JsonRpc.RequestID) (method : String) (param : α),
  sizeOf { id := id, method := method, param := param } = 1 + sizeOf id + sizeOf method + sizeOf param
-- Mathlib.Topology.EMetricSpace.Lipschitz
lipschitzOnWith_restrict : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β} {t : Set ↑s}, LipschitzOnWith K (s.domRestrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.repeat_zero : ∀ {n : ℕ} {α : Sort u_1} (a : Fin n → α), Fin.repeat 0 a = Fin.elim0 ∘ Fin.cast ⋯
-- Std.Async.Select
/-- Creates a `Selector` that performs fair and data-loss free multiplexing on multiple `Selectable`s.
This allows the multiplexing operation to be composed with other selectors.
 -/
Std.Async.Selectable.combine : {α : Type} → Array (Std.Async.Selectable α) → IO (Std.Async.Selector α)
-- Mathlib.Data.Ordmap.Ordnode
BinaryTree.toOrdNode.eq_1 : ∀ {α : Type u_1}, BinaryTree.nil.toOrdNode = Ordnode.nil
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPSnd_obj_toTwoPointing_toProd : ∀ (X : Pointed), (pointedToTwoPSnd.obj X).toTwoPointing.toProd = (none, some X.point)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.support_esymm'' : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] [Nontrivial R]
  (n : ℕ),
  (MvPolynomial.esymm σ R n).support =
    (Finset.powersetCard n Finset.univ).biUnion fun t => (fun₀ | ∑ i ∈ t, fun₀ | i => 1 => 1).support
-- Std.Http.Protocol.H1.Parser
Std.Http.Protocol.H1.TakeResult.incomplete.injEq : ∀ (data : ByteSlice) (remaining : ℕ) (data_1 : ByteSlice) (remaining_1 : ℕ),
  (Std.Http.Protocol.H1.TakeResult.incomplete data remaining =
      Std.Http.Protocol.H1.TakeResult.incomplete data_1 remaining_1) =
    (data = data_1 ∧ remaining = remaining_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toArray_eq_if_roo : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α],
  r.toArray =
    have init := Std.PRange.UpwardEnumerable.least;
    if init < r.upper then #[init] ++ (init<...r.upper).toArray else #[]
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_epi₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, CategoryTheory.Epi T.mor₁ → T.mor₂ = 0
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instIsScalarTower : ∀ {k : Type u_1} {G : Type u_2} {S₁ : Type u_4} {S₂ : Type u_5} [inst : AddMonoid k] [inst_1 : SMul S₁ S₂]
  [inst_2 : SMulZeroClass S₁ k] [inst_3 : SMulZeroClass S₂ k] [IsScalarTower S₁ S₂ k],
  IsScalarTower S₁ S₂ (SkewMonoidAlgebra k G)
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  Multiset.toFinsupp (s ∩ t) = Multiset.toFinsupp s ⊓ Multiset.toFinsupp t
-- Qq.Match
Qq.Impl.unquoteForMatch : Lean.Expr → Qq.Impl.UnquoteM (Lean.LocalContext × Lean.LocalInstances × Lean.Expr)
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.stepRet.match_1.eq_4 : ∀ (motive : Turing.ToPartrec.Cont → List ℕ → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont)
  (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.comp f k, 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_4 f k v
-- Lean.Parser.Extra
Lean.Parser.nodeWithAntiquot.formatter : String → Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_ennreal_smul_measure_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {c : ENNReal},
  c ≠ 0 → ∀ (μ : MeasureTheory.Measure α), MeasureTheory.ae (c • μ) = MeasureTheory.ae μ
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.eLpNorm_aeeqFun : ∀ {α : Type u_6} {E : Type u_7} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E]
  {p : ENNReal} {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ),
  MeasureTheory.eLpNorm (↑(MeasureTheory.AEEqFun.mk f hf)) p μ = MeasureTheory.eLpNorm f p μ
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_idem : ∀ {α : Type u_1} (M : Matroid α), M.removeLoops.removeLoops = M.removeLoops
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ {X : C} (f : X ⟶ T.obj₃),
      CategoryTheory.CategoryStruct.comp f T.mor₃ = 0 → ∃ g, f = CategoryTheory.CategoryStruct.comp g T.mor₂
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.isSquare_or_isSquare_neg : ∀ {R : Type u_1} {inst : Field R} [self : IsRealClosed R] (x : R), IsSquare x ∨ IsSquare (-x)
-- Mathlib.Topology.Semicontinuity.Basic
IsOpen.upperSemicontinuousOn_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s t : Set α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsOpen s → y ≤ 0 → UpperSemicontinuousOn (s.indicator fun _x => y) t
-- Init.Data.String.OrderInstances
String.Slice.Pos.instLTCoOfNatIntHAddCastUtf8ByteSize : ∀ {s : String.Slice}, Lean.Grind.ToInt.LT s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.imageMonoIsoSource_inv_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).inv
      (CategoryTheory.Limits.image.ι f) =
    f
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Continuous.ennreal_mul : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ENNReal},
  Continuous f →
    Continuous g → (∀ (x : α), f x ≠ 0 ∨ g x ≠ ⊤) → (∀ (x : α), g x ≠ 0 ∨ f x ≠ ⊤) → Continuous fun x => f x * g x
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation)
The limit cone restricted to `Over i'` is still a limit because the diagram is cofiltered.
See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.hc' : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] →
              [inst_2 : CategoryTheory.IsCofiltered I] →
                [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) →
                    (j : A.𝒰D.I₀) → CategoryTheory.Limits.IsLimit (A.c' j)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Oriented angles are continuous when the vectors involved are nonzero.  -/
Orientation.continuousAt_oangle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V × V}, x.1 ≠ 0 → x.2 ≠ 0 → ContinuousAt (fun y => o.oangle y.1 y.2) x
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSlice.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → ℕ → List α → Sort u_2) →
    (x x_1 : ℕ) →
      (x_2 : List α) →
        ((x x_3 : ℕ) → motive x x_3 []) →
          ((m : ℕ) → (xs : List α) → (xs = [] → False) → motive 0 m xs) →
            ((n m : ℕ) → (x : α) → (xs : List α) → motive n.succ m (x :: xs)) → motive x x_1 x_2
-- Mathlib.Algebra.Star.StarRingHom
/-- See Note [custom simps projection]  -/
StarRingEquiv.Simps.symm_apply : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Add A] →
      [inst_1 : Add B] →
        [inst_2 : Mul A] → [inst_3 : Mul B] → [inst_4 : Star A] → [inst_5 : Star B] → (A ≃⋆+* B) → B → A
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α] {l : List α}
  {k k' : α},
  (k == k') = true → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashMap.unitOfList l).getKey! k' = k
-- Mathlib.Analysis.Normed.Order.UpperLower
lowerClosure_interior_subset' : ∀ {α : Type u_1} [inst : NormedCommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] (s : Set α),
  ↑(lowerClosure (interior s)) ⊆ interior ↑(lowerClosure s)