mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Diagonal
Matrix.one_apply_ne' : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] {i j : n}, j ≠ i → 1 i j = 0
-- Mathlib.Order.Directed
DirectedOn.mono_comp : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {rb : β → β → Prop} {g : α → β} {s : Set α},
  (∀ ⦃x y : α⦄, r x y → rb (g x) (g y)) → DirectedOn r s → DirectedOn rb (g '' s)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loops.eq_1 : ∀ {α : Type u_1} (M : Matroid α), M.loops = M.closure ∅
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- Elementwise intersection of two `AECover`s is an `AECover`.  -/
MeasureTheory.AECover.inter : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  {φ ψ : ι → Set α},
  MeasureTheory.AECover μ l φ → MeasureTheory.AECover μ l ψ → MeasureTheory.AECover μ l fun i => φ i ∩ ψ i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t.isEmpty = true → ∀ {fallback : α}, (t.insertIfNew k v).minKeyD fallback = k
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {F : CategoryTheory.Functor C D} {x y : F.OplaxMonoidal},
  x = y ↔
    CategoryTheory.Functor.OplaxMonoidal.η F = CategoryTheory.Functor.OplaxMonoidal.η F ∧
      CategoryTheory.Functor.OplaxMonoidal.δ F = CategoryTheory.Functor.OplaxMonoidal.δ F
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.instIsPretransitiveElemOrbit_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (x : MulAction.orbitRel.Quotient G α),
  MulAction.IsPretransitive G ↑x.orbit
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSpace.instSubsingleton : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [h : Subsingleton α],
  Subsingleton (MeasureTheory.NullMeasurableSpace α μ)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_sub : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (f g : CentroidHom α), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Data.Nat.Totient
Nat.Ico_filter_coprime_le : ∀ {a : ℕ} (k n : ℕ), a ≠ 0 → {x ∈ Finset.Ico k (k + n) | a.Coprime x}.card ≤ a.totient * (n / a + 1)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.id_isExpansionOn : ∀ {L : FirstOrder.Language} (M : Type u_1) [inst : L.Structure M], (FirstOrder.Language.LHom.id L).IsExpansionOn M
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `F` is a left adjoint, then so is `post F : Under X ⥤ Under (F X)`.

If the right adjoint of `F` is `G`, then the right adjoint of `post F` is given by
`(F X ⟶ Y) ↦ (X ⟶ G F X ⟶ G Y)`.  -/
CategoryTheory.Under.postAdjunctionLeft : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          {F : CategoryTheory.Functor T D} →
            {G : CategoryTheory.Functor D T} →
              (a : F ⊣ G) →
                CategoryTheory.Under.post F ⊣
                  (CategoryTheory.Under.post G).comp (CategoryTheory.Under.map (a.unit.app X))
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.coe_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : Y ⟶ X), (CategoryTheory.Over.mk f).hom = f
-- Mathlib.FieldTheory.PrimitiveElement
Field.primitive_element_iff_algHom_eq_of_eval' : ∀ (F : Type u_3) {E : Type u_4} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  [Algebra.IsSeparable F E] (A : Type u_5) [inst_5 : Field A] [inst_6 : Algebra F A],
  (∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits) →
    ∀ (α : E), F⟮α⟯ = ⊤ ↔ Function.Injective fun φ => φ α
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.tprod_mul_tprod : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {na nb : ℕ}
  (a : Fin na → M) (b : Fin nb → M),
  GradedMonoid.GMul.mul ((PiTensorProduct.tprod R) a) ((PiTensorProduct.tprod R) b) =
    (PiTensorProduct.tprod R) (Fin.append a b)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableLtOffset : {x y : Std.Time.Nanosecond.Offset} → Decidable (x < y)
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.mono : ∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {t s : Set A},
  t ⊆ s → AlgebraicIndependent R Subtype.val → AlgebraicIndependent R Subtype.val
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.coe_le_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithZero α} {a : α}, ↑a ≤ x ↔ ∃ b, x = ↑b ∧ a ≤ b
-- Mathlib.AlgebraicGeometry.Stalk
/-- Given a local ring `(R, 𝔪)` and a morphism `f : Spec R ⟶ X`,
they induce a (local) ring homomorphism `φ : 𝒪_{X, f 𝔪} ⟶ R`.

