mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Language.Basic
/-- Reports messages on stdout and returns the new total number of errors reported.
If `json` is true, prints messages as JSON (one per line).
If a message's kind is in `severityOverrides`, it will be reported with
the specified severity.
 -/
_private.Lean.Language.Basic.0.Lean.Language.reportMessages : Lean.MessageLog → Lean.Options → Bool → Lean.NameMap Lean.MessageSeverity → ℕ → IO ℕ
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.mkHandlerUnsafe : Lean.Name → Lean.ImportM Lean.Linter.MissingDocs.Handler
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBinaryBicone_snd : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C}
  (b : CategoryTheory.Limits.BinaryBicone X Y), (F.mapBinaryBicone b).snd = F.map b.snd
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_prodMap : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N]
  [Module.Finite R N],
  LinearMap.trace R (M × N) ∘ₗ LinearMap.prodMapLinear R M N M N R =
    LinearMap.id.coprod LinearMap.id ∘ₗ (LinearMap.trace R M).prodMap (LinearMap.trace R N)
-- Init.Data.Array.GetLit
List.drop.eq_3 : ∀ {α : Type u} (n : ℕ) (a : α) (as : List α), List.drop n.succ (a :: as) = List.drop n as
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitLower.eq_1 : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ),
  I.splitLower i x = BoxIntegral.Box.mk' I.lower (Function.update I.upper i (min x (I.upper i)))
-- Lean.Language.Lean.Types
Lean.Language.Lean.instNonemptyCommandResultSnapshot : Nonempty Lean.Language.Lean.CommandResultSnapshot
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeAction : Lean.ToJson Lean.Lsp.CodeAction
-- Mathlib.Data.Sum.Interval
Finset.sumLift₂.eq_1 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f : α₁ → β₁ → Finset γ₁) (g : α₂ → β₂ → Finset γ₂) (a : α₁) (b : β₁),
  Finset.sumLift₂ f g (Sum.inl a) (Sum.inl b) = Finset.map Function.Embedding.inl (f a b)
