mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_right_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : C),
  φ.rightUnitor.hom.right.app X = CategoryTheory.CategoryStruct.id (φ.right.obj X)
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- Any category with coproducts and coequalizers has all colimits.  -/
CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.Limits.HasCoequalizers C], CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.category.inj : ∀ {catName declName : Lean.Name} {behavior : Lean.Parser.LeadingIdentBehavior} {catName_1 declName_1 : Lean.Name}
  {behavior_1 : Lean.Parser.LeadingIdentBehavior},
  Lean.Parser.ParserExtension.Entry.category catName declName behavior =
      Lean.Parser.ParserExtension.Entry.category catName_1 declName_1 behavior_1 →
    catName = catName_1 ∧ declName = declName_1 ∧ behavior = behavior_1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instNonemptySavedState : Nonempty Lean.Elab.Term.SavedState
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Normalizes `e` if it qualifies as a candidate pattern, and returns
`some p` where `p` is the normalized pattern.

`argKinds == NormalizePattern.getPatternArgKinds e.getAppFn e.getAppNumArgs`

If `minIndexable == true`, then enforces the minimal indexable subexpression condition.
That is, an indexable subexpression is minimal if there is no smaller indexable subexpression
whose head constant has at least as high priority.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.normalizePattern? : Lean.Expr →
  Array Lean.Meta.Grind.NormalizePattern.PatternArgKind → Bool → Lean.Meta.Grind.CollectorM✝ (Option Lean.Expr)
-- Mathlib.Data.Sum.Interval
Sum.Ioi_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderTop β] (b : β), Finset.Ioi (Sum.inr b) = Finset.map Function.Embedding.inr (Finset.Ioi b)
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint, then there is the natural isomorphism
`A ⊗[R] B ≃ₐ[R] A ⊔ B` induced by multiplication in `S`.  -/
Subalgebra.LinearDisjoint.mulMap : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] → {A B : Subalgebra R S} → A.LinearDisjoint B → TensorProduct R ↥A ↥B ≃ₐ[R] ↥(A ⊔ B)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.forM_eq_forM_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m' : Type w → Type w'} {β : Type v} {m : Std.DHashMap α fun x => β}
  [inst : Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}},
  Std.DHashMap.forM f m = Array.forM (fun a => f a.1 a.2) (Std.DHashMap.Const.toArray m)
-- Init.NotationExtra
unexpandMkArray1 : Lean.PrettyPrinter.Unexpander
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {b : n → α} [inst : DecidableEq m]
  {i' : m}, M.updateRow i b i' j = if i' = i then b j else M i' j
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The right inverse of matrix A is unique when existing.  -/
Matrix.right_inv_eq_right_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B C : Matrix n n α},
  A * B = 1 → A * C = 1 → B = C
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
/-- Given any linearly ordered commutative group with zero `α`, this is the order isomorphism
between `WithZero αˣ` with `α`.  -/
OrderIso.withZeroUnits : {α : Type u_1} → [inst : LinearOrderedCommGroupWithZero α] → WithZero αˣ ≃o α
-- Mathlib.Topology.Algebra.ConstMulAction
vadd_closure_orbit_subset : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α]
  [ContinuousConstVAdd M α] (c : M) (x : α), c +ᵥ closure (AddAction.orbit M x) ⊆ closure (AddAction.orbit M x)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.get? k = t.get? k'
