mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Context.mk.inj : ∀ {quotContext : Lean.Name} {preserveOrder : Bool} {binderInfoForMVars : Lean.BinderInfo}
  {mvarIdsToAbstract : Lean.MVarIdSet} {quotContext_1 : Lean.Name} {preserveOrder_1 : Bool}
  {binderInfoForMVars_1 : Lean.BinderInfo} {mvarIdsToAbstract_1 : Lean.MVarIdSet},
  { quotContext := quotContext, preserveOrder := preserveOrder, binderInfoForMVars := binderInfoForMVars,
        mvarIdsToAbstract := mvarIdsToAbstract } =
      { quotContext := quotContext_1, preserveOrder := preserveOrder_1, binderInfoForMVars := binderInfoForMVars_1,
        mvarIdsToAbstract := mvarIdsToAbstract_1 } →
    quotContext = quotContext_1 ∧
      preserveOrder = preserveOrder_1 ∧
        binderInfoForMVars = binderInfoForMVars_1 ∧ mvarIdsToAbstract = mvarIdsToAbstract_1
-- Mathlib.Data.Nat.Init
Nat.AtLeastTwo.mk : ∀ {n : ℕ}, 2 ≤ n → n.AtLeastTwo
-- Mathlib.Probability.Kernel.MeasurableLIntegral
Measurable.lintegral_kernel_prod_right'' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {η : ProbabilityTheory.Kernel (α × β) γ} {a : α} [ProbabilityTheory.IsSFiniteKernel η]
  {f : β × γ → ENNReal}, Measurable f → Measurable fun x => ∫⁻ (y : γ), f (x, y) ∂η (a, x)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.eq_of_toNormPoly_eq : ∀ (ctx : Nat.Internal.Linear.Context) (e e' : Nat.Internal.Linear.Expr),
  (e.toNormPoly == e'.toPoly) = true → Nat.Internal.Linear.Expr.denote ctx e = Nat.Internal.Linear.Expr.denote ctx e'
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.map_map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y))
  {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1), (FundamentalGroupoid.map f).map p = Path.Homotopic.Quotient.map p f
-- Init.Data.Function
Function.rightInverse_of_injective_of_leftInverse : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α},
  Function.Injective f → Function.LeftInverse f g → Function.RightInverse f g
-- Mathlib.Topology.Algebra.AffineSubspace
/-- Embedding of an affine subspace to the ambient space, as a continuous affine map.  -/
AffineSubspace.subtypeA : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module R V] →
            [inst_3 : TopologicalSpace P] →
              [inst_4 : AddTorsor V P] → (s : AffineSubspace R P) → [inst_5 : Nonempty ↥s] → ↥s →ᴬ[R] P
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity.eq_1 : ∀ (A : Set ℕ) [inst : DecidablePred fun x => x ∈ A],
  schnirelmannDensity A = ⨅ n, ↑{a ∈ Finset.Ioc 0 ↑n | a ∈ A}.card / ↑↑n
-- Mathlib.Tactic.DeriveTraversable
/-- derive the `map` definition of a `Functor`  -/
Mathlib.Deriving.Traversable.mkMap : Lean.Name → Lean.MVarId → Lean.Elab.TermElabM Unit
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.below.injEq : ∀ (decl : Lean.LocalDecl) (indName : Lean.Name) (vars : Array Lean.FVarId) (decl_1 : Lean.LocalDecl)
  (indName_1 : Lean.Name) (vars_1 : Array Lean.FVarId),
  (Lean.Meta.IndPredBelow.NewDecl.below✝ decl indName vars =
      Lean.Meta.IndPredBelow.NewDecl.below✝ decl_1 indName_1 vars_1) =
    (decl = decl_1 ∧ indName = indName_1 ∧ vars = vars_1)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDelabTermInfo.injEq : ∀ (i i_1 : Lean.Elab.DelabTermInfo), (Lean.Elab.Info.ofDelabTermInfo i = Lean.Elab.Info.ofDelabTermInfo i_1) = (i = i_1)
-- Init.Data.Order.PackageFactories
/-- This class entails `LE α`, `LT α`, `BEq α` and `Ord α` instances as well as proofs that these
operations represent the same linear preorder structure on `α`.
 -/