-- Init.Data.Rat.Lemmas
Rat.ofInt_ofNat : ∀ {n : ℕ}, Rat.ofInt (OfNat.ofNat n) = OfNat.ofNat n
-- Init.Data.Range.Polymorphic.UInt
UInt8.instUpwardEnumerable : Std.PRange.UpwardEnumerable UInt8
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_div_cancel_of_imp' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b : G₀}, (b = 0 → a = 0) → b * (a / b) = a
-- Mathlib.Topology.Order.OrderClosed
/-- The limit of a collection of functions that is frequently antitone on a set is antitone on
that set.  -/
antitoneOn_of_frequently_antitoneOn_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {ι : Type u_1}
  {l : Filter ι} [inst_2 : Preorder β] {F : ι → β → α} {f : β → α} {s : Set β},
  (∃ᶠ (i : ι) in l, AntitoneOn (F i) s) → (∀ x ∈ s, Filter.Tendsto (fun i => F i x) l (nhds (f x))) → AntitoneOn f s
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X X' : C}
  (e : F.CorepresentableBy X) (e' : F.CorepresentableBy X'),
  (e.uniqueUpToIso e').inv =
    (CategoryTheory.Coyoneda.fullyFaithful.preimage
        (CategoryTheory.NatIso.ofComponents
            (fun Z =>
              { hom := TypeCat.ofHom (⇑e.homEquiv.symm ∘ ⇑e'.homEquiv),
                inv := TypeCat.ofHom (⇑e'.homEquiv.symm ∘ ⇑e.homEquiv), hom_inv_id := ⋯, inv_hom_id := ⋯ })
            ⋯).inv).unop
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S],
  Ideal.relNorm R = Ideal.relNorm R
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.zeroHomClass : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N], ZeroHomClass (ZeroHom M N) M N
-- Mathlib.Data.Nat.PrimeFin
Nat.mem_primeFactors_iff_mem_primeFactorsList : ∀ {n p : ℕ}, p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList
-- Mathlib.Computability.RecursiveIn
RecursiveIn.of_eq : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {O : Set (ℕ →. ℕ)} {f g : α →. σ},
  RecursiveIn O f → (∀ (x : α), f x = g x) → RecursiveIn O g
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_ofLE : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A B C : DiscreteQuotient X} (h₁ : A ≤ B) (h₂ : B ≤ C)
  (x : Quotient A.toSetoid), DiscreteQuotient.ofLE h₂ (DiscreteQuotient.ofLE h₁ x) = DiscreteQuotient.ofLE ⋯ x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.ne_zero_of_not_isOrtho_self : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {Q : QuadraticMap R M N} (x : M), ¬Q.IsOrtho x x → x ≠ 0
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instMaxOfSeparatelyContinuousAdd.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousAdd G],
  OpenNormalAddSubgroup.instMaxOfSeparatelyContinuousAdd =
    { max := fun U V => { toOpenAddSubgroup := U.toOpenAddSubgroup ⊔ V.toOpenAddSubgroup, isNormal' := ⋯ } }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → (1 < a⁻¹ ↔ a < 1)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app : ∀ {X : AlgebraicGeometry.Scheme} (X_1 : X.Opensᵒᵖ),
  AlgebraicGeometry.Scheme.restrictFunctorΓ.inv.app X_1 = X.presheaf.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Algebra.Quaternion
/-- The equivalence between the quaternions over `R` and `Fin 4 → R`.  -/
Quaternion.equivTuple : (R : Type u_1) → [inst : Zero R] → [inst_1 : One R] → [inst_2 : Neg R] → Quaternion R ≃ (Fin 4 → R)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.epi_of_base_surjective_of_stalk_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC]
  [inst_2 : CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
  [(CategoryTheory.forget C).ReflectsIsomorphisms] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base) →
    (∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.Mono (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x)) →
      CategoryTheory.Epi f
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.comp_symm_eq : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_14} (f : M₂ → α) (g : M₁ → α), g ∘ ⇑e₁₂.symm = f ↔ g = f ∘ ⇑e₁₂
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- Auxiliary definition for `ProbabilityTheory.Kernel.condKernel`.
A conditional kernel for `κ : Kernel α (γ × ℝ)` where `γ` is countably generated.  -/
ProbabilityTheory.Kernel.condKernelReal : {α : Type u_1} →
  {γ : Type u_3} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [MeasurableSpace.CountablyGenerated γ] →
          (κ : ProbabilityTheory.Kernel α (γ × ℝ)) →
            [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel (α × γ) ℝ
-- Mathlib.Algebra.Group.End
MulAut.apply_inv_self : ∀ (M : Type u_2) [inst : Mul M] (e : MulAut M) (m : M), e (e⁻¹ m) = m
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.ext : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (f g : c' ⟶ c), f.hom = g.hom → f = g
-- Lean.Elab.Tactic.Basic
_private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.eval : Lean.Syntax →
  Lean.Elab.Tactic.SavedState →
    List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Tactic.Tactic) →
      Array Lean.Elab.Tactic.EvalTacticFailure → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Tactic.Linter.Header
/-- `getImportIds s` takes as input `s : Syntax`.
It returns the array of all `import` identifiers in `s`.  -/
Mathlib.Linter.getImportIds : Lean.Syntax → Array Lean.Syntax
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (r₁ r₂ : ℤ) (x : M) {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M},
  l₁.eval * l₂.eval = l.eval → ((r₁, x) ::ᵣ l₁).eval * ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_eq_support_biUnion_support : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R) [inst_1 : DecidableEq σ],
  p.vars = p.support.biUnion Finsupp.support
-- Lean.Elab.Tactic.RCases
/-- Enables the 'unused rcases pattern' linter. This will warn when a pattern is ignored by
`rcases`, `rintro`, `ext` and similar tactics.
 -/
Lean.Elab.Tactic.RCases.linter.unusedRCasesPattern : Lean.Option Bool
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- A presheaf is a sheaf after composing with a universe lift if and only if it is a sheaf.  -/
CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (J : CategoryTheory.GrothendieckTopology C),
  CategoryTheory.Presieve.IsSheaf J (P.comp CategoryTheory.uliftFunctor.{w', w}) ↔ CategoryTheory.Presieve.IsSheaf J P
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.prod_coe : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  {M' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (q₁ : Submodule R M'), ↑(p.prod q₁) = ↑p ×ˢ ↑q₁
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.πE_map_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₂ f₁ f₂ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁' f₂') (n₀ n₁ n₂ : ℤ),
  autoParam (β = CategoryTheory.ComposableArrows.homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯)
      CategoryTheory.Abelian.SpectralObject.πE_map._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_map._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_map._auto_5) {Z : C}
      (h : X.E f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
          (CategoryTheory.CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) h) =
        CategoryTheory.CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁' f₂' β n₁)
          (CategoryTheory.CategoryStruct.comp (X.πE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) h)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.id : ∀ {α : Type u} [inst : UniformSpace α], IsUniformInducing id
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasStrictDerivAt_intCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) [inst_3 : IntCast F] (z : ℤ), HasStrictDerivAt (↑z) 0 x
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.singleton_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (X Y : C),
  CategoryTheory.ObjectProperty.singleton X Y ↔ X = Y
-- Mathlib.Topology.Instances.Rat
Rat.isEmbedding_coe_real : Topology.IsEmbedding Rat.cast
-- Lean.Structure
/-- Returns the transitive closure of all parent structures of the structure.
This is the same as `Lean.getStructureResolutionOrder` but without including `structName`.
 -/