This is inverse to `φ ↦ Spec.map φ ≫ X.fromSpecStalk (f 𝔪)`. See `SpecToEquivOfLocalRing`.
 -/
AlgebraicGeometry.Scheme.stalkClosedPointTo : {X : AlgebraicGeometry.Scheme} →
  {R : CommRingCat} →
    [inst : IsLocalRing ↑R] → (f : AlgebraicGeometry.Spec R ⟶ X) → X.presheaf.stalk (f (IsLocalRing.closedPoint ↑R)) ⟶ R
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_find : ∀ {α : Type u_1} {mα : MeasurableSpace α} {p : α → ℕ → Prop} [inst : (x : α) → DecidablePred (p x)]
  (hp : ∀ (x : α), ∃ N, p x N), (∀ (k : ℕ), MeasurableSet {x | p x k}) → Measurable fun x => Nat.find ⋯
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.inv : ∀ {α : Type u} {β : Type v} [inst : Inv β] {f g : α → β} {l : Filter α}, f =ᶠ[l] g → f⁻¹ =ᶠ[l] g⁻¹
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsCircuit.contract_sdiff_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {K C : Set α}, M.IsCircuit C → K.Nonempty → K ⊆ C → (M.contract (C \ K)).IsCircuit K
-- Mathlib.Order.Lattice
sup_ind : ∀ {α : Type u} [inst : LinearOrder α] (a b : α) {p : α → Prop}, p a → p b → p (max a b)
-- Mathlib.Data.Tree.Basic
BinaryTree.map.eq_1 : ∀ {α : Type u} {β : Type u_1} (f : α → β), BinaryTree.map f BinaryTree.nil = BinaryTree.nil
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.nontrivial_iff : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R], v.Integers O → (Nontrivial O ↔ Nontrivial R)
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.norm_def : ∀ {𝕜 : Type u_1} {V : Type u_3} {W : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W),
  ‖f‖ = max ‖f 0‖ ‖f.contLinear‖
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_lt_of_le_left : ∀ {α : Type u_2} {a b c : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α]
  [inst_2 : DecidablePred fun x => x < c], c ≤ a → {x ∈ Finset.Ico a b | x < c} = ∅
-- Lean.Meta.InferType
/-- `isArrowType type n` is an "approximate" predicate which returns `LBool.true` if `type` is of the
form `A_1 → ... → A_n → Sort _`.