Std.LinearPreorderPackage : Type u → Type u
-- Mathlib.Dynamics.Ergodic.Conservative
/-- Iteration of a conservative system is a conservative system.  -/
MeasureTheory.Conservative.iterate : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ → ∀ (n : ℕ), MeasureTheory.Conservative f^[n] μ
-- Std.Http.Data.Version
Std.Http.instReprVersion.repr : Std.Http.Version → ℕ → Std.Format
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.fold_eq_forIn : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Std.Iter β},
  Std.Iter.fold f init it = (forIn it init fun x acc => pure (ForInStep.yield (f acc x))).run
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearMap.integral_compLp : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  {𝕜' : Type u_7} [inst_1 : RCLike 𝕜] [inst_2 : RCLike 𝕜'] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜' F] {p : ENNReal} [inst_7 : NormedSpace ℝ F] {σ : 𝕜 →+* 𝕜'}
  [inst_8 : RingHomIsometric σ] (L : E →SL[σ] F) (φ : ↥(MeasureTheory.Lp E p μ)),
  ∫ (x : X), ↑↑(L.compLp φ) x ∂μ = ∫ (x : X), L (↑↑φ x) ∂μ
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.freeYonedaHomEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {X : C} {M : A} {F : CategoryTheory.Functor Cᵒᵖ A},
  CategoryTheory.Presheaf.freeYonedaHomEquiv =
    {
      toFun := fun f =>
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Sigma.ι (fun i => M)
            (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X))))
          (f.app (Opposite.op X)),
      invFun := fun g =>
        {
          app := fun Y =>
            CategoryTheory.Limits.Sigma.desc fun φ => CategoryTheory.CategoryStruct.comp g (F.map (Quiver.Hom.op φ)),
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Option.Monadic
Option.throw_eq_none : ∀ {α : Type u_1}, throw () = none
-- Mathlib.Data.Finset.Image
Finset.mem_map_of_mem : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : Finset α}, a ∈ s → f a ∈ Finset.map f s
-- Mathlib.MeasureTheory.Constructions.Pi
/-- `Measure.pi μ` has finite spanning sets in rectangles of finite spanning sets.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.pi : {ι : Type u_1} →
  {α : ι → Type u_3} →
    [inst : Fintype ι] →
      [inst_1 : (i : ι) → MeasurableSpace (α i)] →
        {μ : (i : ι) → MeasureTheory.Measure (α i)} →
          {C : (i : ι) → Set (Set (α i))} →
            ((i : ι) → (μ i).FiniteSpanningSetsIn (C i)) →
              (MeasureTheory.Measure.pi μ).FiniteSpanningSetsIn (Set.univ.pi '' Set.univ.pi C)
-- Mathlib.Data.ZMod.Basic
ZMod.inv_mul_of_unit : ∀ {n : ℕ} (a : ZMod n), IsUnit a → a⁻¹ * a = 1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_right_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ)
  (X_1 : SimplexCategory), X.leftOpRightOpIso.inv.right.app X_1 = CategoryTheory.CategoryStruct.id (X.right.obj X_1)
-- Mathlib.Order.Atoms
CompleteAtomicBooleanAlgebra.instIsCoatomistic : ∀ {α : Type u_4} [inst : CompleteAtomicBooleanAlgebra α], IsCoatomistic α
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The `S`-rank of `M ⊗[R] M'` is `(Module.rank S M).lift * (Module.rank R M').lift`.  -/
rank_tensorProduct : ∀ {R : Type u} {S : Type u'} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M] [StrongRankCondition R]
  [StrongRankCondition S] [inst_7 : Module S M] [inst_8 : Module S M'] [Module.Free S M'] [inst_10 : Algebra S R]
  [inst_11 : IsScalarTower S R M] [Module.Free R M],
  Module.rank R (TensorProduct S M M') =
    Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
-- Mathlib.Algebra.Module.TransferInstance
AddEquiv.linearEquiv_apply : ∀ {α : Type u_2} {β : Type u_3} (A : Type u_4) [inst : Semiring A] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β]
  [inst_3 : Module A β] (e : α ≃+ β) (a : α), (AddEquiv.linearEquiv A e) a = e.toFun a
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.noConfusionType : Sort v✝ → Turing.PartrecToTM2.K' → Turing.PartrecToTM2.K' → Sort v✝
-- Lean.Util.CollectFVars
Lean.CollectFVars.instInhabitedState : Inhabited Lean.CollectFVars.State
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instBEqRingMode : BEq Mathlib.Tactic.RingNF.RingMode
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.below.mul_left : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} {motive : (a a_1 : R) → RingQuot.Rel r a a_1 → Prop} ⦃a b c : R⦄
  (a_1 : RingQuot.Rel r a b), RingQuot.Rel.below a_1 → motive a b a_1 → RingQuot.Rel.below ⋯
