mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonnegg_cases_left : ∀ {c d b : ℕ} {a : ℤ}, (∀ (x : ℕ), a = -↑x → Zsqrtd.SqLe x d b c) → Zsqrtd.Nonnegg c d a ↑b
-- Batteries.Util.ExtendedBinder
/-- A list of parenthesized binders  -/
Batteries.ExtendedBinder.extBinderCollection : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.Dilation
DilationClass.edist_eq' : ∀ {F : Type u_3} {α : outParam (Type u_4)} {β : outParam (Type u_5)} {inst : PseudoEMetricSpace α}
  {inst_1 : PseudoEMetricSpace β} {inst_2 : FunLike F α β} [self : DilationClass F α β] (f : F),
  ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y
-- Mathlib.Logic.Lemmas
iff_right_comm : ∀ {a b c : Prop}, ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
-- Mathlib.Topology.Category.TopCat.Opens
/-- An inducing map `f : X ⟶ Y` induces a Galois insertion between `Opens Y` and `Opens X`.  -/
Topology.IsInducing.opensGI : {X Y : TopCat} →
  {f : X ⟶ Y} →
    (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) →
      GaloisInsertion (TopologicalSpace.Opens.map f).obj hf.functorObj
-- Lean.Parser.Term
Lean.Parser.Term.nofun : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.closure_singleton_zero : ∀ {A : Type u_2} [inst : AddMonoid A], AddSubmonoid.closure {0} = ⊥
-- Init.Data.String.Subslice
String.Slice.Subslice.toStringToString_eq : ∀ {s : String.Slice}, toString = String.Slice.copy ∘ String.Slice.Subslice.toSlice
-- Mathlib.Tactic.Translate.Core
/-- Linter used by translate attributes that warns when a translation was not added
because of being invalid.  -/
Mathlib.Tactic.Translate.linter.translate.warnInvalid : Lean.Option Bool
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.instInhabited : {F : Type u_1} →
  [inst : Field F] → {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → Inhabited (IntermediateField F E)
-- Mathlib.Data.Multiset.MapFold
Multiset.foldl_induction : ∀ {α : Type u_1} (f : α → α → α) [inst : RightCommutative f] (x : α) (p : α → Prop) (s : Multiset α),
  (∀ (a b : α), p a → p b → p (f b a)) → p x → (∀ a ∈ s, p a) → p (Multiset.foldl f x s)
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x y : A},
  IsIntegral R x → IsIntegral R y → IsIntegral R (x * y)
-- Std.Data.DTreeMap.Internal.Operations
/-- Iterate over `l` and erase all of its elements from `t`.  -/
Std.DTreeMap.Internal.Impl.eraseManyEntries : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {ρ : Type w} →
        [ForIn Id ρ ((a : α) × β a)] →
          (t : Std.DTreeMap.Internal.Impl α β) → ρ → t.Balanced → t.IteratedEntryErasureFrom
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- Suppose `X` is a reduced `S`-scheme and `Y` is a separated `S`-scheme.
For any `S`-morphisms `f g : X ⟶ Y`, `f = g` if `ι ≫ f = ι ≫ g` for some dominant `ι`.
 -/