Remark: `type` can be a dependent arrow.  -/
_private.Lean.Meta.InferType.0.Lean.Meta.isArrowType : Lean.Expr → ℕ → Lean.MetaM Lean.LBool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_diff!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff! m₂).get? k = m₁.get? k
-- Mathlib.Data.Rat.Defs
Rat.intCast_injective : Function.Injective Int.cast
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.iterate_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f' : Module.End R M}, Function.Injective ⇑f' → ∀ (n : ℕ), Function.Injective ⇑(f' ^ n)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The sum of `succSub` operators up to `n` equals `P n`.  -/
SchauderBasis.sum_succSub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (P : ℕ → X →L[𝕜] X),
  P 0 = 0 → ∀ (n : ℕ), ∑ i ∈ Finset.range n, SchauderBasis.succSub P i = P n
-- Lean.Compiler.InitAttr
_private.Lean.Compiler.InitAttr.0.Lean.runInitAttrForMod : Lean.Environment → Lean.Options → Lean.EffectiveImport → ℕ → IO Unit
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeValueResult.snap? : Lean.Meta.RealizeValueResult✝ → Option Lean.Language.SnapshotTree
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaMap_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {Y : C} {X : Cᵒᵖ} (f : Opposite.unop X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.uliftYonedaMap F Y).app X)) { down := f } = { down := F.map f }
-- Mathlib.Data.Nat.Bitwise
Nat.testBit_lor : ∀ (m n k : ℕ), (m ||| n).testBit k = (m.testBit k || n.testBit k)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  (homEquiv : {Y : C} → (X ⟶ Y) ≃ F.obj Y)
  (homEquiv_comp :
    autoParam
      (∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
        homEquiv (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map g)) (homEquiv f))
      CategoryTheory.Functor.CorepresentableBy.homEquiv_comp._autoParam)
  (homEquiv_1 : {Y : C} → (X ⟶ Y) ≃ F.obj Y)
  (homEquiv_comp_1 :
    autoParam
      (∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
        homEquiv_1 (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map g)) (homEquiv_1 f))
      CategoryTheory.Functor.CorepresentableBy.homEquiv_comp._autoParam),
  ({ homEquiv := homEquiv, homEquiv_comp := homEquiv_comp } =
      { homEquiv := homEquiv_1, homEquiv_comp := homEquiv_comp_1 }) =
    (homEquiv = homEquiv_1)
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instCategory.eq_1 : MonCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := MonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @MonCat.instCategory._proof_1,
    comp_id := @MonCat.instCategory._proof_2, assoc := @MonCat.instCategory._proof_3 }
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opowAux2.eq_4 : ∀ (o₂ a0 : ONote) (a : ℕ+) (a_1 : ONote) (m : ℕ),
  o₂.opowAux2 (a0.oadd a a_1, m) =
    match o₂.split with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      have eb := a0 * b;
      (eb + a0.mulNat k).scale (a0.oadd a a_1) + eb.opowAux a0 ((a0.oadd a a_1).mulNat m) k m
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.instInhabited : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → Inhabited (CategoryTheory.Subobject X)
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- The shape of multicoequalizer diagrams involved in the definition of coends.  -/
CategoryTheory.Limits.multispanShapeCoend : (J : Type u) → [CategoryTheory.Category.{v, u} J] → CategoryTheory.Limits.MultispanShape
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rco_eq_zero : ∀ {m n i : ℕ}, n ≤ i + m → (m...n).toList[i]! = 0
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.stepAsHetT_filterMapWithPostcondition.match_3.eq_3 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Order.Interval.Finset.Nat
List.toFinset_range : ∀ (a : ℕ), (List.range a).toFinset = Finset.range a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.coconeSMul_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) (U : Cᵒᵖ),
  (PresheafOfModules.ModuleColimit.coconeSMul hcR hcM).ι.app U =
    TypeCat.ofHom fun x =>
      match x with
      | (r, m) => (CategoryTheory.ConcreteCategory.hom (cM.ι.app U)) (r • m)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.tryRecv' : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT (ST IO.RealWorld) m] →
        [MonadLiftT BaseIO m] → Std.AtomicT (Std.CloseableChannel.Bounded.State✝ α) m (Option α)
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.mk.inj : ∀ {M : Type u_10} {N : Type u_11} {inst : MulOne M} {inst_1 : MulOne N} {toOneHom : OneHom M N}
  {map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y} {toOneHom_1 : OneHom M N}
  {map_mul'_1 : ∀ (x y : M), toOneHom_1.toFun (x * y) = toOneHom_1.toFun x * toOneHom_1.toFun y},
  { toOneHom := toOneHom, map_mul' := map_mul' } = { toOneHom := toOneHom_1, map_mul' := map_mul'_1 } →
    toOneHom = toOneHom_1
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.eq_iff_subset : ∀ {α : Type u_1} {n : ℕ} {s t : ↑(Set.powersetCard α n)}, s = t ↔ ↑s ⊆ ↑t
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- A version of `dist_le_Ico_sum_dist` with each intermediate distance replaced
with an upper estimate.  -/
dist_le_Ico_sum_of_dist_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℕ → α} {m n : ℕ},
  m ≤ n →
    ∀ {d : ℕ → ℝ},
      (∀ {k : ℕ}, m ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k) → dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i
-- Mathlib.Analysis.Convex.StdSimplex
ite_eq_mem_stdSimplex : ∀ (𝕜 : Type u_2) {ι : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] [ZeroLEOneClass 𝕜] (i : ι), (fun x => if i = x then 1 else 0) ∈ stdSimplex 𝕜 ι
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.inter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.inter m₂ =
    if (↑m₁).size ≤ (↑m₂).size then Std.DHashMap.Internal.Raw₀.filter (fun k x => m₂.contains k) m₁
    else m₁.interSmaller ↑m₂