-- Mathlib.RingTheory.Perfection
/-- `Perfection M p` as a submonoid of `ℕ → M`.  -/
Perfection.submonoid : (M : Type u_1) → [inst : CommMonoid M] → ℕ → Submonoid (ℕ → M)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_himp : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s t : Subtype MeasurableSet), ↑(s ⇨ t) = ↑s ⇨ ↑t
-- Lean.Parser.Term
Lean.Parser.Term.let.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Localization.Defs
/-- A `CommRing` `S` which is the localization of an integral domain `R` at a subset of
non-zero elements is an integral domain.  -/
IsLocalization.isDomain_of_le_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] [IsDomain R], M ≤ nonZeroDivisors R → IsDomain S
-- Mathlib.CategoryTheory.Limits.Cones
/-- Precomposing by the identity does not change the cocone up to isomorphism.  -/
CategoryTheory.Limits.Cocone.precomposeId : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          CategoryTheory.Limits.Cocone.precompose (CategoryTheory.CategoryStruct.id F) ≅
            CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)
-- Mathlib.CategoryTheory.Square
/-- The bottom-left evaluation `Square C ⥤ C`.  -/
CategoryTheory.Square.evaluation₃ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Square C) C
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeWhileTR.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.takeWhileTR p l = List.takeWhileTR.go✝ p l l #[]
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) (n m : ℤ)
  (hnm : autoParam (n + 1 = m) CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero._auto_1),
  CategoryTheory.CategoryStruct.comp (i.f n) ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) = 0
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_union_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a < b → Set.Ioo a b ∪ {a} = Set.Ico a b
-- Mathlib.Data.Int.Order.Basic
/-- **Alias** of the forward direction of `Int.ofNat_le`. -/
Int.le_of_ofNat_le_ofNat : ∀ {m n : ℕ}, ↑m ≤ ↑n → m ≤ n
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- A morphism between two adjunctions consists of a tuple of mate maps.  -/
CategoryTheory.Bicategory.Adj.Hom₂ : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {a b : CategoryTheory.Bicategory.Adj B} → (a ⟶ b) → (a ⟶ b) → Type w
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_eq_getKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α}
  {h : a ∈ t}, t.getKey a h = t.getKeyD a fallback
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.cosh_dist : ∀ (z w : UpperHalfPlane), Real.cosh (dist z w) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)
-- Mathlib.Order.MinMax
lt_max_of_lt_left : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < b → a < max b c
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
stronglyMeasurable_of_restrict_of_restrict_compl : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β} {s : Set α},
  MeasurableSet s →
    MeasureTheory.StronglyMeasurable (s.domRestrict f) →
      MeasureTheory.StronglyMeasurable (sᶜ.domRestrict f) → MeasureTheory.StronglyMeasurable f
-- Mathlib.Order.Filter.Basic
Filter.sup_neBot : ∀ {α : Type u} {f g : Filter α}, (f ⊔ g).NeBot ↔ f.NeBot ∨ g.NeBot
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalAddGroup.exists_addNegClosureNhd : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] [CompactSpace G]
  {W : Set G}, IsClopen W → ∃ T, IsTopologicalAddGroup.addNegClosureNhd T W
-- Init.Data.Array.Attach
Array.unattach_empty : ∀ {α : Type u_1} {p : α → Prop}, #[].unattach = #[]
-- Mathlib.RepresentationTheory.Basic
/-- Given representations of `G` on `V` and `W`, there is a natural representation of `G` on their
product `V × W`.
 -/