AlgebraicGeometry.ext_of_isDominant_of_isSeparated' : ∀ {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [inst : X.Over S] [inst_1 : Y.Over S]
  [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f g : X ⟶ Y}
  [AlgebraicGeometry.Scheme.Hom.IsOver f S] [AlgebraicGeometry.Scheme.Hom.IsOver g S] {W : AlgebraicGeometry.Scheme}
  (ι : W ⟶ X) [AlgebraicGeometry.IsDominant ι],
  CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g → f = g
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternating_comp_ιMulti : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  (ExteriorAlgebra.liftAlternating f).compAlternatingMap (ExteriorAlgebra.ιMulti R n) = f n
-- Mathlib.Topology.Order.Bornology
Bornology.IsBounded.bddAbove : ∀ {α : Type u_1} {s : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  Bornology.IsBounded s → BddAbove s
-- Mathlib.Algebra.Group.Defs
/-- Bundling a `Mul` and `One` structure together without any axioms about their
compatibility. See `MulOneClass` for the additional assumption that 1 is an identity.  -/
MulOne : Type u_2 → Type u_2
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- If `G` preserves the pushout of `(f,g)`, then the pushout comparison map for `G` at `(f,g)` is
an isomorphism.  -/
CategoryTheory.Limits.PreservesPushout.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {W X Y : C} →
            (f : W ⟶ X) →
              (g : W ⟶ Y) →
                [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] →
                  [inst_3 : CategoryTheory.Limits.HasPushout f g] →
                    [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] →
                      CategoryTheory.Limits.pushout (G.map f) (G.map g) ≅ G.obj (CategoryTheory.Limits.pushout f g)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Subtype.image_closedEBall`. -/
Subtype.image_emetricClosedBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ENNReal),
  Subtype.val '' Metric.closedEBall a r = Metric.closedEBall (↑a) r ∩ {a | p a}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_coe_pi : (↑Real.pi).tan = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.equivMapOfInjective_coe_mulEquiv : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) (e : M ≃* N),
  S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S
-- Lean.MetavarContext
Lean.LocalInstance.mk.injEq : ∀ (className : Lean.Name) (fvar : Lean.Expr) (className_1 : Lean.Name) (fvar_1 : Lean.Expr),
  ({ className := className, fvar := fvar } = { className := className_1, fvar := fvar_1 }) =
    (className = className_1 ∧ fvar = fvar_1)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instCanonicallyOrderedAdd : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  CanonicallyOrderedAdd (LieSubalgebra R L)
-- Mathlib.RingTheory.Algebraic.Integral
rank_polynomial_polynomial : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R],
  Module.rank (Polynomial R) (Polynomial S) = Module.rank R S
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedState.default : Lean.Meta.Sym.Arith.State
-- Std.Http.Data.Body.Basic
/-- Closes the body stream.
 -/
Std.Http.Body.close : {α : Type} → [self : Std.Http.Body α] → α → Std.Async.Async Unit
-- Mathlib.Algebra.GCDMonoid.Basic
_private.Mathlib.Algebra.GCDMonoid.Basic.0.map_mk_unit_aux : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {f : Associates α →* α} (hinv : Function.RightInverse (⇑f) Associates.mk)
  (a : α), a * ↑(Classical.choose ⋯) = f (Associates.mk a)
-- Mathlib.Logic.Small.Defs
Shrink.rec_equivShrink : ∀ {α : Type u_1} [inst : Small.{w, u_1} α] {F : Shrink.{w, u_1} α → Sort v} {f : (a : α) → F ((equivShrink α) a)}
  (a : α), Shrink.rec f ((equivShrink α) a) = f a
-- Batteries.Tactic.Lint.Frontend
/-- Get the list of all declarations in the specified package.  -/
Batteries.Tactic.Lint.getDeclsInPackage : Lean.Name → Lean.CoreM (Array Lean.Name)
-- Mathlib.AlgebraicGeometry.Spec
/-- The induced map of a ring homomorphism on the prime spectra, as a morphism of locally ringed spaces.
 -/
AlgebraicGeometry.Spec.locallyRingedSpaceMap : {R S : CommRingCat} →
  (R ⟶ S) → (AlgebraicGeometry.Spec.locallyRingedSpaceObj S ⟶ AlgebraicGeometry.Spec.locallyRingedSpaceObj R)
-- Mathlib.Topology.Algebra.Order.Group
Filter.Tendsto.abs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G] {α : Type u_2} {l : Filter α} {f : α → G} {a : G},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => |f x|) l (nhds |a|)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_inv_eq_iff_eq_mul_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) [Invertible A] (B C : Matrix m n α), B * A⁻¹ = C ↔ B = C * A
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Derives.eq_or_tail : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)},
  g.Derives u w → w = u ∨ ∃ v, g.Derives u v ∧ g.Produces v w
-- Mathlib.NumberTheory.WellApproximable
_private.Mathlib.NumberTheory.WellApproximable.0.AddCircle.«term_∣∣_» : Lean.TrailingParserDescr
-- Mathlib.Data.Nat.Factorization.PrimePow
isPrimePow_iff_factorization_eq_single : ∀ {n : ℕ}, IsPrimePow n ↔ ∃ p k, 0 < k ∧ n.factorization = fun₀ | p => k
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.van_kampen : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Adhesive C] {W X Y Z : C} {f : W ⟶ X}
  {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Mono f] (H : CategoryTheory.IsPushout f g h i), H.IsVanKampen
-- Mathlib.Order.SetDissipate
Set.directed_dissipate : ∀ {α : Type u_1} {s : ℕ → Set α}, Directed (fun x1 x2 => x1 ⊇ x2) (Set.dissipate s)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.nilpotencyClass_le_of_upperCentralSeries_eq`. -/
nilpotencyClass_le_of_upperCentralSeries_eq : ∀ {G : Type u_1} [inst : Group G] {a b : ℕ},
  a < b → Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b → Group.nilpotencyClass G ≤ a
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.measurableSet_isProbabilityMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω], MeasurableSet {μ | MeasureTheory.IsProbabilityMeasure μ}
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_coeff : ∀ {h : ℝ} (f : UpperHalfPlane → ℂ) (m : ℕ),
  (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h f) =
    (↑m.factorial)⁻¹ * iteratedDeriv m (UpperHalfPlane.cuspFunction h f) 0
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.instIsQuasicoherentOfIsFinitePresentation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R)
  [M.IsFinitePresentation], M.IsQuasicoherent
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic.0.ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub.match_1_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (x : ℕ) → motive x),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | x => h_3 x) =
    h_2 ()