-- Mathlib.Data.Set.Lattice
Set.iUnion_insert_eq_range_union_iUnion : ∀ {β : Type u_2} {ι : Type u_12} (x : ι → β) (t : ι → Set β), ⋃ i, insert (x i) (t i) = Set.range x ∪ ⋃ i, t i
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_zsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] (s : Finset α) (n : ℤ), ↑(n • s) = n • ↑s
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.comp.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [inst_1 : Wₗ.HasPullbacksAgainst Wᵣ] [inst_2 : Wₗ.IsStableUnderBaseChangeAgainst Wᵣ]
  [inst_3 : Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [inst_4 : Wₗ.IsStableUnderComposition]
  [inst_5 : Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ S₁_1 : CategoryTheory.Span Wₗ Wᵣ c c'),
  S₁ = S₁_1 → ∀ (S₂ S₂_1 : CategoryTheory.Span Wₗ Wᵣ c' c''), S₂ = S₂_1 → S₁.comp S₂ = S₁_1.comp S₂_1
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.toZeroMemClass : ∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : AddZeroClass M} {inst_1 : SetLike S M}
  [self : AddSubmonoidClass S M], ZeroMemClass S M
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- **Alias** of `Left.pow_le_one_of_le`. -/
pow_le_one' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M}, a ≤ 1 → ∀ (n : ℕ), a ^ n ≤ 1
-- Mathlib.Algebra.Order.Ring.Cast
Int.nneg_mul_add_sq_of_abs_le_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {x : R} (n : ℤ),
  |x| ≤ 1 → 0 ≤ ↑n * x + ↑n * ↑n
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smulCommClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  SMulCommClass (Set α) (Set β) (Set γ)
-- Mathlib.CategoryTheory.DinatTrans
CategoryTheory.DinatTrans.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)}
  (app : (X : C) → (F.obj (Opposite.op X)).obj X ⟶ (G.obj (Opposite.op X)).obj X)
  (dinaturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp ((F.map f.op).app X)
            (CategoryTheory.CategoryStruct.comp (app X) ((G.obj (Opposite.op X)).map f)) =
          CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op Y)).map f)
            (CategoryTheory.CategoryStruct.comp (app Y) ((G.map f.op).app Y)))
      CategoryTheory.DinatTrans.dinaturality._autoParam)
  (app_1 : (X : C) → (F.obj (Opposite.op X)).obj X ⟶ (G.obj (Opposite.op X)).obj X)
  (dinaturality_1 :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp ((F.map f.op).app X)
            (CategoryTheory.CategoryStruct.comp (app_1 X) ((G.obj (Opposite.op X)).map f)) =
          CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op Y)).map f)
            (CategoryTheory.CategoryStruct.comp (app_1 Y) ((G.map f.op).app Y)))
      CategoryTheory.DinatTrans.dinaturality._autoParam),
  ({ app := app, dinaturality := dinaturality } = { app := app_1, dinaturality := dinaturality_1 }) = (app = app_1)
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.asIdeal : {R : Type u_1} → [inst : CommSemiring R] → PrimeSpectrum R → Ideal R
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, local version for any measure.
Let filters `l` and `l'` be related by `TendstoIxxClass Ioc`.
If `f` has a finite limit `c` at `l' ⊓ ae μ`, where `μ` is a measure
finite at `l'`, then `∫ x in u..v, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, 1 ∂μ)` as both
`u` and `v` tend to `l`.