Representation.prod : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring k] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : Module k V] →
                [inst_4 : AddCommMonoid W] →
                  [inst_5 : Module k W] → Representation k G V → Representation k G W → Representation k G (V × W)
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.simplified.sizeOf_spec : ∀ (newGoal : Lean.MVarId) (usedTheorems : Lean.Meta.Simp.UsedSimps),
  sizeOf (Aesop.SimpResult.simplified newGoal usedTheorems) = 1 + sizeOf newGoal + sizeOf usedTheorems
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.even_sub_one : ∀ {p : ℕ}, Nat.Prime p → p ≠ 2 → Even (p - 1)
-- Init.System.Platform
System.Platform.numBits_pos : 0 < System.Platform.numBits
-- Std.Data.HashSet.Lemmas
Std.HashSet.any_eq_false_iff_forall_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {p : α → Bool},
  m.any p = false ↔ ∀ a ∈ m, p a = false
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
aemeasurable_of_unif_approx : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_3} [inst_1 : MeasurableSpace β] [inst_2 : PseudoMetricSpace β]
  [BorelSpace β] {μ : MeasureTheory.Measure α} {g : α → β},
  (∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε) → AEMeasurable g μ
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromyFunctor_map : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {X_1 Y : FundamentalGroupoid X} (f : X_1 ⟶ Y),
  cov.monodromyFunctor.map f = TypeCat.ofHom (cov.monodromy f)
-- Init.Data.Order.FactoriesExtra
/-- The `LE α` instance obtained from an `Ord α` instance is compatible with said `Ord α`
instance if `compare` is oriented, i.e., `compare a b = .lt ↔ compare b a = .gt`.
 -/
Std.instLawfulOrderOrd_ofOrd : ∀ (α : Type u) [inst : Ord α] [Std.OrientedOrd α], Std.LawfulOrderOrd α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- **Alias** of the forward direction of `nsmul_le_nsmul_iff_right`. -/
le_of_nsmul_le_nsmul_right : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b : M}
  {n : ℕ}, n ≠ 0 → n • a ≤ n • b → a ≤ b
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A product over an index type with exactly one term is just the object over that term.  -/
CategoryTheory.Limits.productUniqueIso : {β : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : Unique β] → (f : β → C) → ∏ᶜ f ≅ f default
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_neg : ∀ {R : Type u} {A : Type z} [inst : CommRing R] {p : Polynomial R} [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A),
  (Polynomial.aeval x) (-p) = -(Polynomial.aeval x) p
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α),
  Disjoint (MeasureTheory.fundamentalInterior G s) (MeasureTheory.fundamentalFrontier G s)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_comp_descCochain : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n),
  (CochainComplex.mappingCocone.inl φ).comp (CochainComplex.mappingCocone.descCochain φ α β h) ⋯ = α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_cons_iff : ∀ {xs : List ℕ} {m n a : ℕ}, (m...n).toList = a :: xs ↔ m = a ∧ m < n ∧ ((m + 1)...n).toList = xs
-- Mathlib.Algebra.CharP.Basic
CharP.ringChar_of_prime_eq_zero : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [Nontrivial R] {p : ℕ}, Nat.Prime p → ↑p = 0 → ringChar R = p
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- `M →ₚₗ[R] N` is the type of `R`-polynomial laws from `M` to `N`.  -/
«term_→ₚₗ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteFar_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : Fintype ↑G.edgeSet] {p : SimpleGraph V → Prop} {r : 𝕜} [inst_3 : Fintype (Sym2 V)],
  G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