-- Mathlib.Order.SuccPred.Basic
/-- A constructor for `SuccOrder α` usable when `α` has no maximal element.  -/
SuccOrder.ofSuccLeIff : {α : Type u_1} → [inst : Preorder α] → (succ : α → α) → (∀ {a b : α}, succ a ≤ b ↔ a < b) → SuccOrder α
-- Mathlib.InformationTheory.Hamming
Hamming.ofHamming_sub : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Sub (β i)] {x y : Hamming β},
  Hamming.ofHamming (x - y) = Hamming.ofHamming x - Hamming.ofHamming y
-- Mathlib.Tactic.DuplicateDecls
Mathlib.Tactic.DuplicateDecls.Target.noConfusionType : Sort v✝ → Mathlib.Tactic.DuplicateDecls.Target → Mathlib.Tactic.DuplicateDecls.Target → Sort v✝
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.BoundaryGE.false_of_isTruncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι},
  e.BoundaryGE j → ∀ [e.IsTruncLE], False
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of
`R`-linearly independent elements of `A`, they are also `B`-linearly independent
in the opposite ring.  -/
Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥B] {ι : Type u_1} {a : ι → ↥A},
      LinearIndependent R a → LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- A linear map `f : M₂ → M` whose values lie in a submodule `p ⊆ M` can be restricted to a
linear map M₂ → p.

See also `LinearMap.codLift`.  -/
LinearMap.codRestrict : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      (p : Submodule R₂ M₂) → (f : M →ₛₗ[σ₁₂] M₂) → (∀ (c : M), f c ∈ p) → M →ₛₗ[σ₁₂] ↥p
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.comap.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G →* H) (K : FiniteIndexNormalSubgroup H),
  FiniteIndexNormalSubgroup.comap f K =
    { toSubgroup := Subgroup.comap f K.toSubgroup, isNormal' := ⋯, isFiniteIndex' := ⋯ }
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
      (CategoryTheory.ChosenPullbacksAlong.snd (CategoryTheory.CategoryStruct.id X) Y.hom) =
    CategoryTheory.CategoryStruct.id Y.left
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
/-- `IsLocalIso` is weaker than every source-Zariski-local property containing identities.  -/
AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.ContainsIdentities]
  [AlgebraicGeometry.IsZariskiLocalAtSource P], @AlgebraicGeometry.IsLocalIso ≤ P
