mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ_eq_succ_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.InfinitelyUpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] {a b : α}, Std.PRange.succ a = Std.PRange.succ b ↔ a = b
-- Mathlib.Data.Finset.Basic
Finset.disjUnion_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (h : Disjoint s t), s.disjUnion t h = s ∪ t
-- Mathlib.SetTheory.Cardinal.NatCard
/-- A custom induction principle for finite types, by strong induction on `Nat.card`:
the base case is a subsingleton type, and the induction step is for nontrivial types,
where one can assume the hypothesis for all types of smaller cardinality.  -/
Finite.induction_subsingleton_or_nontrivial : ∀ {P : Type u_4 → Prop} (α : Type u_4) [Finite α],
  (∀ (α : Type u_4) [Finite α] [Subsingleton α], P α) →
    (∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α) →
      P α
-- Init.Data.List.Basic
/-- Applies a function to the corresponding elements of both lists, stopping when there are no more
elements in either list. If one list is shorter than the other, the function is passed `none` for
the missing elements.

Examples:
* `[1, 6].zipWithAll min [5, 2] = [some 1, some 2]`
* `[1, 2, 3].zipWithAll Prod.mk [5, 6] = [(some 1, some 5), (some 2, some 6), (some 3, none)]`
* `[x₁, x₂].zipWithAll f [y] = [f (some x₁) (some y), f (some x₂) none]`
 -/
List.zipWithAll : {α : Type u} → {β : Type v} → {γ : Type w} → (Option α → Option β → γ) → List α → List β → List γ
-- Mathlib.Data.ZMod.Basic
ZMod.nontrivial_iff : ∀ {n : ℕ}, Nontrivial (ZMod n) ↔ n ≠ 1
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.WeaklyEtale f],
  AlgebraicGeometry.WeaklyEtale (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoX₂_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hg : S.g = 0), (S.cyclesIsoX₂ hg).hom = S.iCycles
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- If a nonnegative square matrix `A` is primitive, then `A` is irreducible.  -/
Matrix.IsPrimitive.isIrreducible : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R} [inst_2 : Fintype n]
  [IsOrderedRing R] [PosMulStrictMono R] [Nontrivial R] [inst_6 : DecidableEq n], A.IsPrimitive → A.IsIrreducible
-- Mathlib.RingTheory.PowerBasis
PowerBasis.mk.sizeOf_spec : ∀ {R : Type u_7} {S : Type u_8} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [inst_3 : SizeOf R]
  [inst_4 : SizeOf S] (gen : S) (dim : ℕ) (basis : Module.Basis (Fin dim) R S)
  (basis_eq_pow : ∀ (i : Fin dim), basis i = gen ^ ↑i),
  sizeOf { gen := gen, dim := dim, basis := basis, basis_eq_pow := basis_eq_pow } =
    1 + sizeOf gen + sizeOf dim + sizeOf basis
-- Mathlib.Data.Fintype.Sum
Finset.toLeft_eq_empty : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype β] {u : Finset (α ⊕ β)},
  u.toLeft = ∅ ↔ u ⊆ Finset.map Function.Embedding.inr Finset.univ
-- Batteries.Data.ByteArray
ByteArray.get_append_left : ∀ {i : ℕ} {a b : ByteArray} (hlt : i < a.size) (h : optParam (i < (a ++ b).size) ⋯), (a ++ b)[i] = a[i]
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_sub_sub_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), inner 𝕜 (x - y) (x - y) = inner 𝕜 x x - inner 𝕜 x y - inner 𝕜 y x + inner 𝕜 y y
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {n : ℕ}
  (F : CategoryTheory.ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯))),
  (CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows W F hF).isoBot.hom =
    CategoryTheory.CategoryStruct.id (F.obj ⊥)