-- Mathlib.Algebra.Polynomial.Div
Polynomial.coeff_divByMonic_X_sub_C_rec : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (a : R) (n : ℕ),
  (p /ₘ (Polynomial.X - Polynomial.C a)).coeff n =
    p.coeff (n + 1) + a * (p /ₘ (Polynomial.X - Polynomial.C a)).coeff (n + 1)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_div : ∀ {a b c : Ordinal.{u_4}}, c ≠ 0 → (a < b / c ↔ c * Order.succ a ≤ b)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.tmul_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M), m ⊗ₜ[R] 0 = 0
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonLocation.toJson : Lean.Lsp.Location → Lean.Json
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_right_injective₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀]
  [ZeroLEOneClass G₀], 0 < a → a ≠ 1 → Function.Injective fun n => a ^ n
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.isCollinear_subset : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (s t : Set (Projectivization K V)), s ⊆ t → Projectivization.IsCollinear t → Projectivization.IsCollinear s
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- `AlternatingMap.domDomCongr` as a linear equivalence.  -/
AlternatingMap.domDomCongrₗ : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  {ι' : Type u_8} →
                    (S : Type u_12) →
                      [inst_5 : Semiring S] →
                        [inst_6 : Module S N] →
                          [inst_7 : SMulCommClass R S N] → ι ≃ ι' → M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι']→ₗ[R] N
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
/-- Preliminary lemma for compactness of the orbit map.  -/
_private.Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction.0.UpperHalfPlane.cdsq_le : ∀ {K : Set UpperHalfPlane},
  IsCompact K → ∃ A, ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℝ), g • UpperHalfPlane.I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio : Type
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
/-- The **Ahlswede-Zhang Identity**.  -/
AhlswedeZhang.infSum_compls_add_supSum : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] [Nonempty α] (𝒜 : Finset (Finset α)),
  AhlswedeZhang.infSum 𝒜.compls + AhlswedeZhang.supSum 𝒜 =
    ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹ + 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_add_of_sign_pos_sign_neg : ∀ {θ ψ : Real.Angle}, θ.sign = 1 → ψ.sign = -1 → (θ + ψ).toReal = θ.toReal + ψ.toReal
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- A valued division ring is separated.  -/
ValuedRing.separated : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : Valued K Γ₀], T0Space K
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.neg_add_cancel : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Lean.Meta.HaveTelescope
Lean.Meta.HaveTelescopeInfo.mk : Array Lean.Meta.HaveInfo →
  Std.HashSet ℕ → Std.HashSet ℕ → Lean.Expr → Lean.Expr → Lean.Level → Lean.Meta.HaveTelescopeInfo
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqvAux_of_rel : ∀ {α : Type u_1} {r : α → α → Bool} {xs ys : Array α} (hsz : xs.size = ys.size) {i : ℕ} (hi : i ≤ xs.size),
  (∀ (j : ℕ) (hj : j < i), r xs[j] ys[j] = true) → xs.isEqvAux ys hsz r i hi = true
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.toSubspaceUnit_isMono : ∀ {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Combinatorics.Line α ι} {C : (ι → α) → κ},
  Combinatorics.Subspace.IsMono C l.toSubspaceUnit ↔ Combinatorics.Line.IsMono C l
-- Mathlib.Algebra.Order.GroupWithZero.Lex
MonoidWithZeroHom.fst_mono : ∀ {M₀ : Type u_1} {N₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero M₀] [inst_1 : GroupWithZero N₀]
  [inst_2 : Preorder N₀], Monotone ⇑(MonoidWithZeroHom.fst M₀ N₀)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rii α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Rii α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.differentiableAt_cuspFunction : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          ∀ {q : ℂ}, ‖q‖ < 1 → DifferentiableAt ℂ (UpperHalfPlane.cuspFunction h f) q
-- Init.Data.Nat.Div.Basic
Nat.div_self : ∀ {n : ℕ}, 0 < n → n / n = 1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_of_comp : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (j : N →+ P), f.lift ⋯ = j
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero₂_of_isThirdQuadrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Y : CategoryTheory.Abelian.SpectralObject C EInt) [Y.IsThirdQuadrant] (i j : EInt) (hij : i ≤ j) (n : ℤ),
  j ≤ WithBotTop.coe n →
    CategoryTheory.Limits.IsZero ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))
-- Mathlib.Data.List.Basic
List.ext_getElem?_iff' : ∀ {α : Type u} {l₁ l₂ : List α}, l₁ = l₂ ↔ ∀ n < max l₁.length l₂.length, l₁[n]? = l₂[n]?
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instIsAlwaysFiniteNat : Std.Rxc.IsAlwaysFinite ℕ