-- Mathlib.Topology.Homotopy.Lifting
/-- The fundamental group of the base of simply-connected covering map is contravariantly
equivalent to the group of the covering map.  -/
IsAddQuotientCoveringMap.fundamentalGroupEquiv : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} →
          {G : Type u_4} →
            [inst_2 : AddGroup G] →
              [inst_3 : AddAction G E] →
                IsAddQuotientCoveringMap p G →
                  {x : X} → ↑(p ⁻¹' {x}) → [SimplyConnectedSpace E] → FundamentalGroup X x ≃* (Multiplicative G)ᵐᵒᵖ
-- Init.Data.Int.Lemmas
Int.eq_one_of_mul_eq_self_right : ∀ {a b : ℤ}, b ≠ 0 → b * a = b → a = 1
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.id_preimage : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (f : (CategoryTheory.Functor.id C).obj X ⟶ (CategoryTheory.Functor.id C).obj Y),
  (CategoryTheory.Functor.FullyFaithful.id C).preimage f = f
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Iio₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a : G₀),
  0 < c → (fun x => x * c) ⁻¹' Set.Iio a = Set.Iio (a / c)
-- Mathlib.Algebra.Algebra.Subalgebra.Order
Subalgebra.toIsOrderedRing : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : PartialOrder A]
  [IsOrderedRing A] [inst_4 : Algebra R A] (S : Subalgebra R A), IsOrderedRing ↥S
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.C1_projOrd : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2) {x : I → Bool},
      x ∈ Profinite.NobelingProof.C1 C ho →
        Profinite.NobelingProof.SwapTrue o
            (Profinite.NobelingProof.Proj (fun x => Profinite.NobelingProof.ord I x < o) x) =
          x
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_ofNat : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo],
  (OfNat.ofNat n).re = OfNat.ofNat n
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_σ_succ' : ∀ {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.succ →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.σ i) =
      CategoryTheory.CategoryStruct.id { len := n }
-- Mathlib.Data.ZMod.Basic
ZMod.val_injective : ∀ (n : ℕ) [NeZero n], Function.Injective ZMod.val
-- Mathlib.RingTheory.Ideal.Maps
Ideal.IsRadical.comap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F) {K : Ideal S}, K.IsRadical → (Ideal.comap f K).IsRadical
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {X Y :
    CategoryTheory.InducedCategory (AlgebraicGeometry.PresheafedSpace C)
      AlgebraicGeometry.SheafedSpace.toPresheafedSpace}
  (f : X ⟶ Y), AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.map f = f.hom
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsFiltered J],
      CategoryTheory.Limits.ReflectsColimitsOfShape J F) →
    CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two : ∀ {θ ψ : Real.Angle}, |θ.toReal| < Real.pi / 2 → |ψ.toReal| < Real.pi / 2 → (2 • θ = 2 • ψ ↔ θ = ψ)