See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae` for a version assuming
`[intervalIntegral.FTCFilter a l l']` and `[MeasureTheory.IsLocallyFiniteMeasure μ]`. If `l` is one
of `𝓝[≥] a`, `𝓝[≤] a`, `𝓝 a`, then it's easier to apply the non-primed version.  The primed version
also works, e.g., for `l = l' = atTop`.

We use integrals of constants instead of measures because this way it is easier to formulate
a statement that works in both cases `u ≤ v` and `v ≤ u`.  -/
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae' : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {c : E}
  {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [l'.IsMeasurablyGenerated]
  [Filter.TendstoIxxClass Set.Ioc l l'],
  StronglyMeasurableAtFilter f l' μ →
    Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c) →
      μ.FiniteAtFilter l' →
        Filter.Tendsto u lt l →
          Filter.Tendsto v lt l →
            (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t =>
              ∫ (x : ℝ) in u t..v t, 1 ∂μ
-- Init.Data.String.Lemmas.FindPos
String.posGE_inc : ∀ {s : String} {p : String.Pos.Raw} {h : p.inc ≤ s.rawEndPos}, s.posGE p.inc h = s.posGT p h
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- Build an `AlgEquiv` from an isomorphism in the category `AlgCat R`.  -/
CategoryTheory.Iso.toAlgEquiv : {R : Type u} → [inst : CommRing R] → {X Y : AlgCat R} → (X ≅ Y) → ↑X ≃ₐ[R] ↑Y
-- Mathlib.GroupTheory.PushoutI
/-- A `Pair d i` is a word in the coproduct, `Coprod G`, the `tail`, and an element of the group `G i`,
the `head`. The first letter of the `tail` must not be an element of `G i`.
Note that the `head` may be `1`. Every letter in the `tail` must be in the transversal given by `d`.
Similar to `Monoid.CoprodI.Pair` except every letter must be in the transversal
(not including the head letter).  -/
Monoid.PushoutI.NormalWord.Pair : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} → Monoid.PushoutI.NormalWord.Transversal φ → ι → Type (max u_1 u_2)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α},
  t.max? = some km → km ∈ t
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_eq_univ : ∀ {α : Type u} {s : Set α} [inst : Fintype α] {h : s.Finite}, h.toFinset = Finset.univ ↔ s = Set.univ
-- Mathlib.Data.List.Rotate
List.get_rotate_one : ∀ {α : Type u} (l : List α) (k : Fin (l.rotate 1).length), (l.rotate 1).get k = l.get ⟨(↑k + 1) % l.length, ⋯⟩
-- Mathlib.Topology.MetricSpace.Thickening
/-- **Alias** of `Metric.eventually_notMem_cthickening_of_infEDist_pos`.

---

An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
closed `δ`-thickening of `E` for small enough positive `δ`.  -/
Metric.eventually_notMem_cthickening_of_infEdist_pos : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {E : Set α} {x : α},
  x ∉ closure E → ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.cthickening δ E
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunctionAux_false : ∀ {c : ℝ} {f : ℕ → Bool} {n : ℕ}, f n = false → Cardinal.cantorFunctionAux c f n = 0
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.dirac.eq_1 : ∀ {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : MeasurableSpace β]
  (x : β) (v : M),
  MeasureTheory.VectorMeasure.dirac x v =
    { measureOf' := fun s => if MeasurableSet s ∧ x ∈ s then v else 0, empty' := ⋯, not_measurable' := ⋯,
      m_iUnion' := ⋯ }
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- Base cases: `b = 0`, `b = 1`, `a = 0`, `a = 1`.  -/
Mathlib.Meta.NormNum.jacobiSymNat.zero_right : ∀ (a : ℕ), Mathlib.Meta.NormNum.jacobiSymNat a 0 = 1
-- Mathlib.NumberTheory.Real.Irrational
Rat.not_irrational : ∀ (q : ℚ), ¬Irrational ↑q
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_of_isRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [G.IsRightAdjoint], G.PreservesZeroMorphisms
-- Mathlib.CategoryTheory.Action.Basic
Action.instIsEquivalenceFunctorSingleObjFunctor : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G],
  Action.FunctorCategoryEquivalence.functor.IsEquivalence
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.topologicalClosure_mono : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : SeparatelyContinuousAdd M]
  {s t : AddSubsemigroup M}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.Analysis.Convex.EGauge
div_le_egauge_closedBall : ∀ (𝕜 : Type u_1) [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (r : NNReal) (x : E), ‖x‖ₑ / ↑r ≤ egauge 𝕜 (Metric.closedBall 0 ↑r) x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, (m.erase k).getD k fallback = fallback
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} (f : α → β → γ),
  m₁.Equiv m₂ → (Std.HashMap.map f m₁).Equiv (Std.HashMap.map f m₂)
-- Mathlib.Data.Set.Prod
Antitone.set_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] {f : α → Set β} {g : α → Set γ},
  Antitone f → Antitone g → Antitone fun x => f x ×ˢ g x
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.add_right : ∀ {α : Type u} {β : Type v} {l : Filter α} [inst : Add β] {f₁ f₂ f₃ : α → β}, f₁ =ᶠ[l] f₂ → f₁ + f₃ =ᶠ[l] f₂ + f₃
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.tmul_coe_mul_one_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {j₁ : ι} (a₁ : A) (b₁ : ↥(ℬ j₁)) (b₂ : B),
  a₁ ᵍ⊗ₜ[R] ↑b₁ * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] (↑b₁ * b₂)