Lean.getAllParentStructures : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Array Lean.Name)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.r.eq_1 : ∀ (z : UpperHalfPlane), EisensteinSeries.r z = min z.im √(EisensteinSeries.r1 z)
-- Mathlib.Data.List.TakeDrop
List.length_dropSlice_lt : ∀ {α : Type u} (i j : ℕ), 0 < j → ∀ (xs : List α), i < xs.length → (List.dropSlice i j xs).length < xs.length
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Filter.EventuallyEq.iteratedDeriv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) {f g : 𝕜 → F} {x : 𝕜}, f =ᶠ[nhds x] g → iteratedDeriv n f x = iteratedDeriv n g x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.documentation? : Lean.Lsp.ResolvableCompletionItem → Option Lean.Lsp.MarkupContent
-- Lean.Widget.Diff
/-- Modifies `goalsAfter` with additional information about how it is different to `goalsBefore`.
If `useAfter` is `true` then `igs₁` is the set of interactive goals _after_ the tactic has been applied.
Otherwise `igs₁` is the set of interactive goals _before_.  -/
Lean.Widget.diffInteractiveGoals : Bool → Lean.Elab.TacticInfo → Lean.Widget.InteractiveGoals → Lean.MetaM Lean.Widget.InteractiveGoals
-- Lean.Meta.Tactic.Grind.Cases
/-- Returns `true` if `s` contains a `declName`.  -/
Lean.Meta.Grind.CasesTypes.contains : Lean.Meta.Grind.CasesTypes → Lean.Name → Bool
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.linearEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [inst_7 : IsLocalizedModule S f]
  [inst_8 : IsLocalizedModule S g] (x : M), (IsLocalizedModule.linearEquiv S f g).symm (g x) = f x
-- Mathlib.RepresentationTheory.Basic
/-- The dual of a representation `ρ` of `G` on a module `V`, given by `(dual ρ) g f = f ∘ₗ (ρ g⁻¹)`,
where `f : Module.Dual k V`.
 -/
Representation.dual : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module k V] → Representation k G V → Representation k G (Module.Dual k V)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.bot_toAddSubgroup : ∀ {R : Type u_4} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], ⊥.toAddSubgroup = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
/-- The pullback cone attached to a commutative square.  -/
CategoryTheory.Square.pullbackCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (sq : CategoryTheory.Square C) → CategoryTheory.Limits.PullbackCone sq.f₂₄ sq.f₃₄
-- Lean.ExtraModUses
Lean.instBEqExtraModUse : BEq Lean.ExtraModUse
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instDistribLattice : DistribLattice ℚ
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.coe_coe : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [inst_3 : OneHomClass F M N] (f : F), ⇑↑f = ⇑f
-- Mathlib.Algebra.Opposites
MulOpposite.op_eq_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : α), MulOpposite.op a = 0 ↔ a = 0
-- Mathlib.Combinatorics.Quiver.Symmetric
_private.Mathlib.Combinatorics.Quiver.Symmetric.0.Quiver.Path.reverse.match_1.eq_1 : ∀ {V : Type u_2} [inst : Quiver V] {a : V} (motive : (x : V) → Quiver.Path a x → Sort u_3)
  (h_1 : Unit → motive a Quiver.Path.nil) (h_2 : (x b : V) → (p : Quiver.Path a b) → (e : b ⟶ x) → motive x (p.cons e)),
  (match a, Quiver.Path.nil with
    | .(a), Quiver.Path.nil => h_1 ()
    | x, p.cons e => h_2 x b p e) =
    h_1 ()
-- Lean.Elab.Binders
/-- Postpone elaboration of the value until after the body is elaborated.  -/
Lean.Elab.Term.LetConfig.postponeValue : Lean.Elab.Term.LetConfig → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.instCreatesFiniteCoproductsOfCreatesFiniteColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteColimits F] → CategoryTheory.Limits.CreatesFiniteCoproducts F
-- Init.Data.UInt.Bitwise
UInt8.ofFin_shiftRight : ∀ (a b : Fin UInt8.size), ↑b < 8 → UInt8.ofFin (a >>> b) = UInt8.ofFin a >>> UInt8.ofFin b
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The dense Grothendieck topology.

See https://ncatlab.org/nlab/show/dense+topology, or [MM92] Chapter III, Section 2, example (e).
 -/