-- Mathlib.Topology.MetricSpace.PiNat
/-- Equivalence between `X` and its embedding into `∀ i, Y i`.  -/
Metric.PiNatEmbed.toPiNatEquiv : {ι : Type u_2} → (X : Type u_3) → (Y : ι → Type u_4) → (f : (i : ι) → X → Y i) → X ≃ Metric.PiNatEmbed X Y f
-- Mathlib.Topology.Algebra.Order.Field
/-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`.  -/
tendsto_inv_nhdsGT_zero : ∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.Tendsto (fun x => x⁻¹) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop
-- Mathlib.Order.Filter.Map
Filter.image_mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {s : Set α}, s ∈ f → m '' s ∈ Filter.map m f
-- Init.Data.Fin.Basic
Fin.instAndOp : {n : ℕ} → AndOp (Fin n)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.instSymm : ∀ {M : Type u_1} [inst : Monoid M], Std.Symm Associated
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomology_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {A : C} (f₁ f₂ : A ⟶ S.rightHomology),
  f₁ = f₂ ↔
    CategoryTheory.CategoryStruct.comp f₁ S.rightHomologyι = CategoryTheory.CategoryStruct.comp f₂ S.rightHomologyι
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SimplexCategory.toTopHomeo_symm_naturality : ∀ {n m : SimplexCategory} (f : n ⟶ m),
  ⇑m.toTopHomeo.symm ∘ stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f) =
    ⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) ∘ ⇑n.toTopHomeo.symm
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_charFn : ∀ {X : Type u_1} (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : MulZeroOneClass Y] {U : Set X} (hU : IsClopen U),
  ⇑(LocallyConstant.charFn Y hU) = U.indicator 1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_algHom_ext : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Semiring K] [inst_4 : Algebra F K] {s : Set E} ⦃φ₁ φ₂ : ↥(IntermediateField.adjoin F s) →ₐ[F] K⦄,
  (∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) → φ₁ = φ₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.Equation.baseChange : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) {P : Fin 3 → A}, (W'.baseChange A).Equation P → (W'.baseChange B).Equation (⇑f ∘ P)
-- Mathlib.Algebra.NoZeroSMulDivisors.Pi
/-- A special case of `Pi.noZeroSMulDivisors` for non-dependent types. Lean struggles to
synthesize this instance by itself elsewhere in the library.  -/
Function.noZeroSMulDivisors : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [IsDomain α] [inst_2 : AddCommGroup β]
  [inst_3 : Module α β] [NoZeroSMulDivisors α β], NoZeroSMulDivisors α (ι → β)
-- Mathlib.Algebra.RingQuot
/-- `EqvGen (RingQuot.Rel r)` is a ring congruence.  -/
RingQuot.ringCon : {R : Type uR} → [inst : Semiring R] → (R → R → Prop) → RingCon R
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wfImp_getThenInsertIfNew? : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β} {a : α} {b : β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m a b).2
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.lift.eq_1 : ∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (fn : N →* H) (fg : G →* H)
  (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn),
  SemidirectProduct.lift fn fg h = { toFun := fun a => fn a.left * fg a.right, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
BirdDet.Spec.birdDetSpec_succ : ∀ {R : Type u_1} [inst : CommRing R] {k : ℕ} (A : Matrix (Fin (k + 1)) (Fin (k + 1)) R),
  BirdDet.Spec.birdDet A = (-1) ^ k * (BirdDet.Spec.stepEntry A)^[k] A 0 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_zero : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint], 0⁺ = 0
-- Mathlib.Order.Filter.Lift
Filter.lift'_cong : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h₁ h₂ : Set α → Set β}, (∀ s ∈ f, h₁ s = h₂ s) → f.lift' h₁ = f.lift' h₂
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Technical lemma to rewrite suitably the preimage of an intersection under an extended chart, to
bring it into a convenient form to apply derivative lemmas.  -/
extChartAt_preimage_inter_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s t : Set M} [inst_5 : ChartedSpace H M] (x : M),
  ↑(extChartAt I x).symm ⁻¹' (s ∩ t) ∩ Set.range ↑I =
    ↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' t
-- Mathlib.RingTheory.Noetherian.Basic
/-- A version of `isNoetherian_pi` for non-dependent functions. We need this instance because
sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
prove that `ι → ℝ` is finite dimensional over `ℝ`).  -/
isNoetherian_pi' : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_6}
  [Finite ι] [IsNoetherian R M], IsNoetherian R (ι → M)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- From a functor `F : J ⥤ C`, given a terminal object of `J`, construct a cocone for `J`.
In `colimitOfDiagramTerminal` we show it is a colimit cocone.  -/
CategoryTheory.Limits.coconeOfDiagramTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {X : J} → CategoryTheory.Limits.IsTerminal X → (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.Cocone F
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_neg_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddLeftStrictMono α] (a : α) {b : α}, b < 0 → a + b < a
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.fork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂),
  (CategoryTheory.Subfunctor.equalizer.fork f g).pt = (CategoryTheory.Subfunctor.equalizer f g).toFunctor
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        (toOrderHom : α →o β) →
          (∀ ⦃a : α⦄ ⦃b : β⦄, toOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toOrderHom.toFun c = b) → PseudoEpimorphism α β
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lapply_comp_lsingle_same : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : α), Finsupp.lapply a ∘ₗ Finsupp.lsingle a = LinearMap.id
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.desc_inl_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.Limits.pushout.desc (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.Limits.pushout.inr f g) ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pushout f g)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.mk : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E],
  Algebra.IsIntegral F E → (∀ (x : E), IsSeparable F x → x ∈ (algebraMap F E).range) → IsPurelyInseparable F E
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure' : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D₁] [inst_3 : CategoryTheory.Category.{v_2, u_2} D₂]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
  (F : CategoryTheory.Functor D₁ D₂) [h : Φ.IsRightDerivabilityStructure] (e : Φ.functor.comp L₂ ≅ L₁.comp F),
  CategoryTheory.TwoSquare.GuitartExact e.hom
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod_top : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (K : AddSubgroup G),
  K.prod ⊤ = AddSubgroup.comap (AddMonoidHom.fst G N) K
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.reduced : Lean.Expr → Lean.Meta.ReduceMatcherResult
-- Init.Data.UInt.Lemmas
USize.ofNatLT_uInt32ToNat : ∀ (n : UInt32), USize.ofNatLT n.toNat ⋯ = n.toUSize
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.pushArgsAux : Array Lean.Meta.ParamInfo → ℕ → Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_eq_head!_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.minKey! = t.keys.head!
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.zero : ONote.NF 0
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.instMonoid : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : Star A] → Monoid (A →⋆ₐ[R] A)
-- Mathlib.Algebra.Group.AddChar
AddChar.prod_eq_sum : ∀ {ι : Type u_1} {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (s : Finset ι)
  (ψ : ι → AddChar A M), ∏ i ∈ s, ψ i = ∑ i ∈ s, ψ i
-- Mathlib.Algebra.GroupWithZero.Action.TransferInstance
/-- Transfer `SMulWithZero` across an `Equiv`  -/
Equiv.smulWithZero : (M₀ : Type u_2) →
  {A : Type u_3} →
    {B : Type u_4} → (e : A ≃ B) → [inst : Zero M₀] → [inst_1 : Zero B] → [SMulWithZero M₀ B] → SMulWithZero M₀ A
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.restrictScalars_coe_linearMap : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (R₀ : Type u_11)
  [inst_9 : CommSemiring R₀] [inst_10 : Algebra R₀ R] [inst_11 : Algebra R₀ A] [inst_12 : Algebra R₀ B]
  [inst_13 : IsScalarTower R₀ R A] [inst_14 : IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ), ↑R₀ ↑f = ↑(↑R₀ f)
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_card_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {n : ℕ}, Nat.card G ∣ p ^ n → IsPGroup p G
-- Mathlib.Analysis.Normed.Field.Lemmas
UniformContinuousOn.inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} [inst_1 : UniformSpace X] {f : X → α} {s : Set X},
  UniformContinuousOn f s → (f '' s)ᶜ ∈ nhds 0 → UniformContinuousOn f⁻¹ s
-- Mathlib.Analysis.InnerProductSpace.Basic
_private.Mathlib.Analysis.InnerProductSpace.Basic.0.«term⟪_,_⟫_5» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.zero_apply : ∀ {V W : SemiNormedGrp₁} (x : V.carrier), ↑(SemiNormedGrp₁.Hom.hom 0) x = 0
-- Lean.CoreM
/-- This is a temporary workaround for generating better error messages for the compiler. It can be deleted after we
rewrite the remaining parts of the compiler in Lean.   -/
_private.Lean.CoreM.0.Lean.checkUnsupported : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Declaration → m Unit
-- Mathlib.Analysis.Calculus.VectorField
VectorField.pullbackWithin_eq_of_fderivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {M : E ≃L[𝕜] F} {x : E},
  ↑M = fderivWithin 𝕜 f s x → ∀ (V : F → F), VectorField.pullbackWithin 𝕜 f V s x = M.symm (V (f x))
-- Mathlib.Algebra.Quaternion
Quaternion.imK_add : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a + b).imK = a.imK + b.imK
-- Mathlib.Algebra.Algebra.Bilinear
/-- The multiplication in a non-unital non-associative algebra is a bilinear map.

A weaker version of this for semirings exists as `AddMonoidHom.mul`.  -/
LinearMap.mul : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [SMulCommClass R A A] → [IsScalarTower R A A] → A →ₗ[R] A →ₗ[R] A
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_self : ∀ (β : Type u_3) [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β] [inst_2 : IsStrictOrderedRing β],
  ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β β = OrderRingIso.refl β
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degreeLE.eq_1 : ∀ (R : Type u) [inst : Semiring R] (n : WithBot ℕ),
  Polynomial.degreeLE R n = ⨅ k, ⨅ (_ : ↑k > n), (Polynomial.lcoeff R k).ker
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, a ∈ m.insert k ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.SetTheory.Cardinal.Finite
Cardinal.toENat_eq_natCast_iff : ∀ {c : Cardinal.{u_3}} {n : ℕ}, Cardinal.toENat c = ↑n ↔ c = ↑n
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Multiplicativity of leading coefficients  -/
MonomialOrder.leadingCoeff_mul_of_isRegular_left : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  IsRegular (m.leadingCoeff f) → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Composition of a partial equivalence and its inverse is equivalent to
the restriction of the identity to the source.  -/
PartialEquiv.self_trans_symm : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.trans e.symm ≈ PartialEquiv.ofSet e.source
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
nhds_basis_closed_balanced : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [(nhdsWithin 0 {0}ᶜ).NeBot] [RegularSpace E],
  (nhds 0).HasBasis (fun s => s ∈ nhds 0 ∧ IsClosed s ∧ Balanced 𝕜 s) id
-- Std.Async.Timer
_private.Std.Async.Timer.0.Std.Async.Sleep.ofNative.injEq : ∀ (native native_1 : Std.Internal.UV.Timer), ({ native := native } = { native := native_1 }) = (native = native_1)
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_exp_rat_of_odd_num : ∀ (q : ℚ), Odd q.num → IsPrimitiveRoot (Complex.exp (↑Real.pi * Complex.I * ↑q)) (2 * q.den)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Any inner regular Haar measure is invariant under inversion in an abelian group.  -/
MeasureTheory.Measure.IsHaarMeasure.isInvInvariant_of_innerRegular : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.InnerRegular],
  μ.IsInvInvariant
-- Init.SimpLemmas
Bool.or_self : ∀ (b : Bool), (b || b) = b
-- Mathlib.Data.Finset.Fold
/-- `fold op b f s` folds the commutative associative operation `op` over the
`f`-image of `s`, i.e. `fold (+) b f {1,2,3} = f 1 + f 2 + f 3 + b`.  -/
Finset.fold : {α : Type u_1} →
  {β : Type u_2} → (op : β → β → β) → [hc : Std.Commutative op] → [ha : Std.Associative op] → β → (α → β) → Finset α → β
-- Mathlib.CategoryTheory.Sites.EpiMono
/-- The class of locally injective morphisms of sheaves, see `Sheaf.IsLocallyInjective`.  -/
CategoryTheory.Sheaf.locallyInjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u') →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {FA : A → A → Type u_1} →
            {CA : A → Type w} →
              [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
                [CategoryTheory.ConcreteCategory A FA] → CategoryTheory.MorphismProperty (CategoryTheory.Sheaf J A)
-- Init.Data.Int.Order
Int.pred_toNat : ∀ (i : ℤ), (i - 1).toNat = i.toNat - 1
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.restrict.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] {V : Set X}
  (D D_1 : Function.locallyFinsuppWithin U Y), D = D_1 → ∀ (h : V ⊆ U), D.restrict h = D_1.restrict h
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_lt_beth : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.beth o₁ < Cardinal.beth o₂ ↔ o₁ < o₂
-- Mathlib.Data.Fin.SuccPred
Fin.succ_le_castSucc_iff : ∀ {n : ℕ} {a b : Fin n}, a.succ ≤ b.castSucc ↔ a < b
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Iio_mul_eq_prod_Iic : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrderBot α] (a : α), (∏ x < a, f x) * f a = ∏ x ≤ a, f x
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.hom_id : ∀ (X : CpltSepUniformSpace), CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X) = ⟨id, ⋯⟩
-- Init.Data.Nat.Basic
/-- Alias for `Nat.zero_lt_one`.  -/
Nat.one_pos : 0 < 1
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.ball_dynEntourage_mem_nhds : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} [inst : UniformSpace X],
  Continuous T → U ∈ uniformity X → ∀ (n : ℕ) (x : X), UniformSpace.ball x (Dynamics.dynEntourage T U n) ∈ nhds x
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldRev.eq_1 : ∀ (α_2 : (i : ℕ) → autoParam (i ≤ 0) Nat.dfoldRev._auto_1 → Type u)
  (f_2 : (i : ℕ) → (h : i < 0) → α_2 (i + 1) ⋯ → α_2 i ⋯) (init_2 : α_2 0 ⋯), Nat.dfoldRev 0 f_2 init_2 = init_2
-- Std.Http.Data.Method
/-- Rebind a resource to a new URI path.
Source: https://www.rfc-editor.org/rfc/rfc5842#section-6
 -/
Std.Http.Method.rebind : Std.Http.Method
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- **Alias** of `toZ_le_toZ`. -/
toZ_le_iff : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i j : ι}, toZ i0 i ≤ toZ i0 j ↔ i ≤ j
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_true_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a : α} {k : ℤ}, Int.blt' 0 k = true → (a < a + ↑k) = True
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.one_div_smul : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {r : X} {s t : ↥S}, (1 /ₒ t) • (r /ₒ s) = r /ₒ (s * t)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.centerToCentroidCenter_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (z : ↥(NonUnitalSubsemiring.center α)) (a : α),
  (CentroidHom.centerToCentroidCenter z) a = ↑z * a