-- Lean.Meta.Sym.Pattern
/-- Structural definitional equality for universe levels.
Uses `tryApproxMaxMax` to handle `max` commutativity when one argument matches structurally.
Attempts metavariable assignment in both directions if structural matching fails.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isLevelDefEqS : Lean.Level → Lean.Level → Lean.MetaM Bool
-- Init.Data.SInt.Lemmas
Int8.neg_ne_zero : ∀ {a : Int8}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.Analysis.Normed.Module.Basic
/-- In a normed algebra, the inclusion of the base field in the extended field is an isometry.  -/
algebraMap_isometry : ∀ (𝕜 : Type u_1) (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  [NormOneClass 𝕜'], Isometry ⇑(algebraMap 𝕜 𝕜')
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mult_isReal : ∀ {K : Type u_1} [inst : Field K] (w : { w // w.IsReal }), (↑w).mult = 1
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instZero : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] → [inst_6 : Module R W] → [inst_7 : TopologicalSpace W] → Zero (P →ᴬ[R] W)
-- Mathlib.NumberTheory.NumberField.ProductFormula
/-- For any non-zero `x` in `K`, the product of `w x`, where `w` runs over `FinitePlace K`, is
equal to the inverse of the absolute value of `Algebra.norm ℚ x`.  -/
NumberField.FinitePlace.prod_eq_inv_abs_norm : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : K},
  x ≠ 0 → ∏ᶠ (w : NumberField.FinitePlace K), w x = ↑|(Algebra.norm ℚ) x|⁻¹
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_one_right : ∀ (n : ℕ), n.factorization 1 = 0
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Debug `grind` by identifying places where it does not yet supersede `ring`.  -/
ringToGrindRegressions : Mathlib.TacticAnalysis.Config
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ico_toDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  Finset.Ico (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioc b a)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.rename_hsymm : ∀ {τ : Type u_2} (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : Fintype τ]
  [inst_3 : DecidableEq σ] [inst_4 : DecidableEq τ] (n : ℕ) (e : σ ≃ τ),
  (MvPolynomial.rename ⇑e) (MvPolynomial.hsymm σ R n) = MvPolynomial.hsymm τ R n
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_le_one : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ}, κ.fst ≤ ν → ∀ (n : ℕ) (a : α) (x : γ) (s : Set β), κ.densityProcess ν n a x s ≤ 1
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
BialgEquiv.toHopfAlgIso_trans : ∀ {R : Type u} [inst : CommRing R] {X Y Z : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : Ring Z]
  [inst_4 : HopfAlgebra R X] [inst_5 : HopfAlgebra R Y] [inst_6 : HopfAlgebra R Z] (e : X ≃ₐc[R] Y) (f : Y ≃ₐc[R] Z),
  (e.trans f).toHopfAlgIso = e.toHopfAlgIso ≪≫ f.toHopfAlgIso
-- Mathlib.Analysis.Quaternion
/-- `QuaternionAlgebra.linearEquivTuple` as a `LinearIsometryEquiv`.  -/
Quaternion.linearIsometryEquivTuple : Quaternion ℝ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4)
-- Init.Omega.Int
Lean.Omega.Int.ofNat_pos_of_pos : ∀ {a : ℕ}, 0 < a → 0 < ↑a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.all_eq_true_iff_forall_mem_getKey_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {p : α → β → Bool}, m.WF → (m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p (m.getKey a h) m[a] = true)
-- Mathlib.Data.Finsupp.BigOperators
Multiset.support_sum_eq : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] (s : Multiset (ι →₀ M)),
  Multiset.Pairwise (Function.onFun Disjoint Finsupp.support) s → s.sum.support = (Multiset.map Finsupp.support s).sup