-- Batteries.Control.AlternativeMonad
StateT.instLawfulAlternativeOfLawfulMonad : ∀ {σ : Type u_1} (m : Type u_1 → Type u_2) [inst : AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m],
  LawfulAlternative (StateT σ m)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.algebraMap_gradedMul : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (r : R)
  (x : TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)),
  ((TensorProduct.gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) x = r • x
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.filter_apply_eq_zero_of_notMem : ∀ {α : Type u_1} {p : PMF α} {s : Set α} (h : ∃ a ∈ s, a ∈ p.support) {a : α}, a ∉ s → (p.filter s h) a = 0
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.prop_map_obj : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) {X : C}, P X → P.map F (F.obj X)
-- Aesop.Frontend.Tactic
/-- `aesop <clause>*` tries to solve the current goal by applying a set of rules
registered with the `@[aesop]` attribute. See [its
README](https://github.com/JLimperg/aesop#readme) for a tutorial and a
reference.

The variant `aesop?` prints the proof it found as a `Try this` suggestion.

Clauses can be used to customise the behaviour of an Aesop call. Available
clauses are:

- `(add <phase> <priority> <builder> <rule>)` adds a rule. `<phase>` is
  `unsafe`, `safe` or `norm`. `<priority>` is a percentage for unsafe rules and
  an integer for safe and norm rules. `<rule>` is the name of a declaration or
  local hypothesis. `<builder>` is the rule builder used to turn `<rule>` into
  an Aesop rule. Example: `(add unsafe 50% apply Or.inl)`.
- `(erase <rule>)` disables a globally registered Aesop rule. Example: `(erase
  Aesop.BuiltinRules.assumption)`.
- `(rule_sets := [<ruleset>,*])` enables or disables named sets of rules for
  this Aesop call. Example: `(rule_sets := [-builtin, MyRuleSet])`.
- `(config { <opt> := <value> })` adjusts Aesop's search options. See
  `Aesop.Options`.
- `(simp_config { <opt> := <value> })` adjusts options for Aesop's built-in
  `simp` rule. The given options are directly passed to `simp`. For example,
  `(simp_config := { zeta := false })` makes Aesop use
  `simp (config := { zeta := false })`.
 -/
Aesop.Frontend.Parser.aesopTactic : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : CancelMonoid α],
  Lex.instCancelMonoid = { toLeftCancelMonoid := Lex.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }
-- Lean.Expr
Lean.reflBoolTrue : Lean.Expr
-- Mathlib.Algebra.Order.Hom.Monoid
/-- See Note [custom simps projection].  -/
OrderAddMonoidIso.Simps.symm_apply : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Add α] → [inst_3 : Add β] → (α ≃+o β) → β → α
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Function `f` has Max-Cut property at some two non-identical labels.  -/
Function.HasMaxCutProperty : {D : Type u_1} → {C : Type u_2} → [PartialOrder C] → ((Fin 2 → D) → C) → Prop
-- Init.Data.SInt.Lemmas
Int64.toInt16_ofIntLE : ∀ {n : ℤ} (h₁ : Int64.minValue.toInt ≤ n) (h₂ : n ≤ Int64.maxValue.toInt),
  (Int64.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n
-- Aesop.Index.Basic
Aesop.IndexingMode.brecOn.eq : ∀ {motive_1 : Aesop.IndexingMode → Sort u} {motive_2 : Array Aesop.IndexingMode → Sort u}
  {motive_3 : List Aesop.IndexingMode → Sort u} (t : Aesop.IndexingMode)
  (F_1 : (t : Aesop.IndexingMode) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.IndexingMode) → Aesop.IndexingMode.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.IndexingMode) → Aesop.IndexingMode.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Aesop.IndexingMode.brecOn.go t F_1 F_2 F_3).2
-- Std.Http.Data.Status
/-- 501 Not Implemented
 -/
Std.Http.Status.notImplemented : Std.Http.Status
-- Mathlib.Data.ENNReal.Operations
ENNReal.toReal_iInf : ∀ {ι : Sort u_1} {f : ι → ENNReal}, (∀ (i : ι), f i ≠ ⊤) → (iInf f).toReal = ⨅ i, (f i).toReal
-- Mathlib.Algebra.Group.TypeTags.Pointwise
Multiplicative.toAdd_image_setMul : ∀ {M : Type u_1} [inst : AddMonoid M] (s t : Set (Multiplicative M)),
  ⇑Multiplicative.toAdd '' (s * t) = ⇑Multiplicative.toAdd '' s + ⇑Multiplicative.toAdd '' t
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_neg : ∀ {ι : Type u_2} {G : Type u_4} [inst : SubtractionCommMonoid G] {m : Multiset ι} {f : ι → G},
  (Multiset.map (fun i => -f i) m).sum = -(Multiset.map f m).sum