-- Mathlib.CategoryTheory.Opposites
/-- The functor from a category to its double-opposite.  -/
CategoryTheory.opOp : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C Cᵒᵖᵒᵖ
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_mul_I : ∀ (x : ℂ), Complex.sin (x * Complex.I) = Complex.sinh x * Complex.I
-- Std.Async.System
_private.Std.Async.System.0.Std.Async.System.Environment.mk.sizeOf_spec : ∀ (toHashMap : Std.HashMap String String), sizeOf { toHashMap := toHashMap } = 1 + sizeOf toHashMap
-- Mathlib.Topology.MetricSpace.GromovHausdorff
TopologicalSpace.NonemptyCompacts.toGHSpace.eq_1 : ∀ {X : Type u} [inst : MetricSpace X] (p : TopologicalSpace.NonemptyCompacts X),
  p.toGHSpace = GromovHausdorff.toGHSpace ↥p
-- Mathlib.Data.Num.Bitwise
/-- Subtract two `SNum`s.  -/
SNum.sub : SNum → SNum → SNum
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.NormNumExt.mk.sizeOf_spec : ∀ (pre post : Bool)
  (eval : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e))
  (name : autoParam Lean.Name Mathlib.Meta.NormNum.NormNumExt.name._autoParam),
  sizeOf { pre := pre, post := post, eval := eval, name := name } = 1 + sizeOf pre + sizeOf post + sizeOf name
-- Mathlib.Topology.NhdsWithin
/-- **Alias** of `sdiff_mem_nhdsWithin_compl`. -/
diff_mem_nhdsWithin_compl : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α}, s ∈ nhds x → ∀ (t : Set α), s \ t ∈ nhdsWithin x tᶜ
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.toEquiv.eq_1 : ∀ {X Y : Type u} (i : X ≅ Y),
  i.toEquiv =
    { toFun := ⇑(CategoryTheory.ConcreteCategory.hom i.hom), invFun := ⇑(CategoryTheory.ConcreteCategory.hom i.inv),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Group.Pi.Basic
Pi.invOneClass : {I : Type u} → {f : I → Type v₁} → [(i : I) → InvOneClass (f i)] → InvOneClass ((i : I) → f i)
-- Init.Notation
/-- Function composition, usually written with the infix operator `∘`. A new function is created from
two existing functions, where one function's output is used as input to the other.

Examples:
 * `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]`
 * `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]`


Conventions for notations in identifiers:

 * The recommended spelling of `∘` in identifiers is `comp`. -/
«term_∘_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Arrow
/-- The monoidal category instance induced by the pushout-product.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasPushouts C] →
      [CategoryTheory.Limits.HasInitial C] →
        [inst_3 : CategoryTheory.CartesianMonoidalCategory C] →
          [CategoryTheory.MonoidalClosed C] →
            [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategory (CategoryTheory.Arrow C)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.finGcdMap_smul : ∀ {r : ℕ} (a : ℤ) {v : Fin 2 → ℤ}, EisensteinSeries.finGcdMap v = r → EisensteinSeries.finGcdMap (a • v) = a.natAbs * r
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.inaccessible : Lean.Expr → Lean.Meta.Match.Pattern
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Subtraction `y ↦ y - x` as an `IsometryEquiv`.  -/
IsometryEquiv.subRight : {G : Type v} → [inst : AddGroup G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricVAdd Gᵃᵒᵖ G] → G → G ≃ᵢ G
-- Mathlib.Topology.Algebra.Monoid
/-- If `f : α → M` and `g : β → M` both tend to zero on the cofinite filter, then so does
`fun i : α × β ↦ f i.1 * g i.2`.  -/
tendsto_mul_cofinite_nhds_zero : ∀ {M : Type u_3} {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M]
  {f : α → M} {g : β → M},
  Filter.Tendsto f Filter.cofinite (nhds 0) →
    Filter.Tendsto g Filter.cofinite (nhds 0) → Filter.Tendsto (fun i => f i.1 * g i.2) Filter.cofinite (nhds 0)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_left_bijective : ∀ {x : ℝ}, x ≠ 0 → Function.Bijective fun y => y ^ x
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSMulCommClass : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M] [inst_4 : SMul R₁ M] [inst_5 : ContinuousConstSMul R₁ M]
  [SMulCommClass R R₁ M], SMulCommClass R R₁ C(α, M)