-- Mathlib.Data.Seq.Computation
Computation.instInhabited : {α : Type u} → Inhabited (Computation α)
-- Init.Data.SInt.Lemmas
Int8.ofInt_tmod : ∀ {a b : ℤ},
  Int8.minValue.toInt ≤ a →
    a ≤ Int8.maxValue.toInt →
      Int8.minValue.toInt ≤ b → b ≤ Int8.maxValue.toInt → Int8.ofInt (a.tmod b) = Int8.ofInt a % Int8.ofInt b
-- Init.Data.Vector.MapIdx
/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction.  -/
Vector.mk_mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {n : ℕ} {x : α} {i : ℕ} {xs : Vector α n}, (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineOpenCover_X : ∀ (X : AlgebraicGeometry.Scheme) (x : ↑X.toTopCat), X.affineOpenCover.X x = Classical.choose ⋯
-- Mathlib.Order.Concept
Concept.swapEquiv_apply : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (a : (Concept α β r)ᵒᵈ),
  Concept.swapEquiv a = (Concept.swap ∘ ⇑OrderDual.ofDual) a
-- Mathlib.Analysis.Normed.Module.Complemented
Submodule.ClosedComplemented.of_isCompl_isClosed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E},
  IsCompl p q → IsClosed ↑p → IsClosed ↑q → Submodule.ClosedComplemented p
-- Mathlib.Topology.Category.TopCat.Opens
IsOpenMap.functorFullOfMono : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) [H : CategoryTheory.Mono f],
  hf.functor.Full
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.coe_mapEquivMonic_comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S) (g : S →ₐ[R] T),
  ↑((MvPolynomial.mapEquivMonic R T n) (g.comp f)) = Polynomial.map ↑g ↑((MvPolynomial.mapEquivMonic R S n) f)
-- Lean.Util.FindMVar
Lean.FindMVar.Visitor : Type
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
/-- The number of cycles of given length  -/
AlternatingGroup.card_of_cycleType_singleton : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {n : ℕ},
  2 ≤ n →
    n ≤ Fintype.card α →
      {g | (↑g).cycleType = {n}}.card = if Odd n then (n - 1).factorial * (Fintype.card α).choose n else 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalSemiring : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Semigroup M] → NonUnitalSemiring (MonoidAlgebra R M)
-- Mathlib.RingTheory.WittVector.MulP
_private.Mathlib.RingTheory.WittVector.MulP.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.Algebra.Group.Finsupp
Finsupp.erase_add_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (f : ι →₀ M), (Finsupp.erase a f + fun₀ | a => f a) = f
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Alias** of `EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist`.

---

**Law of sines** (sine rule), angle-at-point form.  -/
EuclideanGeometry.law_sin : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ : P),
  Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (EuclideanGeometry.angle p₃ p₁ p₂) * dist p₃ p₁
-- Mathlib.Order.Concept
lowerPolar_le : ∀ {β : Type u_3} {t : Set β} [inst : LE β], lowerPolar (fun x1 x2 => x1 ≤ x2) t = lowerBounds t
-- Init.Data.UInt.BasicAux
/-- Converts 8-bit unsigned integers to 16-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.toUInt16 : UInt8 → UInt16
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context : Type
-- Aesop.Forward.Match.Types
Aesop.instBEqCompleteMatch.beq : Aesop.CompleteMatch → Aesop.CompleteMatch → Bool
-- Mathlib.Topology.Algebra.Support
tsupport_fun_zero : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X], (tsupport fun x => 0) = ∅
-- Mathlib.Analysis.Calculus.FDeriv.Mul
differentiableAt_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedDivisionRing R]
  [inst_2 : NormedAlgebra 𝕜 R] {x : R}, x ≠ 0 → DifferentiableAt 𝕜 Inv.inv x
-- Mathlib.Order.Disjoint
top_disjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a : α}, Disjoint ⊤ a ↔ a = ⊥
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsCoseparator (Opposite.op G) ↔ CategoryTheory.IsSeparator G