CategoryTheory.GrothendieckTopology.dense : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C
-- Mathlib.Algebra.Star.Basic
/-- A commutative star monoid is a star module over itself via `Monoid.toMulAction`.  -/
StarMul.toStarModule : ∀ {R : Type u} [inst : CommMonoid R] [inst_1 : StarMul R], StarModule R R
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mk_X_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0),
  (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_closedBall_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, x ∈ Metric.closedBall y ε ↔ y ∈ Metric.closedBall x ε
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_sub : ∀ {d : ℤ} (z w : ℤ√d), (z - w).re = z.re - w.re
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Result.step.sizeOf_spec : ∀ (e' proof : Lean.Expr) (done contextDependent : optParam Bool false),
  sizeOf (Lean.Meta.Sym.Simp.Result.step e' proof done contextDependent) =
    1 + sizeOf e' + sizeOf proof + sizeOf done + sizeOf contextDependent
-- Mathlib.Algebra.Quaternion
instSubsingletonQuaternion : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] [Subsingleton R], Subsingleton (Quaternion R)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- A group algebra is spanned by its group-like elements.  -/
MonoidAlgebra.span_isGroupLikeElem : ∀ {R : Type u_1} {A : Type u_3} {G : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  Submodule.span A {a | IsGroupLikeElem R a} = ⊤
-- Init.Control.Lawful.Instances
EStateM.adaptExcept.eq_1 : ∀ {ε σ α ε' : Type u} (f : ε → ε') (x : EStateM ε σ α) (s : σ),
  EStateM.adaptExcept f x s =
    match x s with
    | EStateM.Result.error e s => EStateM.Result.error (f e) s
    | EStateM.Result.ok a s => EStateM.Result.ok a s
-- Lean.Meta.TransparencyMode
Lean.Meta.TransparencyMode.toString : Lean.Meta.TransparencyMode → String
-- Mathlib.Data.Finset.Defs
Finset.coe_sort_coe : ∀ {α : Type u_1} (s : Finset α), ↑↑s = ↥s
-- Mathlib.Topology.MetricSpace.IsometricSMul
instIsIsometricSMulMulOpposite : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X],
  IsIsometricSMul M Xᵐᵒᵖ
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_smul : ∀ {k : Type u} {G : Type v} [inst : CommSemiring k] [inst_1 : Monoid G] {M N : Type w} [inst_2 : AddCommGroup M]
  [inst_3 : AddCommGroup N] [inst_4 : Module k M] [inst_5 : Module k N] {σ : Representation k G M}
  {ρ : Representation k G N} (f : σ.IntertwiningMap ρ) (r : k), Rep.ofHom (r • f) = r • Rep.ofHom f
-- Mathlib.Topology.Order.Compact
atTop_le_cocompact : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [NoMaxOrder α] [ClosedIciTopology α],
  Filter.atTop ≤ Filter.cocompact α
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.interpretParserDescr' : Lean.ParserDescr → Lean.CoreM Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_zero_right : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : Multiset α}, Multiset.Rel r a 0 ↔ a = 0
-- Mathlib.FieldTheory.KummerExtension
autAdjoinRootXPowSubCEquiv_symm_smul : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [inst_1 : NeZero n]
  (σ : AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)),
  ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) =
    σ (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a))
-- Mathlib.Data.Finset.Preimage
Finset.disjoint_preimage : ∀ {α : Type u} {β : Type v} {f : α → β} {s t : Finset β} {hs : Set.InjOn f (f ⁻¹' ↑s)} {ht : Set.InjOn f (f ⁻¹' ↑t)},
  Disjoint s t → Disjoint (s.preimage f hs) (t.preimage f ht)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticCode.string : String → Lean.Lsp.DiagnosticCode
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toLinearEquiv_symm_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V) (v : V), (SpecialLinearGroup.toLinearEquiv A).symm v = (fun x => ↑A⁻¹ x) v
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.Util.Export
Lean.Export.Entry.expr : Lean.Expr → Lean.Export.Entry
-- Init.Omega.Constraint
Lean.Omega.combo_sat' : ∀ (s t : Lean.Omega.Constraint) (a : ℤ) (x : Lean.Omega.Coeffs) (b : ℤ) (y v : Lean.Omega.Coeffs),
  s.sat' x v = true →
    t.sat' y v = true → (Lean.Omega.Constraint.combo a s b t).sat' (Lean.Omega.Coeffs.combo a x b y) v = true
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.lift_surjective_of_surjective : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  (φ : G →+ M), Function.Surjective ⇑φ → ∀ (HN : N ≤ φ.ker), Function.Surjective ⇑(QuotientAddGroup.lift N φ HN)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.lie_lieDerivation_apply : ∀ (R : Type u_1) (L : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x y : L)
  (D : LieDerivation R L M), ⁅x, D⁆ y = ⁅y, D x⁆
-- Mathlib.Data.Complex.Basic
Complex.ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w
-- Init.Data.List.ToArray
Array.back.eq_1 : ∀ {α : Type u} (xs : Array α) (h : 0 < xs.size), xs.back h = xs[xs.size - 1]
-- Lean.Meta.Transform
/-- Applies beta reduction to all beta-reducible subexpressions in `e`.  -/
Lean.Core.betaReduce : Lean.Expr → Lean.CoreM Lean.Expr