-- Mathlib.Order.Birkhoff
OrderEmbedding.infIrredUpperSet_surjective : ∀ {α : Type u_1} [inst : PartialOrder α] [Finite α], Function.Surjective ⇑OrderEmbedding.infIrredUpperSet
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.recordTheoremWithBadKeys.unsafe_1 : Lean.Meta.SimpTheorem → Lean.Meta.Simp.Diagnostics → Bool
-- Init.Data.Int.Order
Int.NonNeg.elim : ∀ {a : ℤ}, a.NonNeg → ∃ n, a = ↑n
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.commSemigroupTopologicalClosure.eq_1 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [inst_2 : SeparatelyContinuousMul M]
  [inst_3 : T2Space M] (s : Subsemigroup M) (hs : ∀ (x y : ↥s), x * y = y * x),
  s.commSemigroupTopologicalClosure hs = { toSemigroup := MulMemClass.toSemigroup s.topologicalClosure, mul_comm := ⋯ }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_le_size_insertMany : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α], m.WF → ∀ {l : ρ}, m.size ≤ (m.insertMany l).size
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesLimitsOfSize_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), Subsingleton (CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The sine of the angle between two vectors is nonnegative.  -/
InnerProductGeometry.sin_angle_nonneg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  0 ≤ Real.sin (InnerProductGeometry.angle x y)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.isoApp_braiding : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)]
  {X Y : (i : I) → C i} {i : I}, CategoryTheory.Pi.isoApp (β_ X Y) i = β_ (X i) (Y i)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.takeWhile : (Char → Bool) → Lean.ParseImports.Parser
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coeff_mapAlgHom_apply : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (p : Polynomial A) (n : ℕ),
  ((Polynomial.mapAlgHom f) p).coeff n = f (p.coeff n)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P Q : Fin 3 → R),
  W'.negAddY P Q =
    -P 1 * Q 0 ^ 3 * P 2 ^ 3 + 2 * P 1 * Q 1 ^ 2 * P 2 ^ 3 - 3 * P 0 ^ 2 * Q 0 * Q 1 * P 2 ^ 2 * Q 2 +
                                      3 * P 0 * P 1 * Q 0 ^ 2 * P 2 * Q 2 ^ 2 +
                                    P 0 ^ 3 * Q 1 * Q 2 ^ 3 -
                                  2 * P 1 ^ 2 * Q 1 * Q 2 ^ 3 +
                                W'.a₁ * P 0 * Q 1 ^ 2 * P 2 ^ 4 +
                              W'.a₁ * P 1 * Q 0 * Q 1 * P 2 ^ 3 * Q 2 -
                            W'.a₁ * P 0 * P 1 * Q 1 * P 2 * Q 2 ^ 3 -
                          W'.a₁ * P 1 ^ 2 * Q 0 * Q 2 ^ 4 -
                        2 * W'.a₂ * P 0 * Q 0 * Q 1 * P 2 ^ 4 * Q 2 +
                      2 * W'.a₂ * P 0 * P 1 * Q 0 * P 2 * Q 2 ^ 4 +
                    W'.a₃ * Q 1 ^ 2 * P 2 ^ 6 -
                  W'.a₃ * P 1 ^ 2 * Q 2 ^ 6 -
                W'.a₄ * Q 0 * Q 1 * P 2 ^ 6 * Q 2 -
              W'.a₄ * P 0 * Q 1 * P 2 ^ 4 * Q 2 ^ 3 +
            W'.a₄ * P 1 * Q 0 * P 2 ^ 3 * Q 2 ^ 4 +
          W'.a₄ * P 0 * P 1 * P 2 * Q 2 ^ 6 -
        2 * W'.a₆ * Q 1 * P 2 ^ 6 * Q 2 ^ 3 +
      2 * W'.a₆ * P 1 * P 2 ^ 3 * Q 2 ^ 6
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInvolutiveNeg.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : InvolutiveNeg G],
  Filter.Germ.instInvolutiveNeg = { toNeg := Filter.Germ.instNeg, neg_neg := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.getToIntId?.go? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingEquiv.quotientBot_symm_mk : ∀ {R : Type u_1} [inst : Ring R] (r : R), (RingEquiv.quotientBot R).symm r = (Ideal.Quotient.mk ⊥) r